tiny vs Merge

[arademaker]

tinySUMO.kif is considered the minimal set of axioms necessary by SigmaKEE to run the transformations. Merge.kif, on the other hand, is the top-level ontology in SUMO.

We would expect that tinySUMO.kif is a subset of Merge.kif. If so, instead of having copies of axioms from Merge.kif in tinySUMO.kif, we can remove from Merge.kif whatever is already in tinySUMO.kif and call it something like Top.kif ?

Preliminary evaluation shows that some axioms from tinySUMO.kif are not in Merge.kif:

CL-USER> (length (with-open-file (in "Merge.kif")
	   (loop for a = (read in nil nil)
		 while a collect a)))
5074
CL-USER> (length (with-open-file (in "tinySUMO.kif")
	   (loop for a = (read in nil nil)
		 while a collect a)))
133
CL-USER> (length (set-difference *tiny* *merge* :test #'equal))
51

[arademaker]

Related to some discussion started in own-pt/common-sense-lean#10

[arademaker]

The axioms in tiny not in Merge are:

CL-USER> (set-difference *tiny* *merge* :test #'equal)
((=>
  (AND (MINVALUE ?R ?ARG ?N) (?R @ARGS)
       (EQUAL ?VAL (LISTORDERFN (LISTFN @ARGS) ?ARG)))
  (GREATERTHAN ?VAL ?N))
 (DOMAIN LISTORDERFN 2 INTEGER) (DOMAIN MINVALUE 1 RELATION)
 (INSTANCE MINVALUE TERNARYRELATION) (PARENTS ABRAHAMLINCOLN ?Y)
 (=> (INSTANCE ?X HUMAN) (PARENTS ?X (ADDITIONFN 1 1)))
 (DOMAIN PARENTS 2 INTEGER) (DOMAIN PARENTS 1 HUMAN)
 (INSTANCE PARENTS BINARYRELATION) (SUBCLASS INTEGER QUANTITY)
 (DOMAIN FLOORFN 1 READLNUMBER) (DOMAIN LOCATED 2 PHYSICAL)
 (INSTANCE LOCATED BINARYRELATION) (INSTANCE ABRAHAMLINCOLN HUMAN)
 (SUBCLASS HUMAN PHYSICAL)
 (=> (AND (SUBCLASS ?B ?A) (INSTANCE ?C ?B)) (INSTANCE ?C ?A))
 (=> (AND (SUBCLASS ?B ?A) (SUBCLASS ?C ?B)) (SUBCLASS ?C ?A))
 (TERMFORMAT ENGLISHLANGUAGE SUBCLASS "subclass")
 (TERMFORMAT ENGLISHLANGUAGE INSTANCE "instance")
 (FORMAT ENGLISHLANGUAGE SUBCLASS "%1 is a %2")
 (DOCUMENTATION SUBCLASS ENGLISHLANGUAGE "A relation stating that
one class is more specific than another.")
 (FORMAT ENGLISHLANGUAGE INSTANCE "%1 is an instance of %2")
 (DOCUMENTATION INSTANCE ENGLISHLANGUAGE "A relation stating the
class membership of an individual.")
 (DOMAIN PARTITION 2 SETORCLASS) (DOMAIN PARTITION 1 SETORCLASS)
 (DOMAIN TERMFORMAT 1 HUMANLANGUAGE) (INSTANCE TERMFORMAT TERNARYRELATION)
 (DOMAIN FORMAT 1 HUMANLANGUAGE) (INSTANCE FORMAT TERNARYRELATION)
 (INSTANCE DOCUMENTATION TERNARYRELATION) (INSTANCE INSTANCE BINARYRELATION)
 (DOMAIN INSTANCE 2 ENTITY) (=> (SUBCLASS ?X ?Y) (INSTANCE ?X SETORCLASS))
 (DOMAIN SUBCLASS 2 ENTITY) (DOMAIN SUBCLASS 1 ENTITY)
 (INSTANCE SUBCLASS TRANSITIVERELATION) (INSTANCE SUBCLASS BINARYRELATION)
 (DOMAIN DOMAINSUBCLASS 2 INTEGER) (INSTANCE DOMAINSUBCLASS TERNARYRELATION)
 (=> (AND (INSTANCE ?F FUNCTION) (RANGESUBCLASS ?F ?C) (INSTANCE ?I (?F ?X)))
  (INSTANCE ?I ?C))
 (INSTANCE RANGE BINARYRELATION) (DOMAIN DOMAIN 2 INTEGER)
 (INSTANCE DOMAIN TERNARYRELATION)
 (=> (INSTANCE ?R TRANSITIVERELATION)
  (=> (AND (?R ?A ?B) (?R ?B ?C)) (?R ?A ?C)))
 (SUBCLASS TRANSITIVERELATION RELATION) (SUBCLASS FUNCTION RELATION)
 (SUBCLASS ENGLISHLANGUAGE HUMANLANGUAGE) (SUBCLASS HUMANLANGUAGE ENTITY)
 (SUBCLASS SYMBOLICSTRING ENTITY) (SUBCLASS SETORCLASS ENTITY)
 (SUBCLASS RELATION ENTITY))

[apease]

some axioms in tinySUMO.kif are different since it has been just a hack for testing. For example, some subclass statements bypass intervening levels of the hierarchy

[arademaker]

I would prefer no redundancies, more modularity and these extra axioms could be added in the test cases... as part of a particular test.

So the question is if all axioms above from the difference are the ones that can be removed from tiny...

[arademaker]

Take domain of partition in Merge.kif as:

(domain partition 1 Class)
(domain partition 2 Class)

But in tinySUMO:

(domain partition 1 SetOrClass)
(domain partition 2 SetOrClass)

This does not make sense. Proofs using tinySUMO are not valid using Merge.kif and the rest of SUMO.

[apease]

again, tinySUMO is just a hack to try out inferences, I'm not recommending its use