tinySUMO.kif

;; We ask the people using or referencing SUMO cite our primary paper:

;; Niles, I., and Pease, A.  2001.  Towards a Standard Upper Ontology.  In
;; Proceedings of the 2nd International Conference on Formal Ontology in
;; Information Systems (FOIS-2001), Chris Welty and Barry Smith, eds,
;; Ogunquit, Maine, October 17-19, 2001.  Also see http://www.ontologyportal.org

;; author: Adam Pease, apease [at] articulatesoftware [dot] com

(domain subclass 1 Class)
(domain subclass 2 Class)
(instance subclass BinaryPredicate)
(instance subclass TransitiveRelation)

(subclass BinaryRelation Relation)
(subclass BinaryPredicate Predicate)
(subclass Predicate Relation)
(subclass Relation Entity)
(subclass Physical Entity)
(subclass Abstract Entity)
(subclass List Abstract)
(subclass TimePosition Abstract)
(subclass TimeInterval TimePosition)
(subclass Set Abstract)
(subclass Class Abstract)
(subclass Process Physical)
(subclass Object Physical)
(subclass SelfConnectedObject Object)
(subclass Substance SelfConnectedObject)
(subclass Collection Object)
(subclass SingleFamilyResidence SelfConnectedObject)
(subclass SymbolicString Entity)
(subclass HumanLanguage Entity)
(subclass EnglishLanguage HumanLanguage)
(subclass VariableArityRelation Relation)
(subclass BinaryFunction Function)
(subclass TernaryFunction Function)
(subclass UnaryFunction Function)
(subclass Function Relation)
(subclass TernaryPredicate Predicate)
(subclass Attribute Abstract)
(subclass PositionalAttribute Attribute)
(subclass Physical Entity)
(subclass Region Physical)
(subclass GeographicArea Region)
(subclass Nation GeographicArea)
(subclass City GeographicArea)
(subclass Road GeographicArea)
(subclass TransitiveRelation Relation)
(subclass SymmetricRelation Relation)
(subclass MilitaryForce Physical)
(subclass AutonomousAgent Object)
(subclass Organism AutonomousAgent)
(subclass Organization AutonomousAgent)
(subclass Vehicle Object)
(subclass Carrying Process)
(subclass UnitOfMeasure Abstract)
(instance TonMass UnitOfMeasure)
(instance PoundMass UnitOfMeasure)
(subclass CaseRole BinaryPredicate)
(subclass ComputerProgram Abstract)
(subclass Mouth Object)
(subclass RelationalAttribute Attribute)
(subclass ContentBearingObject Object)
(subclass PathologicProcess Process)
(subclass HeartAttack PathologicProcess)

(=>
  (subclass ?X ?Y)
  (and
    (instance ?X Class)
    (instance ?Y Class)))

(domain disjoint 1 Class)	
(domain disjoint 2 Class)	
(instance disjoint BinaryPredicate)
(instance disjoint SymmetricRelation)

(domain contraryAttribute 1 Attribute)	
(instance contraryAttribute VariableArityRelation)

(disjoint Abstract Physical)
(disjoint Object Process)

(=>
  (disjoint ?CLASS1 ?CLASS2)
  (forall (?INST)
    (not
      (and
        (instance ?INST ?CLASS1)
        (instance ?INST ?CLASS2)))))
       
(=>
  (and
    (disjoint ?A ?B)
    (subclass ?C ?A))
  (disjoint ?C ?B))
  
(=>
  (instance ?R TransitiveRelation)
  (=>
    (and
      (?R ?A ?B)
      (?R ?B ?C))
    (?R ?A ?C)))

(=>
  (and
    (instance ?REL SymmetricRelation)
    (?REL ?INST1 ?INST2))
  (?REL ?INST2 ?INST1))

(instance domain TernaryPredicate)
(domain domain 1 Relation)
(domain domain 2 Integer)
(domain domain 3 Class)

(instance range BinaryRelation)
(domain range 1 Function)
(domain range 2 Class)

(domain rangeSubclass 1 Function)
(domainSubclass rangeSubclass 2 Class)
(instance rangeSubclass AsymmetricRelation)
(instance rangeSubclass BinaryPredicate)

;(=>
;  (and
;    (instance ?F Function)
;    (rangeSubclass ?F ?C)
;    (instance ?I (?F ?X)))
;  (instance ?I ?C))

(instance domainSubclass TernaryPredicate)
(domain domainSubclass 1 Relation)
(domain domainSubclass 2 Integer)
(domain domainSubclass 3 Class)

(instance subclass BinaryRelation)
(instance subclass TransitiveRelation)
(domain subclass 1 Class)
(domain subclass 2 Class)

(=>
  (subclass ?X ?Y)
  (instance ?X Class))

(domain subrelation 1 Relation)		
(domain subrelation 2 Relation)	
(instance subrelation BinaryPredicate)
(instance subrelation TransitiveRelation)

(=>
  (and
    (subrelation ?REL1 ?REL2)
    (instance ?REL1 Predicate)
    (instance ?REL2 Predicate)
    (?REL1 @ROW))
  (?REL2 @ROW))

(instance part BinaryPredicate)
(instance part TransitiveRelation)
(domain part 1 Object)
(domain part 2 Object)

(instance piece BinaryPredicate)
(instance piece TransitiveRelation)
(domain piece 1 Object)
(domain piece 2 Object)
(subrelation piece part)

(domain instance 1 Entity)
(domain instance 2 Class)
(instance instance BinaryRelation)

(instance documentation TernaryPredicate)
(domain documentation 1 Entity)
(domain documentation 2 HumanLanguage)
(domain documentation 3 SymbolicString)

(instance format TernaryPredicate)
(domain format 2 Entity)
(domain format 1 HumanLanguage)
(domain format 3 SymbolicString)

(instance termFormat TernaryPredicate)
(domain termFormat 2 Entity)
(domain termFormat 1 HumanLanguage)
(domain termFormat 3 SymbolicString)

(domain exhaustiveDecomposition 1 Class)
(domain exhaustiveDecomposition 2 Class)
(instance exhaustiveDecomposition Predicate)
(instance exhaustiveDecomposition VariableArityRelation)

(domain disjointDecomposition 1 Class)
(domain disjointDecomposition 2 Class)
(instance disjointDecomposition Predicate)
(instance disjointDecomposition VariableArityRelation)

(domain partition 1 Class)
(domain partition 2 Class)
(instance partition Predicate)		
(instance partition VariableArityRelation)

(=>
    (partition @ROW)
    (and
        (exhaustiveDecomposition @ROW)
        (disjointDecomposition @ROW)))

(subclass Animal Organism)
(subclass Plant Organism)
(subclass Fungus Organism)
(subclass Microorganism Organism)

(partition Organism Animal Plant Fungus Microorganism)

(documentation instance EnglishLanguage "A relation stating the
class membership of an individual.")
(format EnglishLanguage instance "%1 is an instance of %2")

(documentation subclass EnglishLanguage "A relation stating that
one class is more specific than another.")

(format EnglishLanguage subclass "%1 is a %2")
(termFormat EnglishLanguage instance "instance")
(termFormat EnglishLanguage subclass "subclass")

(=>
  (and
    (subclass ?B ?A)
    (subclass ?C ?B))
  (subclass ?C ?A))

(=>
  (and
    (subclass ?B ?A)
    (instance ?C ?B))
  (instance ?C ?A))

(subclass Human AutonomousAgent)
(instance AbrahamLincoln Human)

(instance located BinaryRelation)
(instance located AntisymmetricRelation)
(domain located 1 Physical)
(domain located 2 Physical)

(subclass AntisymmetricRelation BinaryRelation)
(=>
    (instance ?REL AntisymmetricRelation)
    (forall (?INST1 ?INST2)
        (=>
            (and
                (?REL ?INST1 ?INST2)
                (?REL ?INST2 ?INST1))
            (equal ?INST1 ?INST2))))

(instance attribute BinaryPredicate)
(domain attribute 1 Entity)
(domain attribute 2 Attribute)

(domain property 1 Entity)	
(domain property 2 Attribute)	
(instance property BinaryPredicate)
(subrelation attribute property)

(instance ChemicalEquilibrium Attribute)
(instance ChemicalProcess Process)

(=>
  (property ?PROCESS ChemicalEquilibrium)
  (instance ?PROCESS ChemicalProcess))

(instance maleficiary BinaryPredicate)
(domain maleficiary 1 Process)
(domain maleficiary 2 AutonomousAgent)

(instance agent BinaryPredicate)
(domain agent 1 Process)
(domain agent 2 AutonomousAgent)

(instance objectTransferred BinaryPredicate)
(domain objectTransferred 1 Process)
(domain objectTransferred 2 Object)

(instance origin BinaryPredicate)
(domain origin 1 Process)
(domain origin 2 Object)

(domain destination 1 Process)
(domain destination 2 Entity)
(instance destination BinaryPredicate)

(instance experiencer BinaryPredicate)
(domain experiencer 1 Process)
(domain experiencer 2 AutonomousAgent)

(instance patient BinaryPredicate)
(domain patient 1 Process)
(domain patient 2 Object)

(instance instrument BinaryPredicate)
(domain instrument 1 Process)
(domain instrument 2 Object)

(domain refers 1 Entity)	
(domain refers 2 Entity)	
(instance refers BinaryPredicate)

;;-------------------------------------------------
;; Numbers and Arithmetic

;; Formula.MATH_FUNCTIONS

(domain AdditionFn 1 RealNumber)
(domain AdditionFn 2 RealNumber)
(instance AdditionFn BinaryFunction)
(range AdditionFn RealNumber)

(domain SubtractionFn 1 RealNumber)
(domain SubtractionFn 2 RealNumber)
(instance SubtractionFn BinaryFunction)
(range SubtractionFn RealNumber)

(domain MultiplicationFn 1 RealNumber)
(domain MultiplicationFn 2 RealNumber)
(instance MultiplicationFn BinaryFunction)
(range MultiplicationFn RealNumber)

(domain DivisionFn 1 RealNumber)
(domain DivisionFn 2 RealNumber)
(instance DivisionFn BinaryFunction)
(range DivisionFn RealNumber)

(domain FloorFn 1 RealNumber)
(instance FloorFn UnaryFunction)
(range FloorFn Integer)

(subclass Quantity Abstract)
(subclass RealNumber Quantity)
(subclass RationalNumber RealNumber)
(subclass Integer RationalNumber)

(subclass PositiveInteger Integer)

(=>
    (instance ?X PositiveInteger)
    (greaterThan ?X 0))

(subclass NonnegativeInteger Integer)

(=>
    (instance ?X NonnegativeInteger)
    (greaterThan ?X -1))

(subclass NonnegativeRealNumber RealNumber)

(=>
    (instance ?NUMBER NonnegativeRealNumber)
    (or
        (equal
            (SignumFn ?NUMBER) 1.0)
        (equal
            (SignumFn ?NUMBER) 0.0)))

(domain SignumFn 1 RealNumber)
(instance SignumFn UnaryFunction)
(range SignumFn Integer)

(<=>
    (instance ?NUMBER NonnegativeRealNumber)
    (and
        (greaterThanOrEqualTo ?NUMBER 0.0)
        (instance ?NUMBER RealNumber)))

(domain MeasureFn 1 RealNumber)
(domain MeasureFn 2 UnitOfMeasure)
(instance MeasureFn BinaryFunction)
(range MeasureFn PhysicalQuantity)

(instance measure BinaryPredicate)
(domain measure 1 Object)
(domain measure 2 PhysicalQuantity)

(instance parents BinaryRelation)
(domain parents 1 Human)
(domain parents 2 Integer)
(=>
  (instance ?X Human)
  (parents ?X (AdditionFn 1 1)))

;;(parents AbrahamLincoln ?Y)

;;-------------------------------------------------
	
(instance minValue TernaryPredicate)
(domain minValue 1 Relation)
(domain minValue 2 Integer)	
(domain minValue 3 Quantity)
	
;; need all Formula.COMPARISON_OPERATOR 

(domain greaterThanOrEqualTo 1 RealNumber)
(domain greaterThanOrEqualTo 2 RealNumber)
(instance greaterThanOrEqualTo BinaryPredicate)

(domain lessThan 1 RealNumber)
(domain lessThan 2 RealNumber)
(instance lessThan BinaryPredicate)

(domain lessThanOrEqualTo 1 RealNumber)
(domain lessThanOrEqualTo 2 RealNumber)
(instance lessThanOrEqualTo BinaryPredicate)

(domain greaterThanOrEqualTo 1 RealNumber)
(domain greaterThanOrEqualTo 2 RealNumber)
(instance greaterThanOrEqualTo BinaryPredicate)

(domain greaterThan 1 RealNumber)
(domain greaterThan 2 RealNumber)
(instance greaterThan BinaryPredicate)

(domain ListOrderFn 1 List)		
(domain ListOrderFn 2 PositiveInteger)
(instance ListOrderFn BinaryFunction)		
; (instance ListOrderFn PartialValuedRelation)		
(range ListOrderFn Entity)

(domain ListLengthFn 1 List)
(instance ListLengthFn UnaryFunction)
(range ListLengthFn NonnegativeInteger)

(domain ListSumFn 1 List)
(instance ListSumFn UnaryFunction)
(range ListSumFn RealNumber)

(domain ListFn 1 Entity)	
(instance ListFn Function)
(instance ListFn VariableArityRelation)	
(range ListFn List)

; can't mix value types in a list
;(=>
;  (and
;    (minValue ?R ?ARG ?N)
;    (?R @ARGS)
;    (equal ?VAL
;      (ListOrderFn
;        (ListFn @ARGS) ?ARG)))
;  (greaterThan ?VAL ?N))

(domain LastFn 1 List)
(instance LastFn UnaryFunction)
(range LastFn Entity)

(domain FirstFn 1 List)
(instance FirstFn UnaryFunction)
(range FirstFn Entity)

(instance inList BinaryPredicate)
(domain inList 1 Entity)	
(domain inList 2 List)

(=>
  (inList ?ITEM ?LIST)
  (exists (?NUMBER)
    (equal
      (ListOrderFn ?LIST ?NUMBER) ?ITEM)))
            
(forall (@ROW ?ITEM)
  (equal
    (ListOrderFn
      (ListFn @ROW ?ITEM)
      (ListLengthFn
        (ListFn @ROW ?ITEM))) ?ITEM))

(=>
  (equal ?LIST1 ?LIST2)
  (=>
    (and
      (equal ?LIST1
        (ListFn @ROW1))
      (equal ?LIST2
        (ListFn @ROW2)))
      (forall (?NUMBER)
        (equal
          (ListOrderFn
            (ListFn @ROW1) ?NUMBER)
          (ListOrderFn
            (ListFn @ROW2) ?NUMBER)))))

(=>
  (and
    (domain ?REL ?NUMBER ?CLASS)
    (instance ?REL Predicate)
    (?REL @ROW))
  (instance
    (ListOrderFn
      (ListFn @ROW) ?NUMBER) ?CLASS))

(=>
  (equal (FirstFn ?L) (LastFn ?L))
  (equal (ListLengthFn ?L) 1))

(=>
  (inList ?I (ListFn ?H))
  (equal ?I ?H))

(=>
  (inList ?I (ListFn ?H @ROW))
  (or
    (and
      (equal (FirstFn (ListFn ?H @ROW)) (LastFn (ListFn ?H @ROW)))
      (equal ?I ?H))
    (inList ?I (ListFn @ROW))))

(=>
  (inList ?I (ListFn ?H @ROW))
  (or
    (equal ?I ?H)
    (inList ?I (ListFn @ROW))))

(domain orientation 1 Object)	
(domain orientation 2 Object)	
(domain orientation 3 PositionalAttribute)		
(instance orientation TernaryPredicate)
(instance Right PositionalAttribute)
(instance Left PositionalAttribute)

(<=>
     (orientation ?OBJ1 ?OBJ2 Right)
     (orientation ?OBJ2 ?OBJ1 Left))

(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (equal 1
            (ListLengthFn ?L)))
    (equal ?A
        (ListOrderFn ?L 1)))

(domain AverageFn 1 List)
(instance AverageFn UnaryFunction)
(range AverageFn RealNumber)

(=>
    (and
        (equal ?A
            (AverageFn ?L))
        (greaterThan
            (ListLengthFn ?L) 0))
    (equal ?A
        (DivisionFn
            (ListSumFn ?L)
            (ListLengthFn ?L))))

(domain RemainderFn 1 Integer)
(domain RemainderFn 2 Integer)
(instance RemainderFn BinaryFunction)
(range RemainderFn Integer)

(<=>
    (equal
        (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
    (equal
        (AdditionFn
            (MultiplicationFn
                (FloorFn
                    (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))

(domain AbsoluteValueFn 1 RealNumber)
(instance AbsoluteValueFn UnaryFunction)
(range AbsoluteValueFn NonnegativeRealNumber)

(<=>
    (and
        (equal
            (AbsoluteValueFn ?NUMBER1) ?NUMBER2)
        (instance ?NUMBER1 RealNumber)
        (instance ?NUMBER2 RealNumber))
    (or
        (and
            (instance ?NUMBER1 NonnegativeRealNumber)
            (equal ?NUMBER1 ?NUMBER2))
        (and
            (instance ?NUMBER1 NegativeRealNumber)
            (equal ?NUMBER2
                (SubtractionFn 0.0 ?NUMBER1)))))

(domain FirstFn 1 List)
(instance FirstFn UnaryFunction)
(range FirstFn Entity)

(=>
  (equal ?X (FirstFn ?L))
  (equal ?L (ListFn ?X @ROW)))

(=>
  (equal ?L (ListFn ?X @ROW))
  (equal ?X (FirstFn ?L)))

(=>
  (equal ?X (FirstFn ?L))
  (equal ?L (ListFn ?X @ROW)))

(=>
  (equal ?L (ListFn ?X @ROW))
  (equal ?X (FirstFn ?L)))

(domain SubListFn 1 Integer)
(domain SubListFn 2 Integer)
(domain SubListFn 3 List)
(instance SubListFn TernaryFunction)
(range SubListFn List)

(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?A
        (AdditionFn
            (FirstFn ?L)
            (ListSumFn
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))

(instance Male Attribute)
(instance Female Attribute)
(contraryAttribute Male Female)
 
(domain mother 1 Organism)	
(domain mother 2 Organism)	
(instance mother BinaryPredicate)
 
(domain father 1 Organism)	
(domain father 2 Organism)	
(instance father BinaryPredicate)
                   
(=>
  (mother ?CHILD ?MOTHER)
  (attribute ?MOTHER Female))
  
(domain WhenFn 1 Physical)		
(instance WhenFn UnaryFunction)	
(range WhenFn TimeInterval)  

(domain earlier 1 TimeInterval)	
(domain earlier 2 TimeInterval)	
(instance earlier BinaryPredicate)
(instance earlier TransitiveRelation)

(subclass ClosedWorldPredicate Predicate)

(instance subclass ClosedWorldPredicate)