;; ================================================
;;      SUMO (Suggested Upper Merged Ontology)
;; ================================================

;; This is the source file for the SUMO (Suggested Upper Merged Ontology), 
;; an ontology that was developed within the SUO Working Group by merging
;; the SUO "candidate content" sources and refining and extending this content on 
;; the basis of various knowledge engineering projects and input from the SUO 
;; Working Group.

;; The SUMO incorporates elements of John Sowa's upper ontology (as described at 
;; http://www.bestweb.net/~sowa/ontology/toplevel.htm and in Chapter 2 of his 
;; book _Knowledge Representation_, Brooks/Cole, 2000), Russell and Norvig's 
;; ontology, PSL (Process Specification Language), Casati and Varzi's theory of 
;; holes, Allen's temporal axioms, the relatively noncontroversial elements of 
;; Smith's and Guarino's respective mereotopologies, the KIF formalization of the 
;; CPR (Core Plan Representation), the ontologies available on the Ontolingua 
;; server maintained by Stanford University's Knowledge Systems Laboratory, the 
;; ontologies developed by ITBM-CNR, some of the spatial relations from an 
;; unpublished paper by Iris Tommelein and Anil Gupta entitled "Conceptual 
;; Structures for Spatial Reasoning", and a "Structural Ontology" proposed by 
;; David Whitten and substantially revised and extended by Chris Menzel.
;; Note that some of the subclasses of 'Process' in the SUMO were originally 
;; inspired by some of the verb classes from the second part of Beth Levin's book 
;; "English Verb Classes and Alternations:  A Preliminary Investigation."

;; The knowledge representation language in which the SUMO is expressed is SUO-KIF, 
;; which stands for "Standard Upper Ontology - Knowledge Interchange Format".  SUO-KIF 
;; is a simplified form of the popular KIF knowledge representation language.  A 
;; specification of SUO-KIF can be found at:  http://suo.ieee.org/suo-kif.html.  It 
;; should be noted that some of the axioms in the SUMO make use of row variables 
;; (indicated with a "@" prefix).  Such variables are not currently part of the SUO-
;; KIF specification, but they simplify matters significantly in some cases.  Details 
;; about row variables can be found in the following paper:  
;; http://reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI2001.pdf.

;; The SUMO is a modular ontology.  That is, the ontology is divided into 
;; self-contained subontologies.  Each subontology is indicated by a section 
;; header, and the dependencies between the subontologies are specified with 
;; statements of the form ";; INCLUDES '<SUBONTOLOGY>'".  These statements are 
;; found at the beginning of each section.  The dependencies between the 
;; various subontologies can also be graphed informally as follows:
;;
;;                             STRUCTURAL ONTOLOGY
;;                                      +
;;                                      |
;;                                      |
;;                                      +
;;                                 BASE ONTOLOGY 
;;                                 /   |   |   \
;;                                /    |   |    \
;;                               /     |   |     \
;;                              /      |   |      \
;;                             /       |   |       \
;;                            +        +   +        +
;;             SET/CLASS THEORY   NUMERIC  TEMPORAL  MEREOTOPOLOGY
;;                               /     |        |           |
;;                              /      |        |           |
;;                             /       |        |           |
;;                            +        +        +           +
;;                        GRAPH   MEASURE   PROCESSES +--+ OBJECTS
;;                                              +           +
;;                                               \         /
;;                                                \       /
;;                                                 \     /
;;                                                  +   +
;;                                                 QUALITIES
;;
;; 
;; Note that the "+" sign at the end of an arc indicates the direction of 
;; dependency - the node near the sign includes the subontology at the other 
;; end of the arc.  Note too that in some cases the dependency is 
;; bidirectional.  Separating ontologies in cases like these is useful when 
;; their respective topics can be cleanly differentiated.

;; The SUMO is copyrighted by Teknowledge (c) 2002.  It is released under the 
;; GNU Public License <http://www.gnu.org/copyleft/gpl.html>.  Users of this 
;; code also consent, by use of this material, to credit Teknowledge in any writings, 
;; briefings, publications, presentations, or other representations of any code 
;; or other product which incorporates, builds on, or uses this material. 


;; BEGIN FILE


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;   STRUCTURAL ONTOLOGY   ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; INCLUDES 'BASE ONTOLOGY'

;; The Structural Ontology consists of definitions of certain syntactic 
;; abbreviations that can be both heuristically useful and computationally 
;; advantageous.

(instance instance BinaryPredicate)
(domain instance 1 Entity)
(domain instance 2 SetOrClass)
(documentation instance "An object is an &%instance of a &%SetOrClass if 
it is included in that &%SetOrClass.  An individual may be an instance of many 
classes, some of which may be subclasses of others.  Thus, there is no 
assumption in the meaning of &%instance about specificity or uniqueness.")

(subrelation immediateInstance instance)
(instance immediateInstance AsymmetricRelation)
(instance immediateInstance IntransitiveRelation)
(documentation immediateInstance "An object is an &%immediateInstance of 
a &%SetOrClass if it is an instance of the &%SetOrClass and there does not exist a 
subclass of &%SetOrClass such that it is an instance of the subclass.")

(=>
   (immediateInstance ?ENTITY ?CLASS)
   (not (exists (?SUBCLASS)
      (and
         (subclass ?SUBCLASS ?CLASS)
         (instance ?ENTITY ?SUBCLASS)))))
                 
(instance inverse BinaryPredicate)
(instance inverse IrreflexiveRelation)
(instance inverse IntransitiveRelation)
(instance inverse SymmetricRelation)
(domain inverse 1 BinaryRelation)
(domain inverse 2 BinaryRelation)
(documentation inverse "The inverse of a &%BinaryRelation is a relation 
in which all the tuples of the original relation are reversed.  In 
other words, one &%BinaryRelation is the inverse of another if they are 
equivalent when their arguments are swapped.")

(=>
   (inverse ?REL1 ?REL2)
   (forall (?INST1 ?INST2)
      (<=>
         (holds ?REL1 ?INST1 ?INST2)
         (holds ?REL2 ?INST2 ?INST1))))

(instance subclass BinaryPredicate)
(instance subclass PartialOrderingRelation)
(domain subclass 1 SetOrClass)
(domain subclass 2 SetOrClass)
(documentation subclass "(&%subclass ?CLASS1 ?CLASS2) means that ?CLASS1 is 
a subclass of ?CLASS2, i.e. every instance of ?CLASS1 is also an instance of 
?CLASS2.  A class may have multiple superclasses and subclasses.")

(<=> 
   (subclass ?SUBCLASS ?CLASS)
   (and
      (instance ?SUBCLASS SetOrClass)
      (instance ?CLASS SetOrClass)
      (forall (?INST)
         (=> 
            (instance ?INST ?SUBCLASS)
            (instance ?INST ?CLASS)))))

(subrelation immediateSubclass subclass)
(instance immediateSubclass AsymmetricRelation)
(instance immediateSubclass IntransitiveRelation)
(documentation immediateSubclass "A &%SetOrClass ?CLASS1 is an &%immediateSubclass 
of another &%SetOrClass ?CLASS2 just in case ?CLASS1 is a subclass of ?CLASS2 and 
there is no other subclass of ?CLASS2 such that ?CLASS1 is also a subclass of it.")

(=>
   (immediateSubclass ?CLASS1 ?CLASS2)
   (not (exists (?CLASS3)
      (and
         (subclass ?CLASS3 ?CLASS2)
         (subclass ?CLASS1 ?CLASS3)
         (not (equal ?CLASS2 ?CLASS3))
         (not (equal ?CLASS1 ?CLASS3)))))) 

(instance subrelation BinaryPredicate)
(instance subrelation PartialOrderingRelation)
(domain subrelation 1 Relation)
(domain subrelation 2 Relation)
(documentation subrelation "(&%subrelation ?REL1 ?REL2) means that 
every tuple of ?REL1 is also a tuple of ?REL2.  In other words, if 
the &%Relation ?REL1 holds for some arguments arg_1, arg_2, ... arg_n, 
then the &%Relation ?REL2 holds for the same arguments.  A consequence 
of this is that a &%Relation and its subrelations must have the same 
&%valence. In CycL, &%subrelation is called #$genlPreds.")

(=>
   (and
      (subrelation ?PRED1 ?PRED2)
      (valence ?PRED1 ?NUMBER))
   (valence ?PRED2 ?NUMBER))
   
(=>
   (and
      (subrelation ?PRED1 ?PRED2)
      (domain ?PRED2 ?NUMBER ?CLASS1))
   (domain ?PRED1 ?NUMBER ?CLASS1))

(=>
   (and
      (subrelation ?REL1 ?REL2)
      (holds ?REL1 @ROW))
   (holds ?REL2 @ROW))

(=>
   (and
      (subrelation ?PRED1 ?PRED2)
      (instance ?PRED2 ?CLASS)
      (instance ?CLASS InheritableRelation))
   (instance ?PRED1 ?CLASS))

(instance domain TernaryPredicate)
(domain domain 1 Relation)
(domain domain 2 PositiveInteger)
(domain domain 3 SetOrClass)
(documentation domain "Provides a computationally and heuristically
convenient mechanism for declaring the argument types of a given relation.  
The formula (&%domain ?REL ?INT ?CLASS) means that the ?INT'th element of each 
tuple in the relation ?REL must be an instance of ?CLASS.  Specifying argument
types is very helpful in maintaining ontologies.  Representation systems can 
use these specifications to classify terms and check integrity constraints.  
If the restriction on the argument type of a &%Relation is not captured by a 
&%SetOrClass already defined in the ontology, one can specify a &%SetOrClass 
compositionally with the functions &%UnionFn, &%IntersectionFn, etc.")

(=>
   (and
      (domain ?REL ?NUMBER ?CLASS1)
      (domain ?REL ?NUMBER ?CLASS2))
   (or
      (subclass ?CLASS1 ?CLASS2)
      (subclass ?CLASS2 ?CLASS1)))

(instance domainSubclass TernaryPredicate)
(domain domainSubclass 1 Relation)
(domain domainSubclass 2 PositiveInteger)
(domain domainSubclass 3 SetOrClass)
(documentation domainSubclass "&%Predicate used to specify argument 
type restrictions of &%Predicates.  The formula (&%domainSubclass 
?REL ?INT ?CLASS) means that the ?INT'th element of each tuple in the 
relation ?REL must be a subclass of ?CLASS.")

(=>
   (and
      (subrelation ?REL1 ?REL2)
      (domainSubclass ?REL2 ?NUMBER ?CLASS1))
   (domainSubclass ?REL1 ?NUMBER ?CLASS1))

(=>
   (and
      (domainSubclass ?REL ?NUMBER ?CLASS1)
      (domainSubclass ?REL ?NUMBER ?CLASS2))
   (or
      (subclass ?CLASS1 ?CLASS2)
      (subclass ?CLASS2 ?CLASS1)))

(instance equal BinaryPredicate)
(instance equal EquivalenceRelation)
(instance equal RelationExtendedToQuantities)
(domain equal 1 Entity)
(domain equal 2 Entity)
(documentation equal "(equal ?ENTITY1 ?ENTITY2) is true just in case 
?ENTITY1 is identical with ?ENTITY2.")

(=>
   (equal ?THING1 ?THING2)
   (forall (?ATTR)
      (<=>
         (property ?THING1 ?ATTR)
         (property ?THING2 ?ATTR))))

(=>
   (equal ?ATTR1 ?ATTR2)
   (forall (?THING)
      (<=>
         (property ?THING ?ATTR1)
         (property ?THING ?ATTR2))))

(=>
   (equal ?THING1 ?THING2)
   (forall (?CLASS)
      (<=>
         (instance ?THING1 ?CLASS)
         (instance ?THING2 ?CLASS))))

(=>
   (equal ?CLASS1 ?CLASS2)
   (forall (?THING)
      (<=>
         (instance ?THING ?CLASS1)
         (instance ?THING ?CLASS2))))

(=>
   (equal ?REL1 ?REL2)
   (forall (@ROW)
      (<=>
         (holds ?REL1 @ROW)
         (holds ?REL2 @ROW))))

(=>
   (equal (ListFn @ROW1) (ListFn @ROW2))
      (<=>
         (holds @ROW1)
         (holds @ROW2)))

(=>
   (equal ?LIST1 ?LIST2)
      (=>
         (and
            (equal ?LIST1 (ListFn @ROW1))
            (equal ?LIST2 (ListFn @ROW2)))
         (forall (?NUMBER)
            (equal (ListOrderFn (ListFn @ROW1) ?NUMBER) (ListOrderFn (ListFn @ROW2) ?NUMBER)))))
    
(instance range BinaryPredicate)
(instance range AsymmetricRelation)
(domain range 1 Function)
(domain range 2 SetOrClass)
(documentation range "Gives the range of a function.  In other words, 
(&%range ?FUNCTION ?CLASS) means that all of the values assigned by 
?FUNCTION are &%instances of ?CLASS.") 

(=>
   (and
      (range ?FUNCTION ?CLASS)
      (equal (AssignmentFn ?FUNCTION @ROW) ?VALUE))
   (instance ?VALUE ?CLASS))

(=>
   (and
      (subrelation ?REL1 ?REL2)
      (range ?REL2 ?CLASS1))
   (range ?REL1 ?CLASS1))

(=>
   (and
      (range ?REL ?CLASS1)
      (range ?REL ?CLASS2))
   (or
      (subclass ?CLASS1 ?CLASS2)
      (subclass ?CLASS2 ?CLASS1)))

(instance rangeSubclass BinaryPredicate)
(instance rangeSubclass AsymmetricRelation)
(domain rangeSubclass 1 Function)
(domainSubclass rangeSubclass 2 SetOrClass)
(documentation rangeSubclass "(&%rangeSubclass ?FUNCTION ?CLASS) means that 
all of the values assigned by ?FUNCTION are &%subclasses of ?CLASS.")

(=>
   (and
      (rangeSubclass ?FUNCTION ?CLASS)
      (equal (AssignmentFn ?FUNCTION @ROW) ?VALUE))
   (subclass ?VALUE ?CLASS))

(=>
   (and
      (subrelation ?REL1 ?REL2)
      (rangeSubclass ?REL2 ?CLASS1))
   (rangeSubclass ?REL1 ?CLASS1))

(=>
   (and
      (rangeSubclass ?REL ?CLASS1)
      (rangeSubclass ?REL ?CLASS2))
   (or
      (subclass ?CLASS1 ?CLASS2)
      (subclass ?CLASS2 ?CLASS1)))

(instance valence BinaryPredicate)
(instance valence AsymmetricRelation)
(instance valence SingleValuedRelation)
(domain valence 1 Relation)
(domain valence 2 PositiveInteger)
(documentation valence "Specifies the number of arguments that a 
relation can take.  If a relation does not have a fixed number of 
arguments, it does not have a valence and it is an instance of 
&%VariableArityRelation.  For example, &%holds is a 
&%VariableArityRelation.")

(instance documentation BinaryPredicate)
(instance documentation AsymmetricRelation)
(domain documentation 1 Entity)
(domain documentation 2 SymbolicString)
(documentation documentation "A relation between objects in the domain 
of discourse and strings of natural language text.  The domain of 
&%documentation is not constants (names), but the objects themselves.  
This means that one does not quote the names when associating them with 
their documentation.")

(instance disjoint BinaryPredicate)
(instance disjoint SymmetricRelation)
(domain disjoint 1 SetOrClass)
(domain disjoint 2 SetOrClass)
(documentation disjoint "&%Classes are &%disjoint only if they share no 
instances, i.e. just in case the result of applying &%IntersectionFn to
them is empty.")

(<=>
   (disjoint ?CLASS1 ?CLASS2)
   (and
      (instance ?CLASS1 NonNullSet)
      (instance ?CLASS2 NonNullSet)
      (forall (?INST)
         (not
            (and 
	         (instance ?INST ?CLASS1)
               (instance ?INST ?CLASS2))))))

(instance disjointRelation Predicate)
(instance disjointRelation VariableArityRelation)
(relatedInternalConcept disjointRelation disjoint)
(documentation disjointRelation "This predicate relates any number of &%Relations.  
(&%disjointRelation @ROW) means that any two relations in @ROW have no tuples in 
common.  As a consequence, the intersection of all of the relations in @ROW is the 
null set.")

(=>
   (and
      (disjointRelation @ROW)
      (inList ?REL (ListFn @ROW)))
   (instance ?REL Relation))

(=>
   (and
      (disjointRelation @ROW)
      (inList ?REL1 (ListFn @ROW))
      (inList ?REL2 (ListFn @ROW))
      (valence ?REL1 ?NUMBER))
   (valence ?REL2 ?NUMBER))

(=>
   (and
      (domain ?REL1 ?NUMBER ?CLASS1)
      (domain ?REL2 ?NUMBER ?CLASS2)
      (disjoint ?CLASS1 ?CLASS2))
   (disjointRelation ?REL1 ?REL2))

(=>
   (and
      (domainSubclass ?REL1 ?NUMBER ?CLASS1)
      (domainSubclass ?REL2 ?NUMBER ?CLASS2)
      (disjoint ?CLASS1 ?CLASS2))
   (disjointRelation ?REL1 ?REL2))

(=>
   (and
      (range ?REL1 ?CLASS1)
      (range ?REL2 ?CLASS2)
      (disjoint ?CLASS1 ?CLASS2))
   (disjointRelation ?REL1 ?REL2))

(=>
   (and
      (rangeSubclass ?REL1 ?CLASS1)
      (rangeSubclass ?REL2 ?CLASS2)
      (disjoint ?CLASS1 ?CLASS2))
   (disjointRelation ?REL1 ?REL2))

(=>
   (and
      (disjointRelation @ROW1)
      (inList ?REL1 (ListFn @ROW1))
      (inList ?REL2 (ListFn @ROW1))
      (not (equal ?REL1 ?REL2))
      (holds ?REL1 @ROW2))
   (not (holds ?REL2 @ROW2)))

(instance contraryAttribute Predicate)
(instance contraryAttribute VariableArityRelation)
(documentation contraryAttribute "A &%contraryAttribute is a set of &%Attributes 
such that something can not simultaneously have more than one of these &%Attributes.  
For example, (&%contraryAttribute &%Pliable &%Rigid) means that nothing can be both 
&%Pliable and &%Rigid.")

(=>
   (contraryAttribute @ROW)
   (=>
      (inList ?ELEMENT (ListFn @ROW))
      (instance ?ELEMENT Attribute)))

(=>
   (contraryAttribute @ROW)
   (forall (?ATTR1 ?ATTR2)
      (=>
         (and
            (equal ?ATTR1 (ListOrderFn (ListFn @ROW) ?NUMBER1))
            (equal ?ATTR2 (ListOrderFn (ListFn @ROW) ?NUMBER2))
            (not (equal ?NUMBER1 ?NUMBER2)))
         (=>
            (property ?OBJ ?ATTR1)
            (not (property ?OBJ ?ATTR2))))))

(instance exhaustiveAttribute Predicate)
(instance exhaustiveAttribute VariableArityRelation)
(domainSubclass exhaustiveAttribute 1 Attribute)
(documentation exhaustiveAttribute "This predicate relates a &%Class to a 
set of &%Attributes, and it means that the elements of this set exhaust the 
instances of the &%Class.  For example, (&%exhaustiveAttribute &%PhysicalState 
&%Solid &%Liquid &%Gas) means that there are only three instances of the class 
&%PhysicalState, viz. &%Solid, &%Liquid, and &%Gas.")

(=>
   (exhaustiveAttribute ?CLASS @ROW)
   (=>
      (inList ?ATTR (ListFn @ROW))
      (instance ?ATTR Attribute))) 

(=>
   (exhaustiveAttribute ?CLASS @ROW)
   (forall (?OBJ)
      (=>
         (instance ?ATTR1 ?CLASS)
         (exists (?ATTR2)
            (and
               (inList ?ATTR2 (ListFn @ROW))
               (equal ?ATTR1 ?ATTR2))))))

(instance exhaustiveDecomposition Predicate)
(instance exhaustiveDecomposition VariableArityRelation)
(domain exhaustiveDecomposition 1 Class)
(relatedInternalConcept exhaustiveDecomposition partition)
(documentation exhaustiveDecomposition "An &%exhaustiveDecomposition of a 
&%Class C is a set of subclasses of C such that every subclass of C either 
is an element of the set or is a subclass of an element of the set.  Note: 
this does not necessarily mean that the elements of the set are disjoint 
(see &%partition - a &%partition is a disjoint exhaustive decomposition.)")

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

(instance disjointDecomposition Predicate)
(instance disjointDecomposition VariableArityRelation)
(domain disjointDecomposition 1 Class)
(relatedInternalConcept disjointDecomposition exhaustiveDecomposition)
(relatedInternalConcept disjointDecomposition disjoint)
(documentation disjointDecomposition "A &%disjointDecomposition of a &%Class 
C is a set of subclasses of C that are mutually &%disjoint.")

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

(instance partition Predicate)
(instance partition VariableArityRelation)
(domain partition 1 Class)
(documentation partition "A &%partition of a class C is a set of 
mutually &%disjoint classes (a subclass partition) which covers C.  
Every instance of C is an instance of exactly one of the subclasses 
in the partition.")

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

(instance relatedInternalConcept BinaryPredicate)
(instance relatedInternalConcept EquivalenceRelation)
(domain relatedInternalConcept 1 Entity)
(domain relatedInternalConcept 2 Entity)
(documentation relatedInternalConcept "Means that the two arguments are 
related concepts within the SUMO, i.e. there is a significant similarity 
of meaning between them.  To indicate a meaning relation between a SUMO 
concept and a concept from another source, use the Predicate 
&%relatedExternalConcept.")

(instance relatedExternalConcept TernaryPredicate)
(domain relatedExternalConcept 1 SymbolicString)
(domain relatedExternalConcept 2 Entity)
(domain relatedExternalConcept 3 Language)
(relatedInternalConcept relatedExternalConcept relatedInternalConcept)
(documentation relatedExternalConcept "Used to signify a three-place 
relation between a concept in an external knowledge source, a concept 
in the SUMO, and the name of the other knowledge source.")

(subrelation synonymousExternalConcept relatedExternalConcept)
(disjointRelation synonymousExternalConcept subsumedExternalConcept subsumingExternalConcept)
(documentation synonymousExternalConcept "(&%synonymousExternalConcept 
?STRING ?THING ?LANGUAGE) means that the SUMO concept ?THING has the 
same meaning as ?STRING in ?LANGUAGE.")

(subrelation subsumingExternalConcept relatedExternalConcept)
(documentation subsumingExternalConcept "(&%subsumingExternalConcept 
?STRING ?THING ?LANGUAGE) means that the SUMO concept ?THING subsumes 
the meaning of ?STRING in ?LANGUAGE, i.e. the concept ?THING is broader 
in meaning than ?STRING.")

(subrelation subsumedExternalConcept relatedExternalConcept)
(documentation subsumedExternalConcept "(&%subsumedExternalConcept 
?STRING ?THING ?LANGUAGE) means that the SUMO concept ?THING is subsumed 
by the meaning of ?STRING in ?LANGUAGE, i.e. the concept ?THING is narrower 
in meaning than ?STRING.")

(instance subAttribute BinaryPredicate)
(instance subAttribute PartialOrderingRelation)
(domain subAttribute 1 Attribute)
(domain subAttribute 2 Attribute)
(disjointRelation subAttribute successorAttribute)
(documentation subAttribute "Means that the second argument can be 
ascribed to everything which has the first argument ascribed to it.")

(=>
   (subAttribute ?ATTR1 ?ATTR2)
   (forall (?OBJ)
      (=>
         (property ?OBJ ?ATTR1)
         (property ?OBJ ?ATTR2))))

(=>
   (and
      (subAttribute ?ATTR1 ?ATTR2)
      (instance ?ATTR2 ?CLASS))
   (instance ?ATTR1 ?CLASS))

(instance successorAttribute BinaryPredicate)
(instance successorAttribute AsymmetricRelation)
(domain successorAttribute 1 Attribute)
(domain successorAttribute 2 Attribute)
(documentation successorAttribute "(&%successorAttribute ?ATTR1 ?ATTR2) 
means that ?ATTR2 is the &%Attribute that comes immediately after ?ATTR1 
on the scale that they share.")

(=>
   (and
      (successorAttribute ?ATTR1 ?ATTR2)
      (holdsDuring ?TIME1 (property ?ENTITY ?ATTR2)))
   (exists (?TIME2)
      (and
         (temporalPart ?TIME2 (PastFn ?TIME1))
         (holdsDuring ?TIME2 (property ?ENTITY ?ATTR1)))))

(instance successorAttributeClosure BinaryPredicate)
(instance successorAttributeClosure TransitiveRelation)
(instance successorAttributeClosure IrreflexiveRelation)
(domain successorAttributeClosure 1 Attribute)
(domain successorAttributeClosure 2 Attribute)
(relatedInternalConcept successorAttributeClosure successorAttribute)
(documentation successorAttributeClosure "The transitive closure of 
&%successorAttribute.  (&%successorAttributeClosure ?ATTR1 ?ATTR2) means 
that there is a chain of &%successorAttribute assertions connecting 
?ATTR1 and ?ATTR2.") 

(=>
   (successorAttribute ?ATTR1 ?ATTR2)
   (successorAttributeClosure ?ATTR1 ?ATTR2))

(instance and VariableArityRelation)
(instance and LogicalOperator)
(domain and 1 Formula)
(domain and 2 Formula)
(documentation and "The truth-functional connective of conjunction.")

(instance or VariableArityRelation)
(instance or LogicalOperator)
(domain or 1 Formula)
(domain or 2 Formula)
(documentation or "The truth-functional connective of disjunction.")

(instance => BinaryPredicate)
(instance => LogicalOperator)
(domain => 1 Formula)
(domain => 2 Formula)
(documentation => "The truth-functional connective of implication.")

(instance <=> BinaryPredicate)
(instance <=> LogicalOperator)
(domain <=> 1 Formula)
(domain <=> 2 Formula)
(documentation <=> "The truth-functional connective of bi-implication.")

(instance not LogicalOperator)
(domain not 1 Formula)
(documentation not "The truth-functional connective of negation.")

(instance forall BinaryPredicate)
(instance forall LogicalOperator)
(domain forall 1 List)
(domain forall 2 Formula)
(documentation forall "The universal quantifier of predicate logic.")

(instance exists BinaryPredicate)
(instance exists LogicalOperator)
(domain exists 1 List)
(domain exists 2 Formula)
(documentation exists "The existential quantifier of predicate logic.")

(instance entails BinaryPredicate)
(instance entails LogicalOperator)
(domain entails 1 Formula)
(domain entails 2 Formula)
(documentation entails "The operator of logical entailment.  (&%entails 
?FORMULA1 ?FORMULA2) means that ?FORMULA2 can be derived from ?FORMULA1 
by means of the proof theory of SUO-KIF.")

;; The following axiom is commented out, because it is rejected by the 
;; inference engine's parser.

;;(=>
;;   (entails ?FORMULA1 ?FORMULA2)
;;   (=> ?FORMULA1 ?FORMULA2))

(instance AssignmentFn Function)
(instance AssignmentFn VariableArityRelation)
(domain AssignmentFn 1 Function)
(range AssignmentFn Entity)
(documentation AssignmentFn "If F is a function with a value for the 
objects denoted by N1,..., NK, then the term (AssignmentFn F N1 ... NK) 
denotes the value of applying F to the objects denoted by N1,..., NK.  
Otherwise, the value is undefined.")

(instance holds Predicate)
(instance holds VariableArityRelation)
(domain holds 1 Relation)
(documentation holds "(holds P N1 ... NK) is true just in case 
the tuple of objects denoted by N1,..., NK is an element of 
the &%Relation P.")

(=>
	(instance ?REL Function)
	(<=>
		(equal (AssignmentFn ?REL @ROW) ?INST)
		(holds ?REL @ROW ?INST)))

(instance PowerSetFn UnaryFunction)
(instance PowerSetFn TotalValuedRelation)
(domain PowerSetFn 1 SetOrClass)
(rangeSubclass PowerSetFn SetOrClass)
(documentation PowerSetFn "(&%PowerSetFn ?CLASS) maps the &%SetOrClass 
?CLASS to the &%SetOrClass of all &%subclasses of ?CLASS.")

;; END FILE

;; BEGIN FILE


;;;;;;;;;;;;;;;;;;;;;;;
;;   BASE ONTOLOGY   ;;
;;;;;;;;;;;;;;;;;;;;;;;

;; INCLUDES 'STRUCTURAL ONTOLOGY'

;; The following hierarchy incorporates content from Sowa, Russell & Norvig, 
;; and the top-level ontology from ITBM-CNR. 

(partition Entity Physical Abstract)
(documentation Entity "The universal class of individuals.  This is the root 
node of the ontology.")

(instance ?THING Entity)

(exists (?THING) (instance ?THING Entity))

(<=> 
	(instance ?CLASS Class)
      (subclass ?CLASS Entity))

(subclass Physical Entity)
(partition Physical Object Process)
(documentation Physical "An entity that has a location in space-time.  
Note that locations are themselves understood to have a location in 
space-time.")

(<=> 
	(instance ?PHYS Physical)
	(exists (?LOC ?TIME)
     		(and 
			(located ?PHYS ?LOC)
                  (time ?PHYS ?TIME))))

(subclass Object Physical)
(documentation Object "Corresponds roughly to the class of ordinary 
objects.  Examples include normal physical objects, geographical regions, 
and locations of &%Processes, the complement of &%Objects in the &%Physical 
class.  In a 4D ontology, an &%Object is something whose spatiotemporal 
extent is thought of as dividing into spatial parts roughly parallel to the 
time-axis.")

(subclass SelfConnectedObject Object)
(documentation SelfConnectedObject "A &%SelfConnectedObject is any 
&%Object that does not consist of two or more disconnected parts.")

(instance FrontFn SpatialRelation)
(instance FrontFn PartialValuedRelation)
(instance FrontFn UnaryFunction)
(instance FrontFn AsymmetricRelation)
(instance FrontFn IrreflexiveRelation)
(domain FrontFn 1 SelfConnectedObject)
(range FrontFn SelfConnectedObject)
(documentation FrontFn "A &%Function that maps an &%Object to the side 
that generally receives the most attention or that typically faces the 
direction in which the &%Object moves.  Note that this is a partial 
function, since some &%Objects do not have sides, e.g. apples and 
spheres.  Note too that the &%range of this &%Function is indefinite in 
much the way that &%ImmediateFutureFn and &%ImmediatePastFn are indefinite.  
Although this indefiniteness is undesirable from a theoretical standpoint, 
it does not have significant practical implications, since there is 
widespread intersubjective agreement about the most common cases.")

(=>
   (instance ?OBJ SelfConnectedObject)
   (side (FrontFn ?OBJ) ?OBJ))

(instance BackFn SpatialRelation)
(instance BackFn PartialValuedRelation)
(instance BackFn UnaryFunction)
(instance BackFn AsymmetricRelation)
(instance BackFn IrreflexiveRelation)
(domain BackFn 1 SelfConnectedObject)
(range BackFn SelfConnectedObject)
(documentation BackFn "A &%Function that maps an &%Object to the side 
that is opposite the &%FrontFn of the &%Object.  Note that this is a 
partial function, since some &%Objects do not have sides, e.g. apples 
and spheres.  Note too that the &%range of this &%Function is indefinite in 
much the way that &%ImmediateFutureFn and &%ImmediatePastFn are indefinite.  
Although this indefiniteness is undesirable from a theoretical standpoint, 
it does not have significant practical implications, since there is 
widespread intersubjective agreement about the most common cases.")

(=>
   (instance ?OBJ SelfConnectedObject)
   (side (BackFn ?OBJ) ?OBJ))

(instance part SpatialRelation)
(instance part PartialOrderingRelation)
(domain part 1 Object)
(domain part 2 Object)
(documentation part "The basic mereological relation.  All other 
mereological relations are defined in terms of this one.  
(&%part ?PART ?WHOLE) simply means that the &%Object ?PART is part
of the &%Object ?WHOLE.  Note that, since &%part is a 
&%ReflexiveRelation, every &%Object is a part of itself.")

(instance properPart AsymmetricRelation)
(instance properPart TransitiveRelation)
(subrelation properPart part)
(documentation properPart "(&%properPart ?OBJ1 ?OBJ2) means that 
?OBJ1 is a part of ?OBJ2 other than ?OBJ2 itself. This is a 
&%TransitiveRelation and &%AsymmetricRelation (hence an 
&%IrreflexiveRelation).")

(<=> 
   (properPart ?OBJ1 ?OBJ2)
      (and
	   (part ?OBJ1 ?OBJ2)
	   (not
	      (part ?OBJ2 ?OBJ1))))

(subrelation piece part)
(domain piece 1 Substance)
(domain piece 2 Substance)
(documentation piece "A specialized common sense notion of part for 
arbitrary parts of &%Substances.  Quasi-synonyms are: chunk, hunk, bit, 
etc.  Compare &%component, the other subrelation of &%part.")

(=>
   (piece ?SUBSTANCE1 ?SUBSTANCE2)
   (forall (?CLASS)
      (=>
         (instance ?SUBSTANCE1 ?CLASS)
         (instance ?SUBSTANCE2 ?CLASS))))

(subrelation component part)
(domain component 1 CorpuscularObject)
(domain component 2 CorpuscularObject)
(documentation component "A specialized common sense notion of part 
for heterogeneous parts of complexes. (&%component ?COMPONENT ?WHOLE) 
means that ?COMPONENT is a component of ?WHOLE. Examples of component 
include the doors and walls of a house, the states or provinces of a 
country, or the limbs and organs of an animal.  Compare &%piece, which 
is also a subrelation of &%part.")

(instance material BinaryPredicate)
(domainSubclass material 1 Substance)
(domain material 2 CorpuscularObject)
(documentation material "(&%material ?SUBSTANCE ?OBJECT) means that 
?OBJECT is structurally made up in part of ?SUBSTANCE. This relation 
encompasses the concepts of 'composed of', 'made of', and 'formed of'.  
For example, plastic is a &%material of my computer monitor.  Compare 
&%part and its subrelations, viz &%component and &%piece.")

(subrelation contains partlyLocated)
(instance contains SpatialRelation)
(instance contains AsymmetricRelation)
(disjointRelation contains part)
(domain contains 1 SelfConnectedObject)
(domain contains 2 Object)
(documentation contains "The relation of spatial containment for two 
separable objects.  When the two objects are not separable (e.g. an 
automobile and one of its seats), the relation of &%part should be used.  
(&%contains ?OBJ1 ?OBJ2) means that the &%SelfConnectedObject ?OBJ1 has 
a space (i.e. a &%Hole) which is at least partially filled by ?OBJ2.")

(<=>
   (contains ?OBJ1 ?OBJ2)
   (exists (?HOLE)
      (and
         (hole ?HOLE ?OBJ1)
         (properlyFills ?OBJ2 ?HOLE))))

(subclass Substance SelfConnectedObject)
(documentation Substance "An &%Object in which every part is similar to 
every other in every relevant respect.  More precisely, something is a 
&%Substance when it has only arbitrary pieces as parts - any parts have 
properties which are similar to those of the whole.  Note that a &%Substance 
may nonetheless have physical properties that vary.  For example, the 
temperature, chemical constitution, density, etc. may change from one part 
to another.  An example would be a body of water.")

(=>
   (and
      (subclass ?OBJECTTYPE Substance)
      (instance ?OBJECT ?OBJECTTYPE)
      (part ?PART ?OBJECT))
   (instance ?PART ?OBJECTTYPE))

(=>
   (and
      (instance ?OBJ Substance)
      (attribute ?OBJ ?ATTR)
      (part ?PART ?OBJ))
   (attribute ?PART ?ATTR))

(subclass PureSubstance Substance) 
(partition PureSubstance CompoundSubstance ElementalSubstance) 
(documentation PureSubstance "The &%Class of &%Substances with constant 
composition.  A &%PureSubstance can be either an element (&%ElementalSubstance) 
or a compound of elements (&%CompoundSubstance).  Examples: Table salt 
(sodium chloride, NaCl), sugar (sucrose, C_{12}H_{22}O_{11}), water (H_2O), 
iron (Fe), copper (Cu), and oxygen (O_2).") 

(subclass ElementalSubstance PureSubstance) 
(documentation ElementalSubstance "The &%Class of &%PureSubstances that 
cannot be separated into two or more &%Substances by ordinary chemical 
(or physical) means. This excludes nuclear reactions. &%ElementalSubstances 
are composed of only one kind of atom. Examples: Iron (Fe), copper (Cu), 
and oxygen (O_2).  &%ElementalSubstances are the simplest 
&%PureSubstances.")

(subclass Metal ElementalSubstance) 
(documentation Metal "A &%Metal is an &%ElementalSubstance that conducts heat 
and electricity, is shiny and reflects many colors of light, and can be hammered 
into sheets or drawn into wire.  About 80% of the known chemical elements 
(&%ElementalSubstances) are metals.")

(subclass Atom ElementalSubstance)
(documentation Atom "An extremely small unit of matter that retains its 
identity in Chemical reactions.  It consists of an &%AtomicNucleus and 
&%Electrons surrounding the &%AtomicNucleus.")

(=>
   (instance ?ATOM Atom)
   (exists (?PROTON ?ELECTRON)
      (and
         (component ?PROTON ?ATOM)
	   (component ?ELECTRON ?ATOM)
         (instance ?PROTON Proton)
         (instance ?ELECTRON Electron))))

(=>
   (instance ?ATOM Atom)
   (forall (?NUCLEUS1 ?NUCLEUS2)
      (=>
         (and
            (component ?NUCLEUS1 ?ATOM)
	      (component ?NUCLEUS2 ?ATOM)
            (instance ?NUCLEUS1 AtomicNucleus)
            (instance ?NUCLEUS2 AtomicNucleus))
	   (equal ?NUCLEUS1 ?NUCLEUS2))))

(subclass SubatomicParticle ElementalSubstance)
(documentation SubatomicParticle "The class of &%ElementalSubstances that 
are smaller than &%Atoms and compose &%Atoms.")

(=>
   (instance ?PARTICLE SubatomicParticle)
   (exists (?ATOM)
      (and
         (instance ?ATOM Atom)
         (part ?PARTICLE ?ATOM))))

(subclass AtomicNucleus SubatomicParticle)
(documentation AtomicNucleus "The core of the &%Atom.  It is composed of 
&%Protons and &%Neutrons.")

(=>
   (instance ?NUCLEUS AtomicNucleus)
   (exists (?NEUTRON ?PROTON)
      (and
         (component ?NEUTRON ?NUCLEUS)
	   (component ?PROTON ?NUCLEUS)
         (instance ?NEUTRON Neutron)
         (instance ?PROTON Proton))))

(subclass Electron SubatomicParticle)
(documentation Electron "&%SubatomicParticles that surround the 
&%AtomicNucleus.  They have a negative charge.")

(subclass Proton SubatomicParticle)
(documentation Proton "Components of the &%AtomicNucleus.  They have a 
positive charge.")

(subclass Neutron SubatomicParticle)
(documentation Neutron "Components of the &%AtomicNucleus.  They have no 
charge.")

(subclass CompoundSubstance PureSubstance) 
(documentation CompoundSubstance "The &%Class of &%Substances that contain 
two or more elements (&%ElementalSubstances), in definite proportion by weight. 
The composition of a pure compound will be invariant, regardless of the method 
of preparation. Compounds are composed of more than one kind of atom (element). 
The term molecule is often used for the smallest unit of a compound that still 
retains all of the properties of the compound.  Examples: Table salt (sodium 
chloride, NaCl), sugar (sucrose, C_{12}H_{22}O_{11}), and water (H_2O). ") 

(subclass Mixture Substance) 
(documentation Mixture "A &%Mixture is two or more &%PureSubstances, 
combined in varying proportions - each retaining its own specific properties. 
The components of a &%Mixture can be separated by physical means, i.e. without 
the making and breaking of chemical bonds. Examples: Air, table salt thoroughly 
dissolved in water, milk, wood, and concrete. ") 

(=> 
   (instance ?MIXTURE Mixture)
   (exists (?PURE1 ?PURE2)
      (and 
         (instance ?PURE1 PureSubstance)
         (instance ?PURE2 PureSubstance)
         (not (equal ?PURE1 ?PURE2))
         (part ?PURE1 ?MIXTURE)
         (part ?PURE2 ?MIXTURE))))

(=>
   (and
      (instance ?MIXTURE Mixture)
      (part ?SUBSTANCE ?MIXTURE)
      (not (instance ?SUBSTANCE Mixture)))
   (instance ?SUBSTANCE PureSubstance))

(subclass Solution Mixture) 
(documentation Solution "A liquid mixture. The most abundant component in 
a solution is called the solvent. Other components are called solutes. 
A solution, though homogeneous, may nonetheless have variable composition. 
Any amount of salt, up to a maximum limit, can be dissolved in a given 
amount of water.") 

(subclass CorpuscularObject SelfConnectedObject)
(disjoint CorpuscularObject Substance)
(documentation CorpuscularObject "A &%SelfConnectedObject whose parts have 
properties that are not shared by the whole.")

(=>
   (instance ?OBJ CorpuscularObject)
   (exists (?SUBSTANCE1 ?SUBSTANCE2)
      (and
         (subclass ?SUBSTANCE1 Substance)
         (subclass ?SUBSTANCE2 Substance)
         (material ?SUBSTANCE1 ?OBJ)
         (material ?SUBSTANCE2 ?OBJ)
         (not (equal ?SUBSTANCE1 ?SUBSTANCE2)))))

(subclass Region Object)
(documentation Region "A topographic location.  &%Regions encompass 
surfaces of &%Objects, imaginary places, and &%GeographicAreas.  Note 
that a &%Region is the only kind of &%Object which can be located at 
itself.  Note too that &%Region is not a subclass of &%SelfConnectedObject, 
because some &%Regions, e.g. archipelagos, have &%parts which are not 
&%connected with one another.")

(=>
   (instance ?REGION Region)
   (exists (?PHYS)
      (located ?PHYS ?REGION)))

(subclass Collection Object)
(disjoint Collection SelfConnectedObject)
(documentation Collection "Collections have &%members like &%Classes, but, 
unlike &%Classes, they have a position in space-time and &%members can be 
added and subtracted without thereby changing the identity of the 
&%Collection.  Some examples are toolkits, football teams, and flocks 
of sheep.")

(=>
   (instance ?COLL Collection)
   (exists (?OBJ)
	(member ?OBJ ?COLL)))

(subrelation member part)
(instance member AsymmetricRelation)
(instance member IntransitiveRelation)
(domain member 1 SelfConnectedObject)
(domain member 2 Collection)
(relatedInternalConcept member instance)
(relatedInternalConcept member element)
(documentation member "A specialized common sense notion of part for 
uniform parts of &%Collections.  For example, each sheep in a flock of 
sheep would have the relationship of member to the flock.")

(instance subCollection BinaryPredicate)
(instance subCollection PartialOrderingRelation)
(domain subCollection 1 Collection)
(domain subCollection 2 Collection)
(documentation subCollection "(&%subCollection ?COLL1 ?COLL2) means that 
the &%Collection ?COLL1 is a proper part of the &%Collection ?COLL2.")

(<=>
   (subCollection ?COLL1 ?COLL2)
   (and
      (instance ?COLL1 Collection)
      (instance ?COLL2 Collection)
      (forall (?MEMBER)
         (=>
            (member ?MEMBER ?COLL1)
            (member ?MEMBER ?COLL2)))))

(subclass ContentBearingObject CorpuscularObject)
(relatedInternalConcept ContentBearingObject containsInformation)
(documentation ContentBearingObject "Any &%SelfConnectedObject that expresses 
information.")

(subclass SymbolicString ContentBearingObject)
(documentation SymbolicString "The &%Class of alphanumeric sequences.")

(subclass Character SymbolicString)
(documentation Character "An element of an alphabet, a set of numerals, etc.  
Note that a &%Character may or may not be part of a &%Language.  &%Character 
is a subclass of &%SymbolicString, because every instance of &%Character is 
an alphanumeric sequence consisting of a single element.")

(=>
    (instance ?STRING SymbolicString)
    (exists (?PART)
        (and
            (part ?PART ?STRING)
            (instance ?PART Character)))) 

(instance containsInformation BinaryPredicate)
(instance containsInformation AsymmetricRelation)
(subrelation containsInformation represents)
(domain containsInformation 1 ContentBearingObject)
(domain containsInformation 2 Proposition)
(documentation containsInformation "A subrelation of &%represents.  This 
predicate relates a &%ContentBearingObject to the &%Proposition that is 
expressed by the &%ContentBearingObject. Examples include the relationships 
between a physical novel and its story and between a printed score and its 
musical content.")

(subclass Icon ContentBearingObject)
(documentation Icon "This is the subclass of &%ContentBearingObjects 
which are not part of a &%Language and which have some sort of similarity 
with the &%Objects that they represent.  This &%Class would include symbolic 
roadway signs, representational art works, photographs, etc.")

(subclass MotionPicture Text)
(documentation MotionPicture "A &%ContentBearingObject which depicts motion 
(and which may have an audio or text component as well).  This &%Class covers 
films, videos, etc.")

(subclass LinguisticExpression ContentBearingObject)
(disjoint LinguisticExpression Icon)
(documentation LinguisticExpression "This is the subclass of 
&%ContentBearingObjects which are language-related.  Note that this &%Class 
encompasses both &%Language and the the elements of &%Languages, 
e.g. &%Words.")

(subclass Language LinguisticExpression)
(disjointDecomposition Language AnimalLanguage HumanLanguage ComputerLanguage)
(documentation Language "A system of signs for expressing thought.  The 
system can be either natural or artificial, i.e. something that emerges 
gradually as a cultural artifact or something that is intentionally created 
by a person or group of people.")

(subclass AnimalLanguage Language)
(documentation AnimalLanguage "The &%subclass of &%Languages used by 
&%Animals other than &%Humans.")

(=>
   (and
      (instance ?LANG AnimalLanguage)
      (agent ?PROC ?AGENT)
      (instrument ?PROC ?LANG))
   (and
      (instance ?AGENT Animal)
      (not (instance ?AGENT Human))))

(subclass ArtificialLanguage Language)
(documentation ArtificialLanguage "The &%subclass of &%Languages that are 
designed by &%Humans.")

(subclass ComputerLanguage ArtificialLanguage)
(documentation ComputerLanguage "The class of &%Languages designed for 
and interpreted by a computer.")

(=>
   (and
      (instance ?LANG ComputerLanguage)
      (agent ?PROC ?AGENT)
      (instrument ?PROC ?LANG))
   (instance ?AGENT Machine))

(subclass HumanLanguage Language)
(partition HumanLanguage NaturalLanguage ConstructedLanguage)
(partition HumanLanguage SpokenHumanLanguage ManualHumanLanguage)
(documentation HumanLanguage "The &%subclass of &%Languages used by 
&%Humans.")

(=>
   (and
      (instance ?LANG HumanLanguage)
      (agent ?PROC ?AGENT)
      (instrument ?PROC ?LANG))
   (instance ?AGENT Human))

(subclass ConstructedLanguage HumanLanguage)
(subclass ConstructedLanguage ArtificialLanguage)
(documentation ConstructedLanguage "An &%ConstructedLanguage is a 
&%HumanLanguage that did not evolve spontaneously within a language
community, but rather had its core grammar and vocabulary invented by 
one or more language experts, often with an aim to produce a more 
grammatically regular language than any language that has evolved 
naturally.  This &%Class includes languages like Esperanto that were 
created to facilitate international communication")

(=>
   (instance ?LANG ConstructedLanguage)
   (exists (?PLAN)
      (and
         (instance ?PLAN Planning)
         (result ?PLAN ?LANG))))

(subclass NaturalLanguage HumanLanguage)
(documentation NaturalLanguage "The &%subclass of &%HumanLanguages which 
are not designed and which evolve from generation to generation.  This 
&%Class includes all of the national languages, e.g. English, Spanish, 
Japanese, etc.  Note that this class includes dialects of natural 
languages.")

(subclass ManualHumanLanguage HumanLanguage)
(documentation ManualHumanLanguage "A &%ManualHumanLanguage is a
&%HumanLanguage which has as its medium gestures and movement, such 
as the shape, position, and movement of the hands.")

(subclass SpokenHumanLanguage HumanLanguage)
(documentation SpokenHumanLanguage "A &%SpokenHumanLanguage is a
&%HumanLanguage which has as its medium the human voice. It can also 
berepresented visually through writing, although not all 
&%SpokenHumanLanguages have a codified written form.")

(subclass Word LinguisticExpression)
(documentation Word "A term of a &%Language that represents a concept.")

(subclass Formula Sentence)
(documentation Formula "A syntactically well-formed formula in the 
SUO-KIF knowledge representation language.")

;; The following ground facts incorporate the 'Agent' hierarchy from the 
;; corresponding ontology on the Ontolingua server.  It also includes 
;; predicates defined in the ITBM-CNR ontology "Actors".

(subclass Agent Object)
(documentation Agent "Something or someone that can act on its own and 
produce changes in the world.")

(<=>
	(instance ?AGENT Agent)
	(exists (?PROC)
		(agent ?PROC ?AGENT)))

(subclass SentientAgent Agent)
(documentation SentientAgent "An &%Agent that has rights but may or may 
not have responsibilities and the ability to reason.  If the latter are 
present, then the &%Agent is also an instance of &%CognitiveAgent.  
Domesticated animals are an example of &%SentientAgents that are not 
also &%CognitiveAgents.")

(subclass CognitiveAgent SentientAgent)
(documentation CognitiveAgent "A &%SentientAgent with responsibilities 
and the ability to reason, deliberate, make plans, etc.  This is 
essentially the legal/ethical notion of a person.  Note that, although 
&%Human is a subclass of &%CognitiveAgent, there may be instances of 
&%CognitiveAgent which are not also instances of &%Human.  For example, 
chimpanzees, gorillas, dolphins, whales, and some extraterrestrials 
(if they exist) may be &%CognitiveAgents.")

(instance leader BinaryPredicate)
(instance leader AsymmetricRelation)
(instance leader SingleValuedRelation)
(domain leader 2 Agent)
(domain leader 1 CognitiveAgent)
(documentation leader "(&%leader ?ORGANIZATION ?PERSON)
means that the leader of ?ORGANIZATION is ?PERSON.")

(subclass Process Physical)
(documentation Process "Intuitively, the class of things that happen 
and have temporal parts or stages.  Examples include extended events 
like a football match or a race, actions like &%Pursuing and &%Reading, 
and biological processes. The formal definition is: anything that lasts 
for a time but is not an &%Object.  Note that a &%Process may have 
participants 'inside' it which are &%Objects, such as the players 
in a football match.  In a 4D ontology, a &%Process is something whose 
spatiotemporal extent is thought of as dividing into temporal stages 
roughly perpendicular to the time-axis.")

(subclass DualObjectProcess Process)
(documentation DualObjectProcess "Any &%Process that requires two, 
nonidentical &%patients.")

(=>
   (instance ?PROCESS DualObjectProcess)
   (exists (?OBJ1 ?OBJ2)
      (and
         (patient ?PROCESS ?OBJ1)
         (patient ?PROCESS ?OBJ2)
         (not (equal ?OBJ1 ?OBJ2)))))
    
(subclass Abstract Entity)
(disjointDecomposition Abstract Quantity Attribute SetOrClass Relation Proposition Graph GraphElement)
(documentation Abstract "Properties or qualities as distinguished from any 
particular embodiment of the properties/qualities in a physical medium.  
Instances of Abstract can be said to exist in the same sense as mathematical 
objects such as sets and relations, but they cannot exist at a particular 
place and time without some physical encoding or embodiment.")

;; Something is Abstract just in case it has neither a spatial nor temporal 
;; location.

(<=> 
   (instance ?ABS Abstract)
   (not 
      (exists (?POINT) 
         (or 
	      (located ?ABS ?POINT)
            (time ?ABS ?POINT)))))

(subclass Quantity Abstract)
(documentation Quantity "Any specification of how many or how much of 
something there is.  Accordingly, there are two subclasses of &%Quantity:  
&%Number (how many) and &%PhysicalQuantity (how much).")

(subclass Attribute Abstract)
(partition Attribute InternalAttribute RelationalAttribute)
(documentation Attribute "Qualities which we cannot or choose not to 
reify into subclasses of &%Object.")

(instance property BinaryPredicate)
(domain property 1 Entity)
(domain property 2 Attribute)
(documentation property "This &%Predicate holds between an instance of 
&%Entity and an instance of &%Attribute.  (property ?ENTITY ?ATTR) 
means that ?ENTITY has the &%Attribute ?ATTR.")

(instance attribute AsymmetricRelation)
(instance attribute IrreflexiveRelation)
(subrelation attribute property)
(domain attribute 1 Object)
(documentation attribute "(&%attribute ?OBJECT ?PROPERTY) means that 
?PROPERTY is a &%Attribute of ?OBJECT.  For example, 
(&%attribute &%MyLittleRedWagon &%Red).")

(instance manner AsymmetricRelation)
(instance manner IrreflexiveRelation)
(subrelation manner property)
(domain manner 1 Process)
(disjointRelation manner attribute)
(documentation manner "(&%manner ?PROCESS ?MANNER) means that the 
&%Process ?PROCESS is qualified by the &%Attribute ?MANNER.  The &%Attributes 
of &%Processes are usually denoted by adverbs and include things like the 
speed of the wind, the style of a dance, or the intensity of a sports 
competition.")

(instance AbstractionFn UnaryFunction)
(instance AbstractionFn PartialValuedRelation)
(domain AbstractionFn 1 Class)
(range AbstractionFn Attribute)
(documentation AbstractionFn "A &%UnaryFunction that maps a &%Class into 
the instance of &%Attribute that specifies the condition(s) for membership 
in the &%Class.")

(<=>
   (equal (AbstractionFn ?CLASS) ?ATTR)
   (forall (?INST)
      (<=>
         (instance ?INST ?CLASS)
         (property ?INST ?ATTR))))

(instance ExtensionFn UnaryFunction)
(instance ExtensionFn PartialValuedRelation)
(domain ExtensionFn 1 Attribute)
(range ExtensionFn Class)
(documentation ExtensionFn "A &%UnaryFunction that maps an &%Attribute 
into the &%Class whose condition for membership is the &%Attribute.")

(<=>
   (equal (ExtensionFn ?ATTRIBUTE) ?CLASS)
   (equal (AbstractionFn ?CLASS) ?ATTRIBUTE))

(subclass InternalAttribute Attribute)
(documentation InternalAttribute "Any &%Attribute of an &%Entity that is an 
internal property of the &%Entity, e.g. its shape, its color, its fragility, 
etc.")

(subclass RelationalAttribute Attribute)
(documentation RelationalAttribute "Any &%Attribute that an &%Entity has by 
virtue of a relationship that it bears to another &%Entity or set of &%Entities, 
e.g. &%SocialRoles and &%PositionalAttributes.") 

;; The following formulas incorporate the Number hierarchy from the 
;; ontology 'kif-numbers' on the Ontolingua server.

(subclass Number Quantity)
(partition Number RealNumber ImaginaryNumber ComplexNumber)
(documentation Number "A measure of how many things there are, or how
much there is, of a certain kind.  &%Numbers are subclassed into 
&%RealNumber, &%ComplexNumber, and &%ImaginaryNumber.")

(instance lessThan BinaryPredicate)
(instance lessThan TransitiveRelation)
(instance lessThan IrreflexiveRelation)
(instance lessThan RelationExtendedToQuantities)
(trichotomizingOn lessThan RealNumber)
(domain lessThan 1 Quantity)
(domain lessThan 2 Quantity)
(documentation lessThan "(&%lessThan ?NUMBER1 ?NUMBER2) is true just 
in case the &%Quantity ?NUMBER1 is less than the &%Quantity ?NUMBER2.")

(instance greaterThan BinaryPredicate)
(instance greaterThan TransitiveRelation)
(instance greaterThan IrreflexiveRelation)
(instance greaterThan RelationExtendedToQuantities)
(trichotomizingOn greaterThan RealNumber)
(domain greaterThan 1 Quantity)
(domain greaterThan 2 Quantity)
(inverse greaterThan lessThan)
(documentation greaterThan "(&%greaterThan ?NUMBER1 ?NUMBER2) is true 
just in case the &%Quantity ?NUMBER1 is greater than the &%Quantity 
?NUMBER2.")

(instance lessThanOrEqualTo BinaryPredicate)
(instance lessThanOrEqualTo PartialOrderingRelation)
(instance lessThanOrEqualTo RelationExtendedToQuantities)
(trichotomizingOn lessThanOrEqualTo RealNumber)
(domain lessThanOrEqualTo 1 Quantity)
(domain lessThanOrEqualTo 2 Quantity)
(documentation lessThanOrEqualTo "(&%lessThanOrEqualTo ?NUMBER1 ?NUMBER2) 
is true just in case the &%Quantity ?NUMBER1 is less than or equal to 
the &%Quantity ?NUMBER2.")

(<=>
	(lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
	(or
		(equal ?NUMBER1 ?NUMBER2)
		(lessThan ?NUMBER1 ?NUMBER2)))

(instance greaterThanOrEqualTo BinaryPredicate)
(instance greaterThanOrEqualTo PartialOrderingRelation)
(instance greaterThanOrEqualTo RelationExtendedToQuantities)
(trichotomizingOn greaterThanOrEqualTo RealNumber)
(domain greaterThanOrEqualTo 1 Quantity)
(domain greaterThanOrEqualTo 2 Quantity)
(inverse greaterThanOrEqualTo lessThanOrEqualTo)
(documentation greaterThanOrEqualTo "(&%greaterThanOrEqualTo ?NUMBER1 
?NUMBER2) is true just in case the &%Quantity ?NUMBER1 is greater 
than the &%Quantity ?NUMBER2.")

(<=>
	(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2)
	(or
		(equal ?NUMBER1 ?NUMBER2)
		(greaterThan ?NUMBER1 ?NUMBER2)))

(subclass RealNumber Number)
(partition RealNumber NegativeRealNumber NonnegativeRealNumber)
(partition RealNumber RationalNumber IrrationalNumber)
(documentation RealNumber "Any &%Number that can be expressed as a 
(possibly infinite) decimal, i.e. any &%Number that has a position 
on the number line.")

(subclass ImaginaryNumber Number) 
(documentation ImaginaryNumber "Any &%Number that is the result of 
multiplying a &%RealNumber by the square root of -1.")

(=>
   (instance ?NUMBER ImaginaryNumber)
   (exists (?REAL)
      (and
         (instance ?REAL RealNumber)
         (equal ?NUMBER (MultiplicationFn ?REAL (SquareRootFn -1))))))

(subclass RationalNumber RealNumber)
(documentation RationalNumber "Any &%RealNumber that is the product of 
dividing two &%Integers.")

(subclass IrrationalNumber RealNumber)
(documentation IrrationalNumber "Any &%RealNumber that is not also a 
&%RationalNumber.")

(subclass NonnegativeRealNumber RealNumber)
(documentation NonnegativeRealNumber "A &%RealNumber that is greater than 
or equal to zero.")

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

(subclass PositiveRealNumber NonnegativeRealNumber)
(documentation PositiveRealNumber "A &%RealNumber that is greater than 
zero.")

(<=>
   (instance ?NUMBER PositiveRealNumber)
   (and
      (greaterThan ?NUMBER 0)
      (instance ?NUMBER RealNumber)))

(subclass NegativeRealNumber RealNumber)
(documentation NegativeRealNumber "A &%RealNumber that is less than 
zero.")

(<=>
   (instance ?NUMBER NegativeRealNumber)
   (and
      (lessThan ?NUMBER 0)
      (instance ?NUMBER RealNumber)))

(subclass Integer RationalNumber)
(partition Integer OddInteger EvenInteger)
(partition Integer NegativeInteger NonnegativeInteger)
(documentation Integer "A negative or nonnegative whole number.")

(subclass EvenInteger Integer)
(documentation EvenInteger "An &%Integer that is evenly divisible 
by 2.")

(subclass OddInteger Integer)
(documentation OddInteger "An &%Integer that is not evenly divisible 
by 2.")

(subclass PrimeNumber Integer)
(documentation PrimeNumber "An &%Integer that is evenly divisible only 
by itself and 1.")

(subclass NonnegativeInteger Integer)
(subclass NonnegativeInteger NonnegativeRealNumber)
(documentation NonnegativeInteger "An &%Integer that is greater than 
or equal to zero.")

(subclass NegativeInteger Integer)
(subclass NegativeInteger NegativeRealNumber)
(documentation NegativeInteger "An &%Integer that is less than zero.")

(subclass PositiveInteger NonnegativeInteger)
(subclass PositiveInteger PositiveRealNumber)
(documentation PositiveInteger "An &%Integer that is greater than zero.")

(subclass BinaryNumber RealNumber)
(documentation BinaryNumber "Elements from the number system with base 2.  
Every &%BinaryNumber is expressed as a sequence of the digits 1 and 0.")

(subclass ComplexNumber Number)
(disjoint ComplexNumber RealNumber)
(documentation ComplexNumber "A &%Number that has the form: x + yi, where x 
and y are &%RealNumbers and i is the square root of -1.")

(=>
   (instance ?NUMBER ComplexNumber)
   (exists (?REAL1 ?REAL2)
      (and
         (instance ?REAL1 RealNumber)
         (instance ?REAL2 RealNumber)
         (equal ?NUMBER (AdditionFn ?REAL1 (MultiplicationFn ?REAL2 (SquareRootFn -1)))))))

(subclass PhysicalQuantity Quantity)
(partition PhysicalQuantity ConstantQuantity FunctionQuantity)
(documentation PhysicalQuantity "&%A PhysicalQuantity is a measure of 
some quantifiable aspect of the modeled world, such as 'the earth's 
diameter' (a constant length) and 'the stress in a loaded deformable 
solid' (a measure of stress, which is a function of three spatial 
coordinates).  All &%PhysicalQuantities are either &%ConstantQuantities 
or &%FunctionQuantities.  Instances of &%ConstantQuantity are dependent 
on a &%UnitOfMeasure, while instances of &%FunctionQuantity are 
&%Functions that map instances of &%ConstantQuantity to other instances 
of &%ConstantQuantity (e.g., &%TimeDependentQuantities are 
&%FunctionQuantities).  Although the name and definition of 
&%PhysicalQuantity is borrowed from physics, &%PhysicalQuantities need 
not be material.  Aside from the dimensions of length, time, velocity, 
etc., nonphysical dimensions such as currency are also possible.  
Accordingly, amounts of money would be instances of &%PhysicalQuantity.  
&%PhysicalQuantities are distinguished from &%Numbers by the fact that 
the former are associated with a dimension of measurement.")

(subclass ConstantQuantity PhysicalQuantity)
(documentation ConstantQuantity "A &%ConstantQuantity is a 
&%PhysicalQuantity which has a constant value, e.g. 3 meters and 5 hours.  
The magnitude (see &%MagnitudeFn) of every &%ConstantQuantity is a 
&%RealNumber.  &%ConstantQuantities are distinguished from 
&%FunctionQuantities, which map &%ConstantQuantities to other 
&%ConstantQuantities.  All &%ConstantQuantites are expressed with the 
&%BinaryFunction &%MeasureFn, which takes a &%Number and a &%UnitOfMeasure 
as arguments.  For example, 3 &%Meters can be expressed as (&%MeasureFn 3 
&%Meter).  &%ConstantQuantities form a partial order (see 
&%PartialOrderingRelation) with the &%lessThan relation, since &%lessThan 
is a &%RelationExtendedToQuantities and &%lessThan is defined over the 
&%RealNumbers.  The &%lessThan relation is not a total order (see 
&%TotalOrderingRelation) over the class &%ConstantQuantity since elements 
of some subclasses of &%ConstantQuantity (such as length quantities) 
are incomparable to elements of other subclasses of &%ConstantQuantity 
(such as mass quantities).")

(subclass TimeMeasure ConstantQuantity)
(documentation TimeMeasure "The class of temporal durations (instances 
of &%TimeDuration) and positions of &%TimePoints and &%TimeIntervals along 
the universal timeline (instances of &%TimePosition).")

(subclass TimeDuration TimeMeasure)
(documentation TimeDuration "Any measure of length of time, 
with or without respect to the universal timeline.")

(subclass TimePosition TimeMeasure)
(partition TimePosition TimeInterval TimePoint)
(documentation TimePosition "Any &%TimePoint or &%TimeInterval 
along the universal timeline from &%NegativeInfinity to 
&%PositiveInfinity.")

(subclass TimeInterval TimePosition)
(documentation TimeInterval "An interval of time.  Note that a 
&%TimeInterval has both an extent and a location on the universal 
timeline.  Note too that a &%TimeInterval has no gaps, i.e. this 
class contains only convex time intervals.")

(subclass TimePoint TimePosition)
(documentation TimePoint "An extensionless point on the universal timeline. 
The &%TimePoints at which &%Processes occur can be known with various 
degrees of precision and approximation, but conceptually &%TimePoints are 
point-like and not interval-like.  That is, it doesn't make sense to talk 
about how long a &%TimePoint lasts.")

(subclass FunctionQuantity PhysicalQuantity)
(subclass FunctionQuantity Function)
(documentation FunctionQuantity "A &%FunctionQuantity is a &%Function that 
maps from one or more instances of &%ConstantQuantity to another instance 
of &%ConstantQuantity.  For example, the velocity of a particle would be 
represented by a &%FunctionQuantity mapping values of time (which are 
&%ConstantQuantities) to values of distance (also &%ConstantQuantities).  
Note that all instances of &%FunctionQuantity are &%Functions with a fixed 
arity.  Note too that all elements of the range of a &%FunctionQuantity 
have the same physical dimension as the &%FunctionQuantity itself.")

(subclass UnaryConstantFunctionQuantity FunctionQuantity)
(subclass UnaryConstantFunctionQuantity UnaryFunction)
(documentation UnaryConstantFunctionQuantity "The class of &%UnaryFunctions 
that map from the &%Class &%ConstantQuantity to the &%Class 
&%ConstantQuantity.")

(=>
   (instance ?FUNCTION UnaryConstantFunctionQuantity)
   (and
      (domain ?FUNCTION 1 ConstantQuantity)
      (range ?FUNCTION ConstantQuantity)))

(subclass TimeDependentQuantity UnaryConstantFunctionQuantity)
(subclass TimeDependentQuantity ContinuousFunction)
(documentation TimeDependentQuantity "A &%UnaryConstantFunction of continuous 
time.  All instances of this &%Class map a time quantity into another 
&%ConstantQuantity such as temperature.  For example, 'the temperature at 
the top of the Empire State Building' is a &%TimeDependentQuantity since 
its value depends on the time.")

(=>
   (instance ?FUNCTION TimeDependentQuantity)
   (domain ?FUNCTION 1 TimeMeasure))

(subclass SetOrClass Abstract)
(partition SetOrClass Set Class)
(documentation SetOrClass "The &%SetOrClass of &%Sets and &%Classes, i.e. any instance 
of &%Abstract that has &%elements or &%instances.")

(subclass Class SetOrClass)
(documentation Class "&%Classes differ from &%Sets in three important respects.  
First, &%Classes are not assumed to be extensional.  That is, distinct 
&%Classes might well have exactly the same instances.  Second, &%Classes typically 
have an associated `condition' that determines the instances of the &%Class.  So, 
for example, the condition `human' determines the &%Class of &%Humans.  Note that 
some &%Classes might satisfy their own condition (e.g., the &%Class of &%Abstract 
things is &%Abstract) and hence be instances of themselves.  Third, the instances 
of a class may occur only once within the class, i.e. a class cannot contain 
duplicate instances.")

(subclass Set SetOrClass)
(documentation Set "A &%SetOrClass that satisfies extensionality as well as
other constraints specified by some choice of set theory.  &%Sets differ 
from &%Classes in two important respects.  First, &%Sets are extensional - 
two &%Sets with the same &%elements are identical.  Second, a &%Set can be 
an arbitrary stock of objects.  That is, there is no requirement that &%Sets 
have an associated condition that determines their membership.  Note that &%Sets 
are not assumed to be unique sets, i.e. &%elements of a &%Set may occur more 
than once in the &%Set.")

(subclass Relation Abstract)
(disjointDecomposition Relation BinaryRelation TernaryRelation QuaternaryRelation QuintaryRelation VariableArityRelation)
(partition Relation Predicate Function List)
(partition Relation TotalValuedRelation PartialValuedRelation)
(documentation Relation "The &%Class of relations.  There are three kinds 
of &%Relation:  &%Predicate, &%Function, and &%List.  &%Predicates and 
&%Functions both denote sets of ordered n-tuples.  The difference between 
these two &%Classes is that &%Predicates cover formula-forming operators, while 
&%Functions cover term-forming operators.  A &%List, on the other hand, is a 
particular ordered n-tuple.")

(=>
   (instance ?REL Relation)
   (<=> 
        (holds ?REL @ROW)
        (?REL @ROW)))

;; The following part of the ontology covers the various classes under 
;; 'Relation'.  Most of the content here is taken from frame-ontology, 
;; abstract-algebra, kif-relations, and kif-extensions (ontologies 
;; available on the Ontolingua server).

(subclass SingleValuedRelation Relation)
(instance SingleValuedRelation InheritableRelation)
(documentation SingleValuedRelation "A &%Relation is a &%SingleValuedRelation 
just in case an assignment of values to every argument position except the last 
one determines at most one assignment for the last argument position.  Note 
that not all &%SingleValuedRelations are &%TotalValuedRelations.")

(=>
   (instance ?REL SingleValuedRelation)
   (forall (@ROW ?ITEM1 ?ITEM2)
      (=>
         (and
            (holds ?REL @ROW ?ITEM1)
            (holds ?REL @ROW ?ITEM2))
         (equal ?ITEM1 ?ITEM2))))

(subclass TotalValuedRelation Relation)
(instance TotalValuedRelation InheritableRelation)
(documentation TotalValuedRelation "A &%Relation is a &%TotalValuedRelation 
just in case there exists an assignment for the last argument position of the 
&%Relation given any assignment of values to every argument position except 
the last one.  Note that declaring a &%Relation to be both a &%TotalValuedRelation 
and a &%SingleValuedRelation means that it is a total function.")

(<=>
   (instance ?REL TotalValuedRelation)
   (exists (?VALENCE)
      (and
         (instance ?REL Relation)
         (valence ?REL ?VALENCE)
         (=>
            (forall (?NUMBER ?ELEMENT ?CLASS)
               (=>
                  (and
                     (lessThan ?NUMBER ?VALENCE)
                     (domain ?REL ?NUMBER ?CLASS)
                     (equal ?ELEMENT (ListOrderFn (ListFn @ROW) ?NUMBER)))
                  (instance ?ELEMENT ?CLASS)))
            (exists (?ITEM)
               (holds ?REL @ROW ?ITEM))))))

(subclass PartialValuedRelation Relation)
(documentation PartialValuedRelation "A &%Relation is a &%PartialValuedRelation 
just in case it is not a &%TotalValuedRelation, i.e. just in case assigning values 
to every argument position except the last one does not necessarily mean that there 
is a value assignment for the last argument position.  Note that, if a &%Relation 
is both a &%PartialValuedRelation and a &%SingleValuedRelation, then it is a partial 
function.")

(subclass BinaryRelation Relation)
(instance BinaryRelation InheritableRelation)
(documentation BinaryRelation "&%BinaryRelations are relations that are 
true only of pairs of things.  &%BinaryRelations are represented as slots 
in frame systems.")

(=>
   (instance ?REL BinaryRelation)
   (not
      (exists (?ITEM1 ?ITEM2 ?ITEM3 @ROW)
         (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 @ROW))))

(subclass ReflexiveRelation BinaryRelation)
(documentation ReflexiveRelation "&%Relation ?REL is reflexive if 
(?REL ?INST ?INST) for all ?INST.")

(=>
   (instance ?REL ReflexiveRelation)
   (=>
      (or
         (holds ?REL ?INST1 ?INST2)
         (holds ?REL ?INST2 ?INST1))
      (holds ?REL ?INST1 ?INST1)))

(subclass IrreflexiveRelation BinaryRelation)
(documentation IrreflexiveRelation "&%Relation ?REL is irreflexive 
if (?REL ?INST ?INST) holds for no value of ?INST.")

(=>
   (instance ?REL IrreflexiveRelation)
   (forall (?INST)
      (not 
         (holds ?REL ?INST ?INST))))

(subclass SymmetricRelation BinaryRelation)
(documentation SymmetricRelation "A &%BinaryRelation ?REL is
symmetric just in case (?REL ?INST1 ?INST2) imples (?REL 
?INST2 ?INST1), for all ?INST1 and ?INST2.")


(=>
   (instance ?REL SymmetricRelation)
   (forall (?INST1 ?INST2)
      (=>
         (holds ?REL ?INST1 ?INST2)
         (holds ?REL ?INST2 ?INST1))))

(subclass AsymmetricRelation IrreflexiveRelation)
(subclass AsymmetricRelation AntisymmetricRelation)
(documentation AsymmetricRelation "A &%BinaryRelation is asymmetric only 
if it is both an &%AntisymmetricRelation and an &%IrreflexiveRelation.")

(=>
   (and
      (instance ?REL BinaryRelation)
      (or
         (domain ?REL 1 ?CLASS1)
         (domainSubclass ?REL 1 ?CLASS1))
      (or
         (domain ?REL 2 ?CLASS2)
         (domainSubclass ?REL 2 ?CLASS2)
         (range ?REL ?CLASS2)
         (rangeSubclass ?REL ?CLASS2))
      (disjoint ?CLASS1 ?CLASS2))
   (instance ?REL AsymmetricRelation))

(subclass AntisymmetricRelation BinaryRelation)
(documentation AntisymmetricRelation "&%BinaryRelation ?REL is an 
&%AntisymmetricRelation if for distinct ?INST1 and ?INST2, (?REL ?INST1 
?INST2) implies not (?REL ?INST2 ?INST1).  In other words, for all ?INST1 
and ?INST2, (?REL ?INST1 ?INST2) and (?REL ?INST2 ?INST1) imply that ?INST1 
and ?INST2 are identical.  Note that it is possible for an 
&%AntisymmetricRelation to be a &%ReflexiveRelation.")

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

(subclass TrichotomizingRelation BinaryRelation)
(documentation TrichotomizingRelation "A &%BinaryRelation ?REL is a 
&%TrichotomizingRelation just in case all ordered pairs consisting of 
distinct individuals are elements of ?REL.") 

(=>
   (instance ?REL TrichotomizingRelation)
   (forall (?INST1 ?INST2)
      (or
         (holds ?REL ?INST1 ?INST2) 
         (equal ?INST1 ?INST2) 
         (holds ?REL ?INST2 ?INST1))))

(subclass TransitiveRelation BinaryRelation)
(documentation TransitiveRelation "A &%BinaryRelation ?REL is transitive 
if (?REL ?INST1 ?INST2) and (?REL ?INST2 ?INST3) imply (?REL ?INST1 ?INST3), 
for all ?INST1, ?INST2, and ?INST3.")

(=>
   (instance ?REL TransitiveRelation)
   (forall (?INST1 ?INST2 ?INST3)
      (=>
         (and
            (holds ?REL ?INST1 ?INST2)
            (holds ?REL ?INST2 ?INST3))
         (holds ?REL ?INST1 ?INST3))))

(subclass IntransitiveRelation BinaryRelation)
(documentation IntransitiveRelation "A &%BinaryRelation ?REL is 
intransitive only if (?REL ?INST1 ?INST2) and (?REL ?INST2 ?INST3) imply not 
(?REL ?INST1 ?INST3), for all ?INST1, ?INST2, and ?INST3.")

(=> 
   (instance ?REL IntransitiveRelation)
   (forall (?INST1 ?INST2 ?INST3)
      (=> 
         (and 
            (holds ?REL ?INST1 ?INST2)
            (holds ?REL ?INST2 ?INST3))
         (not 
            (holds ?REL ?INST1 ?INST3)))))

(subclass PartialOrderingRelation TransitiveRelation)
(subclass PartialOrderingRelation AntisymmetricRelation)
(subclass PartialOrderingRelation ReflexiveRelation)
(documentation PartialOrderingRelation "A &%BinaryRelation is a partial 
ordering if it is a &%ReflexiveRelation, an &%AntisymmetricRelation, and 
a &%TransitiveRelation.")

(subclass TotalOrderingRelation PartialOrderingRelation)
(subclass TotalOrderingRelation TrichotomizingRelation)
(documentation TotalOrderingRelation  "A &%BinaryRelation is a 
&%TotalOrderingRelation if it is a &%PartialOrderingRelation 
and a &%TrichotomizingRelation.")

(=>
   (instance ?REL TotalOrderingRelation)
   (forall (?INST1 ?INST2)
      (or
         (holds ?REL ?INST1 ?INST2)
         (holds ?REL ?INST2 ?INST1))))

(subclass EquivalenceRelation TransitiveRelation)
(subclass EquivalenceRelation SymmetricRelation)
(subclass EquivalenceRelation ReflexiveRelation)
(documentation EquivalenceRelation "A &%BinaryRelation is an equivalence 
relation if it is a &%ReflexiveRelation, a &%SymmetricRelation, and a 
&%TransitiveRelation.")

(subclass CaseRole BinaryPredicate)
(instance CaseRole InheritableRelation)
(subclass CaseRole AsymmetricRelation)
(documentation CaseRole "The &%Class of &%Predicates relating the 
spatially distinguished parts of a &%Process. &%CaseRoles include, for 
example, the &%agent, &%patient or &%destination of an action, the flammable 
substance in a burning process, or the water that falls in rain.")

(instance agent CaseRole)
(domain agent 1 Process)
(domain agent 2 Agent)
(documentation agent "(&%agent ?PROCESS ?AGENT) means that ?AGENT is 
an active determinant, either animate or inanimate, of the &%Process 
?PROCESS, with or without voluntary intention.  For example, water is 
the &%agent of erosion in the following proposition:  the water 
eroded the coastline.  For another example, Eve is an &%agent in the 
following proposition: Eve bit an apple.")

(=>
   (instance ?PROCESS Process)
   (exists (?CAUSE)
      (agent ?PROCESS ?CAUSE)))

(instance destination CaseRole)
(domain destination 1 Process)
(domain destination 2 Entity)
(documentation destination "(destination ?PROCESS ?GOAL) means that 
?GOAL is the target or goal of the Process ?PROCESS.  For example, 
Danbury would be the destination in the following proposition:  Bob went 
to Danbury.  Note that this is a very general &%CaseRole and, in 
particular, that it covers the concepts of 'recipient' and 'beneficiary'.  
Thus, John would be the &%destination in the following proposition:  
Tom gave a book to John.")

(instance experiencer CaseRole)
(domain experiencer 1 Process)
(domain experiencer 2 Agent)
(documentation experiencer "(&%experiencer ?PROCESS ?AGENT) means 
that ?AGENT experiences the &%Process ?PROCESS.  For example, Yojo 
is the &%experiencer of seeing in the following proposition:  Yojo 
sees the fish.  Note that &%experiencer, unlike &%agent, does 
not entail a causal relation between its arguments.")

(subrelation instrument patient)
(domain instrument 1 Process)
(domain instrument 2 Object)
(documentation instrument "(instrument ?EVENT ?TOOL) means that ?TOOL 
is used by an agent in bringing about ?EVENT and that ?TOOL is not 
changed by ?EVENT.  For example, the key is an &%instrument in the 
following proposition: The key opened the door.  Note that &%instrument 
and &%resource cannot be satisfied by the same ordered pair.")

(instance origin CaseRole)
(domain origin 1 Process)
(domain origin 2 Object)
(documentation origin "(&%origin ?PROCESS ?SOURCE) means that ?SOURCE 
indicates where the ?Process began.  Note that this relation implies 
that ?SOURCE is present at the beginning of the process, but need not 
participate throughout the process.  For example, the submarine is the 
&%origin in the following proposition: the missile was launched from a 
submarine.")

(instance patient CaseRole)
(domain patient 1 Process)
(domain patient 2 Entity)
(documentation patient "(&%patient ?PROCESS ?ENTITY) means that ?ENTITY 
is a participant in ?PROCESS that may be moved, said, experienced, etc.  
For example, the direct objects in the sentences 'The cat swallowed the 
canary' and 'Billy likes the beer' would be examples of &%patients.  Note 
that the &%patient of a &%Process may or may not undergo structural 
change as a result of the &%Process.  The &%CaseRole of &%patient is used 
when one wants to specify as broadly as possible the object of a 
&%Process.")

(subrelation resource patient)
(domain resource 1 Process)
(domain resource 2 Object)
(disjointRelation resource result instrument)
(documentation resource "(&%resource ?PROCESS ?RESOURCE) means that 
?RESOURCE is present at the beginning of ?PROCESS, is used by ?PROCESS, 
and as a consequence is changed by ?PROCESS.  For example, soap is a 
&%resource in the following proposition:  the gun was carved out of soap.  
Note that &%resource differs from &%instrument, another subrelation of 
&%patient, in that its internal or physical properties are altered in 
some way by the &%Process.")

(subrelation result patient)
(domain result 1 Process)
(domain result 2 Entity)
(documentation result "(result ?ACTION ?OUTPUT) means that ?OUTPUT is 
a product of ?ACTION.  For example, house is a &%result in the 
following proposition: Eric built a house.")

(instance InheritableRelation Class)
(documentation InheritableRelation "This is a &%Class of &%Classes.  Each 
&%instance of &%InheritableRelation is a &%subclass of &%Relation whose 
properties can be inherited downward in the class hierarchy via the 
&%subrelation &%Predicate.")

(subclass ProbabilityRelation Relation)
(instance ProbabilityRelation InheritableRelation)
(documentation ProbabilityRelation "The &%Class of &%Relations that 
permit assessment of the probability of an event or situation.")

(instance ProbabilityFn ProbabilityRelation)
(instance ProbabilityFn TotalValuedRelation)
(instance ProbabilityFn UnaryFunction)
(domain ProbabilityFn 1 Formula)
(range ProbabilityFn RealNumber)
(instance ProbabilityFn AsymmetricRelation)
(documentation ProbabilityFn "One of the basic &%ProbabilityRelations, 
&%ProbabilityFn is used to state the a priori probability of a state of 
affairs.  (&%ProbabilityFn ?FORMULA) denotes the a priori probability 
of ?FORMULA.")

(instance conditionalProbability ProbabilityRelation)
(instance conditionalProbability TernaryPredicate)
(domain conditionalProbability 1 Formula)
(domain conditionalProbability 2 Formula)
(domain conditionalProbability 3 RealNumber)
(documentation conditionalProbability "One of the basic &%ProbabilityRelations.  
&%conditionalProbability is used to state the numeric value of a conditional 
probability.  (&%conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER) means 
that the probability of ?FORMULA2 being true given that ?FORMULA1 is true is 
?NUMBER.") 

(instance increasesLikelihood ProbabilityRelation)
(instance increasesLikelihood BinaryPredicate)
(instance increasesLikelihood IrreflexiveRelation)
(domain increasesLikelihood 1 Formula)
(domain increasesLikelihood 2 Formula)
(disjointRelation increasesLikelihood decreasesLikelihood independentProbability)
(documentation increasesLikelihood "One of the basic &%ProbabilityRelations.  
(&%increasesLikelihood ?FORMULA1 ?FORMULA2) means that ?FORMULA2 is more 
likely to be true if ?FORMULA1 is true.")

(=>
   (and
      (increasesLikelihood ?FORMULA1 ?FORMULA2)
      (equal (ProbabilityFn ?FORMULA2) ?NUMBER1)
      (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
   (greaterThan ?NUMBER2 ?NUMBER1))

(instance decreasesLikelihood ProbabilityRelation)
(instance decreasesLikelihood BinaryPredicate)
(instance decreasesLikelihood IrreflexiveRelation)
(domain decreasesLikelihood 1 Formula)
(domain decreasesLikelihood 2 Formula)
(documentation decreasesLikelihood "One of the basic &%ProbabilityRelations.  
(&%decreasesLikelihood ?FORMULA1 ?FORMULA2) means that ?FORMULA2 is less 
likely to be true if ?FORMULA1 is true.")

(=>
   (and
      (decreasesLikelihood ?FORMULA1 ?FORMULA2)
      (equal (ProbabilityFn ?FORMULA2) ?NUMBER1)
      (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
   (lessThan ?NUMBER2 ?NUMBER1))

(instance independentProbability ProbabilityRelation)
(instance independentProbability BinaryPredicate)
(instance independentProbability SymmetricRelation)
(domain independentProbability 1 Formula)
(domain independentProbability 2 Formula)
(documentation independentProbability "One of the basic &%ProbabilityRelations.  
(&%independentProbability ?FORMULA1 ?FORMULA2) means that the probabilities of 
?FORMULA1 and ?FORMULA2 being true are independent.") 

(=>
   (and
      (independentProbability ?FORMULA1 ?FORMULA2)
      (equal (ProbabilityFn ?FORMULA2) ?NUMBER1)
      (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
   (equal ?NUMBER2 ?NUMBER1))

(=>
   (and
      (instance ?FORMULA1 Formula)
      (instance ?FORMULA2 Formula))
   (or
      (increasesLikelihood ?FORMULA1 ?FORMULA2)
      (decreasesLikelihood ?FORMULA1 ?FORMULA2)
      (independentProbability ?FORMULA1 ?FORMULA2)))

(subclass SpatialRelation Relation)
(instance SpatialRelation InheritableRelation)
(documentation SpatialRelation "The &%Class of &%Relations that are 
spatial in a wide sense.  This &%Class includes mereological relations 
and topological relations.")

(subclass TemporalRelation Relation)
(instance TemporalRelation InheritableRelation)
(documentation TemporalRelation "The &%Class of temporal &%Relations.  
This &%Class includes notions of (temporal) topology of intervals, 
(temporal) schemata, and (temporal) extension.")

(instance IntentionalRelation InheritableRelation)
(documentation IntentionalRelation "The &%Class of &%Relations between 
an &%Agent and one or more &%Entities, where the &%Relation requires that 
the &%Agent have awareness of the &%Entity.")

(=>
   (and
      (instance ?REL IntentionalRelation)
      (holds ?REL ?AGENT @ROW)
      (inList ?OBJ (ListFn @ROW)))
   (inScopeOfInterest ?AGENT ?OBJ))

(instance prefers TernaryPredicate)
(instance prefers IntentionalRelation)
(domain prefers 1 CognitiveAgent)
(domain prefers 2 Formula)
(domain prefers 3 Formula)
(documentation prefers "(&%prefers ?AGENT ?FORMULA1 ?FORMULA2) means that 
&%CognitiveAgent ?AGENT prefers the state of affairs expressed by ?FORMULA1
over the state of affairs expressed by ?FORMULA2 all things being equal.")

(=>
   (prefers ?AGENT ?FORMULA1 ?FORMULA2)
   (not (and
      (true ?FORMULA1 True)
      (true ?FORMULA2 True))))  

(subclass PropositionalAttitude IntentionalRelation)
(subclass PropositionalAttitude AsymmetricRelation)
(instance PropositionalAttitude InheritableRelation)
(documentation PropositionalAttitude "The &%Class of 
&%IntentionalRelations where the &%Agent has awareness of a 
&%Proposition.")

(=>
   (and
      (instance ?REL PropositionalAttitude)
      (holds ?REL ?AGENT ?FORMULA))
   (instance ?FORMULA Formula))

(subclass ObjectAttitude IntentionalRelation)
(instance ObjectAttitude InheritableRelation)
(disjoint ObjectAttitude PropositionalAttitude)
(documentation ObjectAttitude "The &%Class of &%IntentionalRelations 
where the &%Agent has awareness of an instance of &%Physical.")

(=>
   (and
      (instance ?REL ObjectAttitude)
      (holds ?REL ?AGENT ?THING))
   (instance ?THING Physical))

(instance inScopeOfInterest BinaryPredicate)
(instance inScopeOfInterest IntentionalRelation)
(domain inScopeOfInterest 1 CognitiveAgent)
(domain inScopeOfInterest 2 Entity)
(documentation inScopeOfInterest "A very general &%Predicate.  
(&%inScopeOfInterest ?AGENT ?ENTITY) means that ?ENTITY is within the 
scope of interest of ?AGENT.  Note that the interest indicated can be 
either positive or negative, i.e. the ?AGENT can have an interest in 
avoiding or promoting ?ENTITY.")

(=>
   (and
      (instance ?PROCESS IntentionalProcess)
      (agent ?PROCESS ?AGENT)
      (patient ?PROCESS ?OBJECT))
   (inScopeOfInterest ?AGENT ?OBJECT))

(instance needs ObjectAttitude)
(subrelation needs inScopeOfInterest)
(domain needs 1 CognitiveAgent)
(domain needs 2 Physical)
(documentation needs "(&%needs ?AGENT ?OBJECT) means that ?OBJECT is 
physically required for the continued existence of ?AGENT.")

(=>
    (needs ?AGENT ?OBJECT)
    (wants ?AGENT ?OBJECT))

(instance wants ObjectAttitude)
(subrelation wants inScopeOfInterest)
(relatedInternalConcept wants desires)
(domain wants 1 CognitiveAgent)
(domain wants 2 Physical)
(documentation wants "(&%wants ?AGENT ?OBJECT) means that ?OBJECT is desired by ?AGENT, 
i.e. ?AGENT believes that ?OBJECT will satisfy one of its goals.  Note that there is 
no implication that what is wanted by an agent is not already possessed by the agent.")

(=>
   (wants ?AGENT ?OBJ)
   (exists (?PURP)
      (hasPurposeForAgent ?OBJ ?PURP ?AGENT)))

(=>
   (wants ?AGENT ?OBJ)
   (desires ?AGENT (possesses ?AGENT ?OBJ)))

(instance desires PropositionalAttitude)
(subrelation desires inScopeOfInterest)
(relatedInternalConcept desires wants)
(domain desires 1 CognitiveAgent)
(domain desires 2 Formula)
(documentation desires "(&%desires ?AGENT ?FORMULA) means that ?AGENT wants 
to bring about the state of affairs expressed by ?FORMULA.  Note that there 
is no implication that what is desired by the agent is not already true.  
Note too that &%desires is distinguished from &%wants only in that the former 
is a &%PropositionalAttitude, while &%wants is an &%ObjectAttitude.")

(instance considers PropositionalAttitude)
(subrelation considers inScopeOfInterest)
(domain considers 1 CognitiveAgent)
(domain considers 2 Formula)
(documentation considers "(&%considers ?AGENT ?FORMULA) means that ?AGENT 
considers or wonders about the truth of the proposition expressed by 
?FORMULA.") 

(instance believes PropositionalAttitude)
(subrelation believes inScopeOfInterest)
(domain believes 1 CognitiveAgent)
(domain believes 2 Formula)
(documentation believes "The epistemic predicate of belief.  
(&%believes ?AGENT ?FORMULA) means that ?AGENT believes the proposition 
expressed by ?FORMULA.")

(=>
   (believes ?AGENT ?FORMULA)
   (exists (?TIME)
      (holdsDuring ?TIME (considers ?AGENT ?FORMULA))))

(instance knows PropositionalAttitude)
(subrelation knows inScopeOfInterest)
(domain knows 1 CognitiveAgent)
(domain knows 2 Formula)
(documentation knows "The epistemic predicate of knowing.  (&%knows 
?AGENT ?FORMULA) means that ?AGENT knows the proposition expressed by 
?FORMULA.  Note that &%knows entails conscious awareness, so this 
&%Predicate cannot be used to express tacit or subconscious or 
unconscious knowledge.")

(=>
    (knows ?AGENT ?FORMULA)
    (believes ?AGENT ?FORMULA))

(=>
   (knows ?AGENT ?FORMULA)
   (true ?FORMULA True))

(subclass TernaryRelation Relation)
(instance TernaryRelation InheritableRelation)
(documentation TernaryRelation "&%TernaryRelations relate three items.  
The two &%subclasses of &%TernaryRelation are &%TernaryPredicate and 
&%BinaryFunction.")

(=>
   (instance ?REL TernaryRelation)
   (not
      (exists (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW)
         (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW))))

(subclass QuaternaryRelation Relation)
(instance QuaternaryRelation InheritableRelation)
(documentation QuaternaryRelation "&%QuaternaryRelations relate four 
items.  The two &%subclasses of &%QuaternaryRelation are 
&%QuaternaryPredicate and &%TernaryFunction.")

(=>
   (instance ?REL QuaternaryRelation)
   (not
      (exists (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW)
         (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW))))

(subclass QuintaryRelation Relation)
(instance QuintaryRelation InheritableRelation)
(documentation QuintaryRelation "&%QuintaryRelations relate five items.  
The two &%subclasses of &%QuintaryRelation are &%QuintaryPredicate and 
&%QuaternaryFunction.")

(=>
   (instance ?REL QuintaryRelation)
   (not
      (exists (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW)
         (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW))))

(subclass List Relation)
(documentation List "Every &%List is a particular ordered n-tuple of 
items.  Generally speaking, &%Lists are created by means of the &%ListFn 
&%Function, which takes any number of items as arguments and returns a 
&%List with the items in the same order.  Anything, including other 
&%Lists, may be an item in a &%List.  Note too that &%Lists are 
extensional - two lists that have the same items in the same order are 
identical.  Note too that a &%List may contain no items.  In that case, 
the &%List is the &%NullList.")

(=>
   (instance ?LIST List)
   (exists (?NUMBER1)
      (exists (?ITEM1)
         (and
            (not (equal (ListOrderFn ?LIST ?NUMBER1) ?ITEM1))
            (forall (?NUMBER2)
               (=>
                  (and
                     (instance ?NUMBER2 PositiveInteger)
                     (lessThan ?NUMBER2 ?NUMBER1))
                  (exists (?ITEM2)
                     (equal (ListOrderFn ?LIST ?NUMBER2) ?ITEM2))))))))

(subclass UniqueList List)
(documentation UniqueList "A &%List in which no item appears more than once, 
i.e. a &%List for which there are no distinct numbers ?NUMBER1 and ?NUMBER2 
such that (&%ListOrderFn ?LIST ?NUMBER1) and (&%ListOrderFn ?LIST ?NUMBER2) 
return the same value.")

(=>
   (instance ?LIST UniqueList)
   (forall (?NUMBER1 ?NUMBER2)
      (=>
         (equal (ListOrderFn ?LIST ?NUMBER1) (ListOrderFn ?LIST ?NUMBER2))
         (equal ?NUMBER1 ?NUMBER2)))) 

(instance NullList List)
(documentation NullList "The &%List that has no items.  The uniqueness of 
&%NullList follows from the extensionality of &%Lists, i.e. the fact that 
two &%Lists with the same items in the same order are identical.")

(<=>
   (equal ?LIST NullList)
   (and
      (instance ?LIST List)
      (not 
         (exists (?ITEM)
            (inList ?ITEM ?LIST)))))

(instance ListFn Function)
(instance ListFn VariableArityRelation)
(instance ListFn TotalValuedRelation)
(range ListFn List)
(documentation ListFn "A &%Function that takes any number of arguments and 
returns the &%List containing those arguments in exactly the same order.")

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

(=>
   (disjointDecomposition ?CLASS @ROW)
   (forall (?ITEM)
      (=>
         (inList ?ITEM (ListFn @ROW))
         (subclass ?ITEM ?CLASS))))

(=>
   (disjointDecomposition ?CLASS @ROW)
   (forall (?ITEM1 ?ITEM2)
      (=>
         (and
            (inList ?ITEM1 (ListFn @ROW))
            (inList ?ITEM2 (ListFn @ROW))
            (not
               (equal ?ITEM1 ?ITEM2)))
         (disjoint ?ITEM1 ?ITEM2))))

(instance ListOrderFn BinaryFunction)
(instance ListOrderFn PartialValuedRelation)
(domain ListOrderFn 1 List)
(domain ListOrderFn 2 PositiveInteger)
(range ListOrderFn Entity)
(documentation ListOrderFn "(&%ListOrderFn ?LIST ?NUMBER) denotes the item 
that is in the ?NUMBER position in the &%List ?LIST.  For example, 
(&%ListOrderFn (&%ListFn &%Monday &%Tuesday &%Wednesday) 2) would return the 
value &%Tuesday.")

(=>
   (and
      (instance ?LIST1 List)
      (instance ?LIST2 List)
      (forall (?NUMBER)
         (equal (ListOrderFn ?LIST1 ?NUMBER) (ListOrderFn ?LIST2 ?NUMBER))))
   (equal ?LIST1 ?LIST2))

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

(=>
   (and
      (domainSubclass ?REL ?NUMBER ?CLASS)
      (holds ?REL @ROW))
   (subclass (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS))

(instance ListLengthFn UnaryFunction)
(instance ListLengthFn TotalValuedRelation)
(domain ListLengthFn 1 List)
(range ListLengthFn NonnegativeInteger)
(documentation ListLengthFn "A &%Function that takes a &%List as its sole 
argument and returns the number of items in the &%List.  For example, 
(&%ListLengthFn (&%ListFn &%Monday &%Tuesday &%Wednesday)) would return the 
value 3.")

(=>
   (and
      (equal (ListLengthFn ?LIST) ?NUMBER1)
      (instance ?LIST List)
      (instance ?NUMBER1 PositiveInteger))
   (forall (?NUMBER2)
      (<=>
         (exists (?ITEM)
            (and
               (equal (ListOrderFn ?LIST ?NUMBER2) ?ITEM)
               (inList ?ITEM ?LIST)))
         (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

(equal (ListLengthFn (ListFn @ROW ?ITEM)) (SuccessorFn (ListLengthFn (ListFn @ROW))))

(equal (ListOrderFn (ListFn @ROW ?ITEM) (ListLengthFn (ListFn @ROW ?ITEM))) ?ITEM)

(=>
   (valence ?REL ?NUMBER)
   (forall (@ROW)
      (=>
         (holds ?REL @ROW)
         (equal (ListLengthFn (ListFn @ROW)) ?NUMBER))))

(=>
   (and
      (equal (ListLengthFn ?LIST1) ?NUMBER)
      (instance ?LIST List)
      (instance ?NUMBER1 PositiveInteger))
   (exists (?LIST2 ?ITEM)
      (and
         (initialList ?LIST1 ?LIST2)
         (equal (SuccessorFn ?NUMBER) (ListLengthFn ?LIST2))
         (equal (ListOrderFn ?LIST2 (SuccessorFn ?NUMBER)) ?ITEM))))

(instance ListConcatenateFn BinaryFunction)
(instance ListConcatenateFn TotalValuedRelation)
(domain ListConcatenateFn 1 List)
(domain ListConcatenateFn 2 List)
(range ListConcatenateFn List)
(documentation ListConcatenateFn "A &%Function that returns the concatenation 
of the two &%Lists that are given as arguments.  For example, the value of 
(&%ListConcatenateFn (&%ListFn &%Monday &%Tuesday) (&%ListFn &%Wednesday 
&%Thursday)) would be (&%ListFn &%Monday &%Tuesday &%Wednesday &%Thursday).")

(<=>
   (equal ?LIST3 (ListConcatenateFn ?LIST1 ?LIST2))
   (forall (?NUMBER1 ?NUMBER2)
      (=>
         (and
            (lessThanOrEqualTo ?NUMBER1 (ListLengthFn ?LIST1))
            (lessThanOrEqualTo ?NUMBER2 (ListLengthFn ?LIST2))
            (instance ?NUMBER1 PositiveInteger)
            (instance ?NUMBER2 PositiveInteger))
         (and
            (equal (ListOrderFn ?LIST3 ?NUMBER1) (ListOrderFn ?LIST1 ?NUMBER1))
            (equal (ListOrderFn ?LIST3 (AdditionFn (ListLengthFn ?LIST1) ?NUMBER2)) (ListOrderFn ?LIST2 ?NUMBER2))))))

(instance inList BinaryPredicate)
(instance inList IrreflexiveRelation)
(instance inList AsymmetricRelation)
(domain inList 1 Entity)
(domain inList 2 List)
(documentation inList "The analog of &%element and &%instance for &%Lists.  
(&%inList ?OBJ ?LIST) means that ?OBJ is in the &%List ?LIST.  For example, 
(&%inList &%Tuesday (&%ListFn &%Monday &%Tuesday &%Wednesday)) would be true.")

(=>
   (inList ?ITEM ?LIST)
   (exists (?NUMBER)
      (equal (ListOrderFn ?LIST ?NUMBER) ?ITEM)))

(instance subList BinaryPredicate)
(instance subList PartialOrderingRelation)
(domain subList 1 List)
(domain subList 2 List)
(documentation subList "(&%subList ?LIST1 ?LIST2) means that ?LIST1 is a 
sublist of ?LIST2, i.e. every element of ?LIST1 is an element of ?LIST2 and 
the elements that are common to both &%Lists have the same order in both 
&%Lists.")

(=>
   (subList ?LIST1 ?LIST2)
   (forall (?ITEM)
      (=>
         (inList ?ITEM ?LIST1)
         (inList ?ITEM ?LIST2))))

(=>
   (subList ?LIST1 ?LIST2)
   (exists (?NUMBER3)
      (forall (?ITEM)
         (=>
            (inList ?ITEM ?LIST1)
            (exists (?NUMBER1 ?NUMBER2)
               (and
                  (equal (ListOrderFn ?LIST1 ?NUMBER1) ?ITEM)
                  (equal (ListOrderFn ?LIST2 ?NUMBER2) ?ITEM)
                  (equal ?NUMBER2 (AdditionFn ?NUMBER1 ?NUMBER3))))))))

(instance initialList BinaryPredicate)
(instance initialList PartialOrderingRelation)
(subrelation initialList subList)
(documentation initialList "(&%initialList ?LIST1 ?LIST2) means that ?LIST1 
is a &%subList of ?LIST2 and (&%ListOrderFn ?LIST1 ?NUMBER) returns the same 
value as (&%ListOrderFn ?LIST2 ?NUMBER) for all of the values of ?NUMBER over 
which (&%ListOrderFn ?LIST1 ?NUMBER) is defined.")

(=>
   (initialList ?LIST1 ?LIST2)
   (forall (?NUMBER1 ?NUMBER2)
      (=>
         (and
            (equal (ListLengthFn ?LIST1) ?NUMBER1)
            (lessThanOrEqualTo ?NUMBER2 ?NUMBER1)) 
         (equal (ListOrderFn ?LIST1 ?NUMBER2) (ListOrderFn ?LIST2 ?NUMBER2)))))

(initialList (ListFn @ROW) (ListFn @ROW ?ITEM))

(subclass Predicate Relation)
(instance Predicate InheritableRelation)
(documentation Predicate "A &%Predicate is a sentence-forming &%Relation.  
Each tuple in the &%Relation is a finite, ordered sequence of objects.  
The fact that a particular tuple is an element of a &%Predicate is denoted 
by '(*predicate* arg_1 arg_2 .. arg_n)', where the arg_i are the 
objects so related.  In the case of &%BinaryPredicates, the fact can
be read as `arg_1 is *predicate* arg_2' or `a *predicate* of
arg_1 is arg_2'.")

(subclass Function SingleValuedRelation)
(instance Function InheritableRelation)
(documentation Function "A &%Function is a term-forming &%Relation that 
maps from a n-tuple of arguments to a range and that associates this 
n-tuple with at most one range element.  Note that the range is a &%SetOrClass, 
and each element of the range is an instance of the &%SetOrClass.")

(subclass UnaryFunction Function)
(subclass UnaryFunction BinaryRelation)
(instance UnaryFunction InheritableRelation)
(documentation UnaryFunction "The &%Class of &%Functions that require a 
single argument.")

(=>
   (instance ?FUNCTION UnaryFunction)
   (valence ?FUNCTION 1))

(subclass OneToOneFunction UnaryFunction)
(documentation OneToOneFunction "The &%Class of &%UnaryFunctions which 
are one to one.  A function F is one to one just in case for all X, Y in the 
domain of F, if X is not identical to Y, then F(X) is not identical to F(Y).")

(=> 
   (instance ?FUN OneToOneFunction) 
   (forall (?ARG1 ?ARG2) 
      (=> 
         (and 
            (domain ?FUN 1 ?CLASS)
            (instance ?ARG1 ?CLASS)
            (instance ?ARG2 ?CLASS)
            (not (equal ?ARG1 ?ARG2))) 
         (not (equal (AssignmentFn ?FUN ?ARG1) (AssignmentFn ?FUN ?ARG2))))))

(subclass SequenceFunction OneToOneFunction)
(documentation SequenceFunction "The &%Class of &%OneToOneFunctions whose range 
is a subclass of the &%PositiveIntegers.")

(=> 
   (and
      (instance ?SEQ SequenceFunction) 
      (range ?SEQ ?CLASS))
   (subclass ?CLASS Integer))

(subclass BinaryFunction Function)
(subclass BinaryFunction TernaryRelation)
(instance BinaryFunction InheritableRelation)
(documentation BinaryFunction "The &%Class of &%Functions that require 
two arguments.")

(=>
	(instance ?FUNCTION BinaryFunction)
	(valence ?FUNCTION 2))

(subclass AssociativeFunction BinaryFunction)
(documentation AssociativeFunction "A &%BinaryFunction is associative if 
bracketing has no effect on the value returned by the &%Function.  More 
precisely, a &%Function ?FUNCTION is associative just in case 
(?FUNCTION ?INST1 (?FUNCTION ?INST2 ?INST3)) is equal to 
(?FUNCTION (?FUNCTION ?INST1 ?INST2) ?INST3), for all ?INST1, ?INST2, 
and ?INST3.")

(=>
   (instance ?FUNCTION AssociativeFunction)
   (forall (?INST1 ?INST2 ?INST3)
      (=>
         (and
            (domain ?FUNCTION 1 ?CLASS)
            (instance ?INST1 ?CLASS)
            (instance ?INST2 ?CLASS)
            (instance ?INST3 ?CLASS))
         (equal (AssignmentFn ?FUNCTION ?INST1 (AssignmentFn ?FUNCTION ?INST2 ?INST3))
             (AssignmentFn ?FUNCTION (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?INST3)))))

(subclass CommutativeFunction BinaryFunction)
(documentation CommutativeFunction "A &%BinaryFunction is commutative if 
the ordering of the arguments of the function has no effect on the value 
returned by the function.  More precisely, a function ?FUNCTION is 
commutative just in case (?FUNCTION ?INST1 ?INST2) is equal to (?FUNCTION 
?INST2 ?INST1), for all ?INST1 and ?INST2.")

(=>
   (instance ?FUNCTION CommutativeFunction)
   (forall (?INST1 ?INST2)
      (=>
         (and
            (domain ?FUNCTION 1 ?CLASS)
            (instance ?INST1 ?CLASS)
            (instance ?INST2 ?CLASS))
         (equal (AssignmentFn ?FUNCTION ?INST1 ?INST2) 
                (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))

(subclass TernaryFunction Function)
(subclass TernaryFunction QuaternaryRelation)
(instance TernaryFunction InheritableRelation)
(documentation TernaryFunction "The &%Class of &%Functions that require 
exactly three arguments.")

(=>
	(instance ?FUNCTION TernaryFunction)
	(valence ?FUNCTION 3))

(subclass QuaternaryFunction Function)
(subclass QuaternaryFunction QuintaryRelation)
(instance QuaternaryFunction InheritableRelation)
(documentation QuaternaryFunction "The &%Class of &%Functions that require 
exactly four arguments.")

(=>
	(instance ?FUNCTION QuaternaryFunction)
	(valence ?FUNCTION 4))

(subclass ContinuousFunction Function)
(documentation ContinuousFunction "&%Functions which are continuous.  
This concept is taken as primitive until representations for limits 
are devised.")

(subclass LogicalOperator Predicate)
(documentation LogicalOperator "This &%Class currently comprises all 
of the logical operators (viz. 'and', 'or', 'not', '=>', and '<=>').")

(subclass BinaryPredicate Predicate)
(subclass BinaryPredicate BinaryRelation)
(instance BinaryPredicate InheritableRelation)
(documentation BinaryPredicate "A &%Predicate relating two items - its 
valence is two.")

(=>
	(instance ?REL BinaryPredicate)
	(valence ?REL 2))

(subclass TernaryPredicate Predicate)
(subclass TernaryPredicate TernaryRelation)
(instance TernaryPredicate InheritableRelation)
(documentation TernaryPredicate "The &%Class of &%Predicates that require 
exactly three arguments.")

(=>
	(instance ?REL TernaryPredicate)
	(valence ?REL 3))

(subclass QuaternaryPredicate Predicate)
(subclass QuaternaryPredicate QuaternaryRelation)
(instance QuaternaryPredicate InheritableRelation)
(documentation QuaternaryPredicate "The &%Class of &%Predicates that 
require four arguments.")

(=>
	(instance ?REL QuaternaryPredicate)
	(valence ?REL 4))

(subclass QuintaryPredicate Predicate)
(subclass QuintaryPredicate QuintaryRelation)
(instance QuintaryPredicate InheritableRelation)
(documentation QuintaryPredicate "The &%Class of &%Predicates that 
require five arguments.")

(=>
	(instance ?REL QuintaryPredicate)
	(valence ?REL 5))

(subclass VariableArityRelation Relation)
(documentation VariableArityRelation "The &%Class of &%Relations that 
do not have a fixed number of arguments.")

(=>
        (instance ?REL VariableArityRelation)
        (not
           (exists (?INT)
              (valence ?REL ?INT))))

(subclass RelationExtendedToQuantities Relation)
(instance RelationExtendedToQuantities InheritableRelation)
(documentation RelationExtendedToQuantities "A 
&%RelationExtendedToQuantities is a &%Relation that, when it is true on 
a sequence of arguments that are &%RealNumbers, it is also true on a 
sequence of &%ConstantQuantites with those magnitudes in some unit of 
measure.  For example, the &%lessThan relation is extended to quantities.  
This means that for all pairs of quantities ?QUANTITY1 and ?QUANTITY2, 
(lessThan ?QUANTITY1 ?QUANTITY2) if and only if, for some ?NUMBER1, 
?NUMBER2, and ?UNIT, ?QUANTITY1 = (MeasureFn ?NUMBER1 ?UNIT), 
?QUANTITY2 = (MeasureFn ?NUMBER2 ?UNIT), and (lessThan ?NUMBER1 ?NUMBER2), 
for all units ?UNIT on which ?QUANTITY1 and ?QUANTITY2 can be measured.  
Note that, when a &%RelationExtendedToQuantities is extended from 
&%RealNumbers to &%ConstantQuantities, the &%ConstantQuantities must be 
measured along the same physical dimension.")

(subclass Proposition Abstract)
(documentation Proposition "&%Propositions are &%Abstract entities that 
express a complete thought or a set of such thoughts.  As an example, 
the formula '(instance Yojo Cat)' expresses the &%Proposition that the 
entity named Yojo is an element of the &%Class of Cats.  Note that 
propositions are not restricted to the content expressed by individual 
sentences of a &%Language.  They may encompass the content expressed by 
theories, books, and even whole libraries.  It is important to distinguish 
&%Propositions from the &%ContentBearingObjects that express them.  A 
&%Proposition is a piece of information, e.g. that the cat is on the mat, 
but a &%ContentBearingObject is an &%Object that represents this information.  
A &%Proposition is an abstraction that may have multiple representations: 
strings, sounds, icons, etc.  For example, the &%Proposition that the cat is 
on the mat is represented here as a string of graphical characters displayed 
on a monitor and/or printed on paper, but it can be represented by a sequence 
of sounds or by some non-latin alphabet or by some cryptographic form")

(instance closedOn BinaryPredicate)
(instance closedOn AsymmetricRelation)
(domain closedOn 1 Function)
(domain closedOn 2 SetOrClass)
(documentation closedOn "A &%BinaryFunction is closed on a &%SetOrClass 
if it is defined for all instances of the &%SetOrClass and its value is 
always an instance of the &%SetOrClass.")

(=>
   (and
      (closedOn ?FUNCTION ?CLASS)
      (instance ?FUNCTION UnaryFunction))
   (forall (?INST)
      (=> 
         (instance ?INST ?CLASS) 
         (instance (AssignmentFn ?FUNCTION ?INST) ?CLASS))))

(=>
   (and
      (closedOn ?FUNCTION ?CLASS)
      (instance ?FUNCTION BinaryFunction))
   (forall (?INST1 ?INST2)
      (=> 
         (and 
            (instance ?INST1 ?CLASS) 
            (instance ?INST2 ?CLASS))
         (instance (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?CLASS))))

(instance reflexiveOn BinaryPredicate)
(instance reflexiveOn AsymmetricRelation)
(domain reflexiveOn 1 BinaryRelation)
(domain reflexiveOn 2 SetOrClass)
(documentation reflexiveOn "A &%BinaryRelation is reflexive on a 
&%SetOrClass only if every instance of the &%SetOrClass bears the relation 
to itself.")

(=> 
   (reflexiveOn ?RELATION ?CLASS)
   (forall (?INST)
      (=> 
         (instance ?INST ?CLASS)
         (holds ?RELATION ?INST ?INST))))

(instance irreflexiveOn BinaryPredicate)
(instance irreflexiveOn AsymmetricRelation)
(domain irreflexiveOn 1 BinaryRelation)
(domain irreflexiveOn 2 SetOrClass)
(documentation irreflexiveOn "A &%BinaryRelation is irreflexive on a 
&%SetOrClass only if no instance of the &%SetOrClass bears the relation to 
itself.")

(=> 
   (irreflexiveOn ?RELATION ?CLASS)
   (forall (?INST)
      (=> 
         (instance ?INST ?CLASS)
         (not 
            (holds ?RELATION ?INST ?INST)))))

(instance partialOrderingOn BinaryPredicate)
(instance partialOrderingOn AsymmetricRelation)
(domain partialOrderingOn 1 BinaryRelation)
(domain partialOrderingOn 2 SetOrClass)
(documentation partialOrderingOn "A &%BinaryRelation is a partial 
ordering on a &%SetOrClass only if the relation is &%reflexiveOn the 
&%SetOrClass, and it is both an &%AntisymmetricRelation, and a 
&%TransitiveRelation.")

(=> 
   (partialOrderingOn ?RELATION ?CLASS)
   (and 
      (reflexiveOn ?RELATION ?CLASS)
      (instance ?RELATION TransitiveRelation)
      (instance ?RELATION AntisymmetricRelation)))

(instance totalOrderingOn BinaryPredicate)
(instance totalOrderingOn AsymmetricRelation)
(domain totalOrderingOn 1 BinaryRelation)
(domain totalOrderingOn 2 SetOrClass)
(documentation totalOrderingOn "A &%BinaryRelation ?REL is a total 
ordering on a &%SetOrClass only if it is a partial ordering for which either 
(?REL ?INST1 ?INST2) or (?REL ?INST2 ?INST1) for every ?INST1 and ?INST2 
in the &%SetOrClass.")

(<=> 
     (totalOrderingOn ?RELATION ?CLASS)
     (and 
          (partialOrderingOn ?RELATION ?CLASS)
          (trichotomizingOn ?RELATION ?CLASS)))

(instance trichotomizingOn BinaryPredicate)
(instance trichotomizingOn AsymmetricRelation)
(domain trichotomizingOn 1 BinaryRelation)
(domain trichotomizingOn 2 SetOrClass)
(documentation trichotomizingOn "A &%BinaryRelation ?REL is 
trichotomizing on a &%SetOrClass only if, for all instances ?INST1 and ?INST2 
of the &%SetOrClass, at least one of the following holds:  (?REL ?INST1 ?INST2),
(?REL ?INST2 ?INST1) or (equal ?INST1 ?INST2).")

(=>
   (trichotomizingOn ?RELATION ?CLASS)
   (forall (?INST1 ?INST2)
      (=> 
         (and 
            (instance ?INST1 ?CLASS)
            (instance ?INST2 ?CLASS))
         (or 
            (holds ?RELATION ?INST1 ?INST2) 
            (holds ?RELATION ?INST2 ?INST1) 
            (equal ?INST1 ?INST2)))))

(instance equivalenceRelationOn BinaryPredicate)
(instance equivalenceRelationOn AsymmetricRelation)
(domain equivalenceRelationOn 1 BinaryRelation)
(domain equivalenceRelationOn 2 SetOrClass)
(documentation equivalenceRelationOn "A &%BinaryRelation is an 
&%equivalenceRelationOn a &%SetOrClass only if the relation is &%reflexiveOn 
the &%SetOrClass and it is both a &%TransitiveRelation and a 
&%SymmetricRelation.")

(=>
   (equivalenceRelationOn ?RELATION ?CLASS)
   (and
      (instance ?RELATION TransitiveRelation)
      (instance ?RELATION SymmetricRelation)
      (reflexiveOn ?RELATION ?CLASS))) 

(instance distributes BinaryPredicate)
(instance distributes BinaryRelation)
(domain distributes 1 BinaryFunction)
(domain distributes 2 BinaryFunction)
(documentation distributes "A &%BinaryFunction ?FUNCTION1 is 
distributive over another &%BinaryFunction ?FUNCTION2 just in case 
(?FUNCTION1 ?INST1 (?FUNCTION2 ?INST2 ?INST3)) is equal to 
(?FUNCTION2 (?FUNCTION1 ?INST1 ?INST2) (?FUNCTION1 ?INST1 ?INST3)), 
for all ?INST1, ?INST2, and ?INST3.") 

(=>
   (distributes ?FUNCTION1 ?FUNCTION2)
   (forall (?INST1 ?INST2 ?INST3)
      (=>
         (and
            (domain ?FUNCTION1 1 ?CLASS1)
            (instance ?INST1 ?CLASS1)
            (instance ?INST2 ?CLASS1)
            (instance ?INST3 ?CLASS1)
            (domain ?FUNCTION2 1 ?CLASS2)
            (instance ?INST1 ?CLASS2)
            (instance ?INST2 ?CLASS2)
            (instance ?INST3 ?CLASS2))
         (equal (AssignmentFn ?FUNCTION1 ?INST1 
                        (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                (AssignmentFn ?FUNCTION2 
                        (AssignmentFn ?FUNCTION1 ?INST1 ?INST2) 
                        (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))

(instance causes BinaryPredicate)
(instance causes AsymmetricRelation)
(domain causes 1 Process)
(domain causes 2 Process)
(relatedInternalConcept causes causesSubclass)
(documentation causes "The causation relation between instances of &%Process.  
(&%causes ?PROCESS1 ?PROCESS2) means that the instance of &%Process ?PROCESS1 
brings about the instance of &%Process ?PROCESS2, e.g. (&%causes &%Killing &%Death).")

(=>
   (instance ?PROC1 Process)
   (exists (?PROC2)
      (causes ?PROC2 ?PROC1)))

(instance causesSubclass BinaryPredicate)
(instance causesSubclass AsymmetricRelation)
(domainSubclass causesSubclass 1 Process)
(domainSubclass causesSubclass 2 Process)
(documentation causesSubclass "The causation relation between subclasses of &%Process.  
(&%causesSubclass ?PROCESS1 ?PROCESS2) means that the subclass of &%Process ?PROCESS1 
brings about the subclass of &%Process ?PROCESS2, e.g. (&%causes &%Killing &%Death).")

(=>
   (causesSubclass ?PROC1 ?PROC2)
   (forall (?INST2)
      (=>
         (instance ?INST2 ?PROC2)
         (exists (?INST1) 
		(and
		   (instance ?INST1 ?PROC1)
		   (causes ?INST1 ?INST2))))))

(instance copy BinaryPredicate)
(instance copy EquivalenceRelation)
(domain copy 1 Object)
(domain copy 2 Object)
(documentation copy "relates an &%Object to an exact copy of the 
&%Object, where an exact copy is indistinguishable from the original 
with regard to every property except (possibly) spatial and/or temporal 
location.")

(=>
   (copy ?OBJ1 ?OBJ2)
   (forall (?ATTR)
      (=>
         (attribute ?OBJ1 ?ATTR)
         (attribute ?OBJ2 ?ATTR))))

(instance time BinaryPredicate)
(instance time TemporalRelation)
(instance time AsymmetricRelation)
(domain time 1 Physical)
(domain time 2 TimePosition)
(documentation time "This relation holds between an instance of 
&%Physical and an instance of &%TimePosition just in case the temporal 
lifespan of the former includes the latter.  The constants &%located 
and &%time are the basic spatial and temporal predicates, 
respectively.")

(instance holdsDuring BinaryPredicate)
(instance holdsDuring AsymmetricRelation)
(domain holdsDuring 1 TimePosition)
(domain holdsDuring 2 Formula)
(documentation holdsDuring "(&%holdsDuring ?TIME ?FORMULA) means that the 
proposition denoted by ?FORMULA is true in the time frame ?TIME.  Note 
that this implies that ?FORMULA is true at every &%TimePoint which is a 
&%temporalPart of ?TIME.")

(=>
   (and
      (holdsDuring ?TIME ?SITUATION1)
      (entails ?SITUATION1 ?SITUATION2))
   (holdsDuring ?TIME ?SITUATION2))

(=>
   (holdsDuring ?TIME (not ?SITUATION))
   (not (holdsDuring ?TIME ?SITUATION)))

(instance capability TernaryPredicate)
(domainSubclass capability 1 Process)
(domain capability 2 CaseRole)
(domain capability 3 Object)
(documentation capability "(&%capability ?PROCESS ?ROLE ?OBJ) means 
that ?OBJ has the ability to play the role of ?ROLE in &%Processes of 
type ?PROCESS.")

(=>
   (and
      (instance ?ROLE CaseRole)
      (holds ?ROLE ?ARG1 ?ARG2)
      (instance ?ARG1 ?PROC)
      (subclass ?PROC Process))
   (capability ?PROC ?ROLE ?ARG2))

(instance exploits BinaryPredicate)
(instance exploits AsymmetricRelation)
(domain exploits 1 Object)
(domain exploits 2 Agent)
(documentation exploits "(&%exploits ?OBJ ?AGENT) means that ?OBJ is used 
by ?AGENT as a &%resource in an unspecified instance of &%Process.  This 
&%Predicate, as its corresponding axiom indicates, is a composition of the 
relations &%agent and &%resource.")

(=>
     (exploits ?OBJ ?AGENT)
     (exists (?PROCESS)
          (and
               (agent ?PROCESS ?AGENT)
               (resource ?PROCESS ?OBJ)))) 

(instance hasPurpose BinaryPredicate)
(instance hasPurpose AsymmetricRelation)
(domain hasPurpose 1 Physical)
(domain hasPurpose 2 Formula)
(documentation hasPurpose "This &%Predicate expresses the concept of a 
conventional goal, i.e. a goal with a neutralized agent's intention.  
Accordingly, (&%hasPurpose ?THING ?FORMULA) means that the instance of 
&%Physical ?THING has, as its purpose, the &%Proposition expressed by 
?FORMULA.  Note that there is an important difference in meaning between 
the &%Predicates &%hasPurpose and &%result.  Although the second argument 
of the latter can satisfy the second argument of the former, 
a conventional goal is an expected and desired outcome, while a result 
may be neither expected nor desired.  For example, a machine process may 
have outcomes but no goals, aimless wandering may have an outcome but no 
goal; a learning process may have goals with no outcomes, and so on.")

(instance hasPurposeForAgent TernaryPredicate)
(domain hasPurposeForAgent 1 Physical)
(domain hasPurposeForAgent 2 Formula)
(domain hasPurposeForAgent 3 CognitiveAgent)
(documentation hasPurposeForAgent "Expresses a cognitive attitude of an 
agent with respect to a particular instance of Physical.  More precisely, 
(&%hasPurposeForAgent ?THING ?FORMULA ?AGENT) means that the purpose of 
?THING for ?AGENT is the proposition expressed by ?FORMULA.  Very complex 
issues are involved here.  In particular, the rules of inference of the 
first order predicate calculus are not truth-preserving for the second 
argument position of this &%Predicate.")

(=>
   (hasPurpose ?THING ?PURPOSE)
   (exists (?AGENT)
      (hasPurposeForAgent ?THING ?PURPOSE ?AGENT)))

(instance hasSkill BinaryPredicate)
(instance hasSkill AsymmetricRelation)
(domainSubclass hasSkill 1 Process)
(domain hasSkill 2 Agent)
(documentation hasSkill "Similar to the &%capability &%Predicate 
with the additional restriction that the ability be practised/
demonstrated to some measurable degree.")

(=>
   (hasSkill ?PROC ?AGENT)
   (capability ?PROC agent ?AGENT))

(instance holdsRight BinaryPredicate)
(instance holdsRight AsymmetricRelation)
(domain holdsRight 1 Formula)
(domain holdsRight 2 CognitiveAgent)
(documentation holdsRight "Expresses a relationship between a &%Formula 
and a &%CognitiveAgent whereby the &%CognitiveAgent has the right to 
bring it about that the &%Formula is true.")

(instance confersRight TernaryPredicate)
(domain confersRight 1 Formula)
(domain confersRight 2 Entity)
(domain confersRight 3 CognitiveAgent)
(documentation confersRight "Expresses the relationship between a &%Formula, 
an &%Entity, and a &%CognitiveAgent when the &%Entity authorizes the 
&%CognitiveAgent to bring it about that the &%Formula is true.")

(=>
   (confersRight ?FORMULA ?AGENT1 ?AGENT2)
   (holdsRight ?FORMULA ?AGENT2))

(instance holdsObligation BinaryPredicate)
(instance holdsObligation AsymmetricRelation)
(domain holdsObligation 1 Formula)
(domain holdsObligation 2 CognitiveAgent)
(relatedInternalConcept holdsObligation holdsRight)
(documentation holdsObligation "Expresses a relationship between a 
&%Formula and a &%CognitiveAgent whereby the &%CognitiveAgent has 
the obligation to bring it about that the &%Formula is true.")

(instance confersObligation TernaryPredicate)
(domain confersObligation 1 Formula)
(domain confersObligation 2 Entity)
(domain confersObligation 3 CognitiveAgent)
(relatedInternalConcept confersObligation confersRight)
(documentation confersObligation "Expresses the relationship between a 
a &%Formula, an &%Entity, and a &%CognitiveAgent when the &%Entity 
obligates the &%CognitiveAgent to bring it about that the &%Formula is 
true.")

(=>
   (confersObligation ?FORMULA ?AGENT1 ?AGENT2)
   (holdsObligation ?FORMULA ?AGENT2))

(instance partlyLocated SpatialRelation)
(instance partlyLocated AntisymmetricRelation)
(instance partlyLocated BinaryPredicate)
(domain partlyLocated 1 Physical)
(domain partlyLocated 2 Object)
(documentation partlyLocated "(&%partlyLocated ?THING ?OBJ) means that the 
instance of &%Physical ?THING is at least partially located at ?OBJ.  For 
example, Istanbul is partly located in Asia and partly located in Europe.  
Note that &%partlyLocated is the most basic localization relation:  &%located 
is an immediate &%subrelation of &%partlyLocated and &%exactlyLocated is 
an immediate &%subrelation of &%located.") 

(=>
   (and
      (instance ?OBJ1 Object)
      (partlyLocated ?OBJ1 ?OBJ2))
   (overlapsSpatially ?OBJ1 ?OBJ2)) 

(=>
   (and
      (instance ?OBJ1 Object)
      (partlyLocated ?OBJ1 ?OBJ2))
   (exists (?SUB)
      (and
         (part ?SUB ?OBJ1)
         (located ?SUB ?OBJ2))))

(instance located AntisymmetricRelation)
(instance located TransitiveRelation)
(subrelation located partlyLocated)
(documentation located "(&%located ?PHYS ?OBJ) means that ?PHYS is &%partlyLocated 
at ?OBJ, and there is no &%part or &%subProcess of ?PHYS that is not &%located at 
?OBJ.")

(=>
   (located ?OBJ1 ?OBJ2)
   (forall (?SUB)
      (=>
         (part ?SUB ?OBJ1)
         (located ?SUB ?OBJ2))))

(=>
   (located ?PROCESS ?OBJ)
   (forall (?SUB)
      (=>
         (subProcess ?SUB ?PROCESS)
         (located ?SUB ?OBJ))))

(subrelation exactlyLocated located)
(documentation exactlyLocated "The actual, minimal location of an 
Object.  This is a subrelation of the more general &%Predicate 
&%located.")

(=>
   (exactlyLocated ?OBJ ?REGION)
   (not
      (exists (?OTHEROBJ)
         (and
            (exactlyLocated ?OTHEROBJ ?REGION)
            (not
               (equal ?OTHEROBJ ?OBJ))))))

(instance between SpatialRelation)
(instance between TernaryPredicate)
(domain between 1 Object)
(domain between 2 Object)
(domain between 3 Object)
(documentation between "(between ?OBJ1 ?OBJ2 ?OBJ3) means that ?OBJ2 is 
spatially located between ?OBJ1 and ?OBJ3.  Note that this implies that 
?OBJ2 is directly between ?OBJ1 and ?OBJ3, i.e. the projections of ?OBJ1 
and ?OBJ3 overlap with ?OBJ2.")

(instance traverses SpatialRelation)
(domain traverses 1 Object)
(domain traverses 2 Object)
(documentation traverses "(&%traverses ?OBJ1 ?OBJ2) means that ?OBJ1 
crosses or extends across ?OBJ2.  Note that &%crosses and 
&%penetrates are subrelations of &%traverses.")

(=>
   (traverses ?OBJ1 ?OBJ2)
   (or
      (crosses ?OBJ1 ?OBJ2)
      (penetrates ?OBJ1 ?OBJ2)))

(subrelation crosses traverses)
(instance crosses AsymmetricRelation)
(instance crosses TransitiveRelation)
(disjointRelation crosses connected)
(documentation crosses "(crosses ?OBJ1 ?OBJ2) means that 
&%Object ?OBJ1 &%traverses Object ?OBJ2, without being &%connected 
to it.")

(subrelation penetrates traverses)
(subrelation penetrates meetsSpatially)
(instance penetrates AsymmetricRelation)
(instance penetrates IntransitiveRelation)
(documentation penetrates "(penetrates ?OBJ1 ?OBJ2) means that 
?OBJ1 is &%connected to ?OBJ2 along at least one whole dimension (length, 
width or depth).") 

(instance WhereFn BinaryFunction)
(instance WhereFn SpatialRelation)
(instance WhereFn TotalValuedRelation)
(domain WhereFn 1 Physical)
(domain WhereFn 2 TimePoint)
(range WhereFn Region)
(relatedInternalConcept WhereFn WhenFn)
(documentation WhereFn "Maps an &%Object and a &%TimePoint at which the 
&%Object exists to the &%Region where the &%Object existed at that 
&%TimePoint.")

(<=>
   (equal (WhereFn ?THING ?TIME) ?REGION)
   (holdsDuring ?TIME (exactlyLocated ?THING ?REGION)))

(instance possesses BinaryPredicate)
(instance possesses AsymmetricRelation)
(domain possesses 1 Agent)
(domain possesses 2 Object)
(documentation possesses "&%Relation that holds between an &%Agent and 
an &%Object when the &%Agent has ownership of the &%Object.")

(=>
   (possesses ?PERSON ?OBJ)
   (holdsRight (uses ?OBJ ?PERSON) ?PERSON))

(=>
   (and
      (instance ?TIME TimePosition)
      (holdsDuring ?TIME (possesses ?AGENT1 ?OBJ))
      (holdsDuring ?TIME (possesses ?AGENT2 ?OBJ)))
   (equal ?AGENT1 ?AGENT2))

(instance PropertyFn UnaryFunction)
(instance PropertyFn TotalValuedRelation)
(domain PropertyFn 1 Agent)
(range PropertyFn Set)
(documentation PropertyFn "A &%UnaryFunction that maps an &%Agent to the &%Set of &%Property owned by the &%Agent.")

(<=> 
   (instance ?OBJ (PropertyFn ?PERSON))
   (possesses ?PERSON ?OBJ))

(instance precondition BinaryPredicate)
(instance precondition AsymmetricRelation)
(instance precondition TransitiveRelation)
(domainSubclass precondition 1 Process)
(domainSubclass precondition 2 Process)
(documentation precondition "A very general &%Predicate.  (&%precondition 
?PROC1 ?PROC2) means that an instance of ?PROC2 can exist only if an 
instance of ?PROC1 also exists.")

(=>
   (precondition ?PROC1 ?PROC2)
   (=>
      (exists (?INST2) (instance ?INST2 ?PROC2))
      (exists (?INST1) (instance ?INST1 ?PROC1))))

(instance inhibits BinaryPredicate)
(instance inhibits IrreflexiveRelation)
(domainSubclass inhibits 1 Process)
(domainSubclass inhibits 2 Process)
(documentation inhibits "A very general &%Predicate.  (&%inhibits 
?PROC1 ?PROC2) means that the &%Process ?PROC1 inhibits or hinders 
the occurrence of the &%Process ?PROC2.  For example, obstructing an 
object inhibits moving it.  Note that this is a relation between types 
of &%Processes, not between instances.")

(=>
   (inhibits ?PROC1 ?PROC2)
   (forall (?TIME ?PLACE)
      (decreasesLikelihood 
		(holdsDuring ?TIME (exists (?INST1) (and (instance ?INST1 ?PROC1) (located ?INST1 ?PLACE))))
            (holdsDuring ?TIME (exists (?INST2) (and (instance ?INST2 ?PROC2) (located ?INST2 ?PLACE)))))))

(instance prevents BinaryPredicate)
(instance prevents IrreflexiveRelation)
(domainSubclass prevents 1 Process)
(domainSubclass prevents 2 Process)
(relatedInternalConcept prevents inhibits)
(documentation prevents "A very general &%Predicate.  (&%prevents ?PROC1 
?PROC2) means that ?PROC1 prevents the occurrence of ?PROC2.  In other 
words, if ?PROC1 is occurring in a particular time and place, ?PROC2 
cannot occur at the same time and place.  For example, innoculating 
prevents contracting disease.  Note that this is a relation between types 
of &%Processes, not between instances.") 

(=>
   (prevents ?PROC1 ?PROC2)
   (forall (?TIME ?PLACE)
      (=>
         (holdsDuring ?TIME (exists (?INST1) (and (instance ?INST1 ?PROC1) (located ?INST1 ?PLACE))))
         (not (holdsDuring ?TIME (exists (?INST2) (and (instance ?INST2 ?PROC2) (located ?INST2 ?PLACE))))))))

(instance refers BinaryPredicate)
(domain refers 1 Physical)
(domain refers 2 Entity)
(documentation refers "(&%refers ?OBJ1 ?OBJ2) means that ?OBJ1 
mentions or includes a reference to ?OBJ2. Note that &%refers is 
more general in meaning than &%represents, because presumably something 
can represent something else only if it refers to this other thing.  
For example, an article whose topic is a recent change in the price of 
oil may refer to many other things, e.g. the general state of the economy, 
the weather in California, the prospect of global warming, the options 
for alternative energy sources, the stock prices of various oil companies, 
etc.")

(subrelation names refers)
(domain names 1 SymbolicString)
(documentation names "(&%names ?STRING ?ENTITY) means that the thing ?ENTITY 
has the &%SymbolicString ?STRING as its name.  Note that &%names and &%represents 
are the two immediate &%subrelations of &%refers.  The predicate &%names is used 
when the referring item is merely a tag without connotative content, while the 
predicate &%represents is used for referring items that have such content.")

(subrelation uniqueIdentifier names)
(instance uniqueIdentifier SingleValuedRelation)
(documentation uniqueIdentifier "The class of &%names that uniquely identify 
an instance of &%Entity.  Some examples of &%uniqueIdentifiers are the keys 
of tables in database applications and the ISBN (International Standard Book 
Number).")

(subrelation represents refers)
(documentation represents "A very general semiotics &%Predicate.  
(&%represents ?THING ?ENTITY) means that ?THING in some way indicates, 
expresses, connotes, pictures, describes, etc. ?ENTITY.  The &%Predicates 
&%containsInformation and &%realization are subrelations of &%represents.  
Note that &%represents is a subrelation of &%refers, since something can 
represent something else only if it refers to this other thing.  See the 
documentation string for &%names.") 

(instance representsForAgent TernaryPredicate)
(domain representsForAgent 1 Physical)
(domain representsForAgent 2 Entity)
(domain representsForAgent 3 Agent)
(documentation representsForAgent "A very general predicate.  
(&%representsForAgent ?THING ?ENTITY ?AGENT) means that the ?AGENT 
chooses to use the &%instance of &%Physical ?THING to 'stand for' 
?ENTITY.")

(=>
   (representsForAgent ?REP ?ENTITY ?AGENT)
   (represents ?REP ?ENTITY))

(instance representsInLanguage TernaryPredicate)
(domain representsInLanguage 1 LinguisticExpression)
(domain representsInLanguage 2 Entity)
(domain representsInLanguage 3 Language)
(documentation representsInLanguage "A very general predicate.  
(&%representsInLanguage ?THING ?ENTITY ?LANGUAGE) means that the 
&%LinguisticExpression ?THING stands for ?ENTITY in the &%Language 
?LANGUAGE.")

(=>
   (representsInLanguage ?REP ?ENTITY ?LANGUAGE)
   (exists (?AGENT)
      (representsForAgent ?REP ?ENTITY ?AGENT)))

(subrelation equivalentContentClass subsumesContentClass)
(instance equivalentContentClass EquivalenceRelation)
(domainSubclass equivalentContentClass 1 ContentBearingObject)
(domainSubclass equivalentContentClass 2 ContentBearingObject)
(documentation equivalentContentClass "A &%BinaryPredicate that relates two 
subclasses of &%ContentBearingObject.  (&%equivalentContentClass ?CLASS1 
?CLASS2) means that the content expressed by each instance of ?CLASS1 is 
also expressed by each instance of ?CLASS2, and vice versa.  An example 
would be the relationship between English and Russian editions of Agatha 
Christie's 'Murder on the Orient Express'.  Note that 
(&%equivalentContentClass ?CLASS1 ?CLASS2) implies (&%subsumesContentClass 
?CLASS1 ?CLASS2) and (&%subsumesContentClass ?CLASS2 ?CLASS1).")

(<=>
   (and
      (subsumesContentClass ?CLASS1 ?CLASS2)
      (subsumesContentClass ?CLASS2 ?CLASS1))
   (equivalentContentClass ?CLASS1 ?CLASS2))

(instance subsumesContentClass BinaryPredicate)
(instance subsumesContentClass PartialOrderingRelation)
(domainSubclass subsumesContentClass 1 ContentBearingObject)
(domainSubclass subsumesContentClass 2 ContentBearingObject)
(documentation subsumesContentClass "A &%BinaryPredicate that relates two 
subclasses of &%ContentBearingObject.  (&%subsumesContentClass ?CLASS1 
?CLASS2) means that the content expressed by each instance of ?CLASS2 is 
also expressed by each instance of ?CLASS1.  Examples include the 
relationship between a poem and one of its stanzas or between a book and 
one of its chapters.  Note that this is a relation between subclasses of 
&%ContentBearingObject, rather than instances.  If one wants to relate 
instances, the &%Predicate &%subsumesContentInstance can be used.  Note 
that &%subsumesContentClass is needed in many cases.  Consider, for 
example, the relation between the King James edition of the Bible and its 
Book of Genesis.  This relation holds for every copy of this edition and 
not just for a single instance.")

(=>
   (subsumesContentClass ?CLASS1 ?CLASS2)
   (forall (?OBJ2 ?INFO)
      (=>
         (and
	      (instance ?OBJ2 ?CLASS2)
            (containsInformation ?OBJ2 ?INFO))
         (exists (?OBJ1)
            (and
               (instance ?OBJ1 ?CLASS1)
               (containsInformation ?OBJ1 ?INFO))))))

(subrelation equivalentContentInstance subsumesContentInstance)
(instance equivalentContentInstance EquivalenceRelation)
(domain equivalentContentInstance 1 ContentBearingObject)
(domain equivalentContentInstance 2 ContentBearingObject)
(relatedInternalConcept equivalentContentInstance equivalentContentClass)
(documentation equivalentContentInstance "A &%BinaryPredicate relating two 
instances of &%ContentBearingObject.  (&%equivalentContentInstance 
?OBJ1 ?OBJ2) means that the content expressed by ?OBJ1 is identical to 
the content expressed by ?OBJ2.  An example would be the relationship 
between a handwritten draft of a letter to one's lawyer and a typed 
copy of the same letter.  Note that (&%equivalentContentInstance ?OBJ1 
?OBJ2) implies (&%subsumesContentInstance ?OBJ1 ?OBJ2) and 
(&%subsumesContentInstance ?OBJ2 ?OBJ2).")

(<=>
   (and
      (subsumesContentInstance ?OBJ1 ?OBJ2)
      (subsumesContentInstance ?OBJ2 ?OBJ1))
   (equivalentContentInstance ?OBJ1 ?OBJ2))

(instance subsumesContentInstance BinaryPredicate)
(instance subsumesContentInstance PartialOrderingRelation)
(domain subsumesContentInstance 1 ContentBearingObject)
(domain subsumesContentInstance 2 ContentBearingObject)
(relatedInternalConcept subsumesContentInstance subsumesContentClass)
(documentation subsumesContentInstance "A &%BinaryPredicate relating two 
instances of &%ContentBearingObject.  (&%subsumesContentInstance ?OBJ1 ?OBJ2) 
means that the content expr