exhaustiveDecomposition axioms

[arademaker]

http://sigma.ontologyportal.org:8080/sigma/Browse.jsp?kb=SUMO&lang=EnglishLanguage&flang=SUO-KIF&term=exhaustiveDecomposition

I found two axioms for exhaustiveDecomposition. I believe only the second one is right and the first should be removed from Merge.kif:

(=>
   (exhaustiveDecomposition @ROW)
   (=>
      (inList ?ELEMENT (ListFn @ROW))
      (instance ?ELEMENT Class)))

(=>
   (exhaustiveDecomposition ?CLASS @ROW)
   (forall (?OBJ)
      (=>
         (instance ?OBJ ?CLASS)
         (exists (?ITEM)
            (and
               (inList ?ITEM (ListFn @ROW))
               (instance ?OBJ ?ITEM))))))

Note that (instance ?OBJ ?ITEM) already impose ?ITEM to be a SetOrClass by the definition of instance. Moreover, the type of its arguments are already defined by the domain declaration, right?

(domain exhaustiveDecomposition 1 Class)
(domain exhaustiveDecomposition 2 Class)

Assuming that in a VariableArityRelation, the second declaration above says that in the case of a row variable being used, all its elements should have the same type. Actually, I really prefer something more explicit about the types of VariableArityRelation relations and its range of min and max number of arguments. The two declarations of the domain say that min arity is 2?

[apease]

the first axiom says every argument to exhaustiveDecomposition is a Class. That is accurate. The domain declaration is explicit about the argument number but we also need a specification for the arguments beyond that number. The type guards created during translation to TPTP and TFF0 take care of this but it's certainly good to have an explicit axiom stating the types. A better axiom would state that all the types of the arguments after the last explicit domain statement are the same. Would you like to try writing that?

[arademaker]

We pay a high price in terms of complexity for having VariableArityRelation, considering that it is not used as much as expected. I really don't like to add those axioms, but anyway, my first attempt using the ConsFn define in https://github.com/arademaker/sumo/blob/lists/list.kif#L4:

(=>
 (and
  (instance ?REL VariableArityRelation)
  (instance ?REL Predicate)
  (?REL @ROW)
  (equal ?L (ListFn @ROW)))
 (argumentsType ?REL ?L 0 (ListLengthFn ?L)))

(=> (and (argumentsType ?REL (ConsFn ?X ?L) ?N ?M)
	 (lessThan ?N ?M)
	 (domain ?REL ?N ?CLASS))
    (and (instance ?X ?CLASS)
	 (argumentsType ?REL ?L (SucessorFn ?N) ?M)))

(=> (and (argumentsType ?REL (ConsFn ?X ?L) ?N ?M)
	 (equal ?N ?M)
	 (domain ?REL ?N ?CLASS))
    (and (instance ?X ?CLASS)
	 (restArgumentsType ?REL ?L ?CLAS)))

(=> (restArgumentsType ?REL (ConsFn ?X ?L) ?CLASS)
    (and (instance ?X ?CLASS)
	 (argumentsType ?REL ?L ?CLASS)))

(argumentsType ?REL NullList ?N ?M)
(restArgumentsType ?REL NullList ?CLASS)

The difficult part is how to get the "the last explicit domain statement from a given ?R"! Another possible simpler alternative is

(=> (and
     (instance ?REL VariableArityRelation)
     (instance ?REL Predicate)
     (?REL @ROW)
     (=> (and
	  (domain ?REL ?N ?CLASS1)
	  (not (exists (?M)
		       (and (greaterThan ?M ?N)
			    (domain ?REL ?M ?CLASS2)))))
	 (forall (?M)
		 (and (greaterThan ?M ?N)
		      (equal ?A (ListOrderFn (ListFn @ROW) ?M))
		      (instance ?A ?CLASS1))))))

But I am still not very confortable with those kind of axioms!