instance (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.

Ontologie

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

třída

inheritable relation

binární predikát

instance

Subrelation(s)

immediate instance element

Související termín(y)

arc weight authors before or equal causes causes subclass citizen closed on connected contains information cooccur copy date decreases likelihood developmental form disjoint distributes documentation duration earlier editor element employs equal equivalence relation on exploits expressed in language faces family relation finishes frequency graph part greater than greater than or equal to has purpose has skill holds during holds obligation holds right hole identity element in list in scope of interest increases likelihood independent probability inhabits inhibits initial list inverse irreflexive on larger less than less than or equal to material measure meets temporally modal attribute overlaps temporally parent partial ordering on partly located path length possesses precondition prevents property publishes range range subclass refers reflexive on related internal concept sibling smaller starts sub attribute sub collection sub graph sub list sub process sub proposition subclass subrelation subsumes content class subsumes content instance successor attribute successor attribute closure temporal part time total ordering on trichotomizing on uses valence version

Typy argumentů

instance(entita, množina nebo třída)

Related WordNet synsets

member: anything that belongs to a set or class: "snakes are members of the class Reptilia"; "members of the opposite sex"
be: have the quality of being; (copula, used with an adjective or a predicate noun); "John is rich"; "This is not a good answer"

See more related synsets on a separate page.

Axiomy (537)

Jestliže immediate instance(entity,class) platí, potom neexistuje class subclass tak, že entity je instancí třídy subclass.

(=>
      (immediateInstance ?ENTITY ?CLASS)
      (not
            (exists
                  (?SUBCLASS)
                  (and
                        (subclass ?SUBCLASS ?CLASS)
                        (instance ?ENTITY ?SUBCLASS)))))

subclass je podtřídou class tehdy a jen tehdy pokud

subclass je instancí třídy množina nebo třída
class je instancí třídy množina nebo třída
pro všechny inst platí: jestliže inst je instancí třídy subclass, potom inst je instancí třídy class

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

Jestliže pred1 je a subrelation of pred2 a pred2 je instancí třídy class a class je instancí třídy inheritable relation, potom pred1 je instancí třídy class.

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

Jestliže thing1 se rovná thing2, potom pro všechny class platí: thing1 je instancí třídy class tehdy a jen tehdy pokud thing2 je instancí třídy class.

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

Jestliže class1 se rovná class2, potom pro všechny thing platí: thing je instancí třídy class1 tehdy a jen tehdy pokud thing je instancí třídy class2.

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

Jestliže range of function je an instance of class a "function()" se rovná value, potom value je instancí třídy class.

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

class1 je disjoint from class2 tehdy a jen tehdy pokud

class1 je instancí třídy množina nebo třída
class2 je instancí třídy množina nebo třída
pro všechny inst platí: inst není instancí třídy class1 nebo inst není instancí třídy class2

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

Jestliže and ? are disjoint a rel je a member of "()", potom rel je instancí třídy relace.

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

jestliže contrary attribute() platí,
potom jestliže element je a member of "()", potom element je instancí třídy atribut

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

jestliže exhaustive attribute(class,) platí,
potom jestliže attr je a member of "()", potom attr je instancí třídy atribut

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

jestliže exhaustive attribute(class,) platí,
potom pro všechny obj platí: jestliže attr1 je instancí třídy class, potom existuje attr2 tak, že attr2 je a member of "()" a attr1 se rovná attr2

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

jestliže je covered by ,
potom jestliže element je a member of "()", potom element je instancí třídy třída

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

jestliže je disjointly decomposed into ,
potom jestliže element je a member of "()", potom element je instancí třídy třída

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

Jestliže attr1 je a subattribute of attr2 a attr2 je instancí třídy class, potom attr1 je instancí třídy class.

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

Jestliže rel(,inst) holds a rel je instancí třídy funkce, potom "rel()" se rovná inst.

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

Existuje thing tak, že thing je instancí třídy entita.

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

Jestliže class je instancí třídy třída, potom class je podtřídou entita.

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

phys je instancí třídy fyzický objekt tehdy a jen tehdy pokud existují loc,time tak, že phys je located at loc a phys exists during time.

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

Jestliže obj je instancí třídy spojitý objekt, potom "front fn(obj)" je částí obj.

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

Jestliže obj je instancí třídy spojitý objekt, potom "back fn(obj)" je částí obj.

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

jestliže substance1 je a piece of substance2,
potom pro všechny class platí: jestliže substance1 je instancí třídy class, potom substance2 je instancí třídy class

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

Jestliže objecttype je podtřídou látka a object je instancí třídy objecttype a part je částí object, potom part je instancí třídy objecttype.

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

Jestliže obj je instancí třídy látka a attr je atributem obj a part je částí obj, potom attr je atributem part.

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

Jestliže atom je instancí třídy atom, potom existují proton proton,elektron electron tak, že proton je a component of atom a electron je a component of atom.

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

jestliže atom je instancí třídy atom,
potom pro všechny nucleus1,nucleus2 platí: jestliže nucleus1 je a component of atom a nucleus2 je a component of atom a nucleus1 je instancí třídy atomové jádro a nucleus2 je instancí třídy atomové jádro, potom nucleus1 se rovná nucleus2

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

Jestliže particle je instancí třídy subatomická částice, potom existuje atom atom tak, že particle je částí atom.

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

Jestliže nucleus je instancí třídy atomové jádro, potom existují neutron neutron,proton proton tak, že neutron je a component of nucleus a proton je a component of nucleus.

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

Jestliže mixture je instancí třídy směs, potom existují čistá látka pure1,čistá látka pure2 tak, že pure1 se nerovná pure2 a pure1 je a piece of mixture a pure2 je a piece of mixture.

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

Jestliže obj je instancí třídy složený objekt, potom existují látka substance1,látka substance2 tak, že substance1 je z obj a substance2 je z obj a substance1 se nerovná substance2.

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

Jestliže region je instancí třídy oblast, potom existuje phys tak, že phys je located at region.

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

Jestliže coll je instancí třídy kolekce, potom existuje obj tak, že obj je a členem coll.

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

member je internally related to instance.

(relatedInternalConcept member instance)

coll1 je a proper sub-collection of coll2 tehdy a jen tehdy pokud

coll1 je instancí třídy kolekce
coll2 je instancí třídy kolekce
pro všechny member platí: jestliže member je a členem coll1, potom member je a členem coll2

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

Jestliže string je instancí třídy řetězec, potom existuje znak part tak, že part je částí string.

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

Jestliže lang je instancí třídy zvířecí jazyk a agent je původcem proc a lang je nástrojem for proc, potom agent je instancí třídy zvíře a agent není instancí třídy člověk.

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

Jestliže lang je instancí třídy počítačový jazyk a agent je původcem proc a lang je nástrojem for proc, potom agent je instancí třídy stroj.

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

Jestliže lang je instancí třídy lidský jazyk a agent je původcem proc a lang je nástrojem for proc, potom agent je instancí třídy člověk.

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

Jestliže lang je instancí třídy umělý lidský jazyk, potom existuje plánování plan tak, že lang je výsledkem plan.

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

agent je instancí třídy původce tehdy a jen tehdy pokud existuje proc tak, že agent je původcem proc.

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

Jestliže process je instancí třídy proces nad dvěma objekty, potom existují obj1,obj2 tak, že obj1 je účastníkem process a obj2 je účastníkem process a obj1 se nerovná obj2.

(=>
      (instance ?PROCESS DualObjectProcess)
      (exists
            (?OBJ1 ?OBJ2)
            (and
                  (patient ?PROCESS ?OBJ1)
                  (patient ?PROCESS ?OBJ2)
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

abs je instancí třídy abstraktum tehdy a jen tehdy pokud neexistuje point tak, že abs je located at point nebo abs exists during point.

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

"abstraction fn(class)" se rovná attr tehdy a jen tehdy pokud pro všechny inst platí: inst je instancí třídy class tehdy a jen tehdy pokud inst má atribut attr.

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

Jestliže number je instancí třídy imaginární číslo, potom existuje reálné číslo real tak, že number se rovná "real*"square root fn()"".

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

number je instancí třídy nezáporné reálné číslo tehdy a jen tehdy pokud number je větší než nebo roven a number je instancí třídy reálné číslo.

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

number je instancí třídy kladné reálné číslo tehdy a jen tehdy pokud number je větší než a number je instancí třídy reálné číslo.

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

number je instancí třídy záporné reálné číslo tehdy a jen tehdy pokud number je menší než a number je instancí třídy reálné číslo.

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

Jestliže number je instancí třídy komplexní číslo, potom existují reálné číslo real1,reálné číslo real2 tak, že number se rovná "(real1+"real2*"square root fn()"")".

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

Jestliže function je instancí třídy unary constant functionquantity, potom th argument of function je an instance of konstantní veličina a range of function je an instance of konstantní veličina.

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

Jestliže function je instancí třídy časově závislá veličina, potom th argument of function je an instance of časová míra.

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

Jestliže rel je instancí třídy relace, potom rel() holds tehdy a jen tehdy pokud rel() platí.

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

rel je instancí třídy relace s jedinou hodnotou tehdy a jen tehdy pokud pro všechny ,item1,item2 platí: jestliže rel(,item1) holds a rel(,item2) holds, potom item1 se rovná item2.

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

rel je instancí třídy úplná relace tehdy a jen tehdy pokud existuje valence tak, že rel je instancí třídy relace a rel has valence argument(s) a

jestliže pro všechny number,element,class platí: jestliže number je menší než valence a numberth argument of rel je an instance of class a element se rovná "numberth element of "()"", potom element je instancí třídy class,
potom existuje item tak, že rel(,item) holds

(<=>
      (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))))))

Jestliže rel je instancí třídy binární relace, potom neexistují item1,item2,item3, tak, že rel(item1,item2,item3,) holds.

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

jestliže rel je instancí třídy reflexivní relace,
potom jestliže rel(inst1,inst2) holds nebo rel(inst2,inst1) holds, potom rel(inst1,inst1) holds

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

Jestliže rel je instancí třídy ireflexivní relace, potom pro všechny inst platí: rel(inst,inst) doesn't hold.

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

jestliže rel je instancí třídy symetrická relace,
potom pro všechny inst1,inst2 platí: jestliže rel(inst1,inst2) holds, potom rel(inst2,inst1) holds

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

Jestliže

rel je instancí třídy binární relace
th argument of rel je an instance of class1 nebo th argument of rel je a subclass of class1
th argument of rel je an instance of class2 nebo th argument of rel je a subclass of class2 nebo range of rel je an instance of class2 nebo range subclass(rel,class2) platí
class1 je disjoint from class2

, potom rel je instancí třídy nesymetrická relace.

(=>
      (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))

jestliže rel je instancí třídy antisymetrická relace,
potom pro všechny inst1,inst2 platí: jestliže rel(inst1,inst2) holds a rel(inst2,inst1) holds, potom inst1 se rovná inst2

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

Jestliže rel je instancí třídy trichotomická relace, potom pro všechny inst1,inst2 platí: rel(inst1,inst2) holds nebo inst1 se rovná inst2 nebo rel(inst2,inst1) holds.

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

jestliže rel je instancí třídy tranzitivní relace,
potom pro všechny inst1,inst2,inst3 platí: jestliže rel(inst1,inst2) holds a rel(inst2,inst3) holds, potom rel(inst1,inst3) holds

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

jestliže rel je instancí třídy netranzitivní relace,
potom pro všechny inst1,inst2,inst3 platí: jestliže rel(inst1,inst2) holds a rel(inst2,inst3) holds, potom rel(inst1,inst3) doesn't hold

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

Jestliže rel je instancí třídy relace úplné uspořádání, potom pro všechny inst1,inst2 platí: rel(inst1,inst2) holds nebo rel(inst2,inst1) holds.

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

Jestliže process je instancí třídy proces, potom existuje cause tak, že cause je původcem process.

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

Jestliže formula1 je instancí třídy formule a formula2 je instancí třídy formule, potom formula1 increases likelihood of formula2 nebo formula1 decreases likelihood of formula2 nebo probability of formula1 and formula2 je independent.

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

Jestliže rel je instancí třídy intentional relation a rel(agent,) holds a obj je a member of "()", potom agent je interested in obj.

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

Jestliže rel je instancí třídy terciální relace, potom neexistují item1,item2,item3,item4, tak, že rel(item1,item2,item3,item4,) holds.

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

Jestliže rel je instancí třídy relace se čtyřmi argumenty, potom neexistují item1,item2,item3,item4,item5, tak, že rel(item1,item2,item3,item4,item5,) holds.

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

Jestliže rel je instancí třídy relace s pěti argumenty, potom neexistují item1,item2,item3,item4,item5,item6, tak, že rel(item1,item2,item3,item4,item5,item6,) holds.

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

jestliže list je instancí třídy seznam,
potom existuje number1 tak, že existuje item1 tak, že "number1th element of list" se nerovná item1 a pro všechny number2 platí: jestliže number2 je instancí třídy kladné celé číslo a number2 je menší než number1, potom existuje item2 tak, že "number2th element of list" se rovná item2

(=>
      (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))))))))

list je instancí třídy seznam bez duplicit tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže "number1th element of list" se rovná "number2th element of list", potom number1 se rovná number2.

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

jestliže class je covered by ,
potom pro všechny obj platí: jestliže obj je instancí třídy class, potom existuje item tak, že item je a member of "()" a obj je instancí třídy item

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

Jestliže list1 je instancí třídy seznam a list2 je instancí třídy seznam a pro všechny number platí: "numberth element of list1" se rovná "numberth element of list2", potom list1 se rovná list2.

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

Jestliže numberth argument of rel je an instance of class a rel() holds, potom "numberth element of "()"" je instancí třídy class.

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

list3 se rovná "list concatenate fn(list1,list2)" tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže number1 je menší než nebo roven "length of list1" a number2 je menší než nebo roven "length of list2" a number1 je instancí třídy kladné celé číslo a number2 je instancí třídy kladné celé číslo, potom "number1th element of list3" se rovná "number1th element of list1" a ""("length of list1"+number2)"th element of list3" se rovná "number2th element of list2".

(<=>
      (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))))))

Jestliže function je instancí třídy unární funkce, potom function has argument(s).

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

jestliže fun je instancí třídy prostá funkce na,
potom pro všechny arg1,arg2 platí: jestliže th argument of fun je an instance of class a arg1 je instancí třídy class a arg2 je instancí třídy class a arg1 se nerovná arg2, potom "fun(arg1)" se nerovná "fun(arg2)"

(=>
      (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))))))

Jestliže seq je instancí třídy sekvenční funkce a range of seq je an instance of class, potom class je podtřídou celé číslo.

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

Jestliže function je instancí třídy binární funkce, potom function has argument(s).

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

jestliže function je instancí třídy asociativní funkce,
potom pro všechny inst1,inst2,inst3 platí: jestliže th argument of function je an instance of class a inst1 je instancí třídy class a inst2 je instancí třídy class a inst3 je instancí třídy class, potom "function(inst1,"function(inst2,inst3)")" se rovná "function("function(inst1,inst2)",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)))))

jestliže function je instancí třídy komutativní funkce,
potom pro všechny inst1,inst2 platí: jestliže th argument of function je an instance of class a inst1 je instancí třídy class a inst2 je instancí třídy class, potom "function(inst1,inst2)" se rovná "function(inst2,inst1)"

(=>
      (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)))))

Jestliže function je instancí třídy funkce se třemi argumenty, potom function has argument(s).

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

Jestliže function je instancí třídy funkce se čtyřmi argumenty, potom function has argument(s).

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

Jestliže rel je instancí třídy binární predikát, potom rel has argument(s).

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

Jestliže rel je instancí třídy predikát se třemi argumenty, potom rel has argument(s).

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

Jestliže rel je instancí třídy predikát se čtyřmi argumenty, potom rel has argument(s).

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

Jestliže rel je instancí třídy predikát s pěti argumenty, potom rel has argument(s).

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

Jestliže rel je instancí třídy relace s proměnným počtem argumentů, potom neexistuje int tak, že rel has int argument(s).

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

jestliže function je closed on class a function je instancí třídy unární funkce,
potom pro všechny inst platí: jestliže inst je instancí třídy class, potom "function(inst)" je instancí třídy class

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

jestliže function je closed on class a function je instancí třídy binární funkce,
potom pro všechny inst1,inst2 platí: jestliže inst1 je instancí třídy class a inst2 je instancí třídy class, potom "function(inst1,inst2)" je instancí třídy class

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

jestliže relation je reflexive on class,
potom pro všechny inst platí: jestliže inst je instancí třídy class, potom relation(inst,inst) holds

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

jestliže relation je irreflexive on class,
potom pro všechny inst platí: jestliže inst je instancí třídy class, potom relation(inst,inst) doesn't hold

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

Jestliže relation je partial ordering on class, potom relation je reflexive on class a relation je instancí třídy tranzitivní relace a relation je instancí třídy antisymetrická relace.

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

jestliže relation je trichotomizing on class,
potom pro všechny inst1,inst2 platí: jestliže inst1 je instancí třídy class a inst2 je instancí třídy class, potom relation(inst1,inst2) holds nebo relation(inst2,inst1) holds nebo inst1 se rovná 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)))))

Jestliže relation je equivalence relation on class, potom relation je instancí třídy tranzitivní relace a relation je instancí třídy symetrická relace a relation je reflexive on class.

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

jestliže function1 je distributive over function2,
potom pro všechny inst1,inst2,inst3 platí: jestliže th argument of function1 je an instance of class1 a inst1 je instancí třídy class1 a inst2 je instancí třídy class1 a inst3 je instancí třídy class1 a th argument of function2 je an instance of class2 a inst1 je instancí třídy class2 a inst2 je instancí třídy class2 a inst3 je instancí třídy class2, potom "function1(inst1,"function2(inst2,inst3)")" se rovná "function2("function1(inst1,inst2)","function1(inst1,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))))))

Jestliže proc1 je instancí třídy proces, potom existuje proc2 tak, že proc2 causes proc1.

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

jestliže causes subclass(proc1,proc2) platí,
potom pro všechny inst2 platí: jestliže inst2 je instancí třídy proc2, potom existuje proc1 inst1 tak, že inst1 causes inst2

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

Jestliže role je instancí třídy case role a role(arg1,arg2) holds a arg1 je instancí třídy proc, potom arg2 je capable to do proc in role role.

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

jestliže person posesses obj,
potom existuje type tak, že type has the right to perform person a pro všechny process platí: jestliže process je instancí třídy type, potom obj je účastníkem process

(=>
      (possesses ?PERSON ?OBJ)
      (exists
            (?TYPE)
            (and
                  (holdsRight ?PERSON ?TYPE)
                  (forall
                        (?PROCESS)
                        (=>
                              (instance ?PROCESS ?TYPE)
                              (patient ?PROCESS ?OBJ))))))

Jestliže time je instancí třídy časová pozice a agent1 posesses obj během time a agent2 posesses obj během time, potom agent1 se rovná agent2.

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

obj je instancí třídy "belongings of person" tehdy a jen tehdy pokud person posesses obj.

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

jestliže precondition(proc1,proc2) platí,
potom jestliže existuje inst2 tak, že inst2 je instancí třídy proc2, potom existuje inst1 tak, že inst1 je instancí třídy proc1

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

Jestliže inhibits(proc1,proc2) platí, potom pro všechny time,place platí: "existuje proc1 inst1 tak, že inst1 je located at place během time" decreases likelihood of "existuje proc2 inst2 tak, že inst2 je located at place během time".

(=>
      (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)))))))

jestliže prevents(proc1,proc2) platí,
potom pro všechny time,place platí: jestliže existuje proc1 inst1 tak, že inst1 je located at place během time, potom existuje proc2 inst2 tak, že inst2 je located at place během time

(=>
      (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))))))))

subsumes content class(class1,class2) platí tehdy a jen tehdy pokud pro všechny obj2,info platí: jestliže obj2 je instancí třídy class2 a obj2 contains information info, potom existuje class1 obj1 tak, že obj1 contains information info.

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

Jestliže realization(process,prop) platí, potom existuje objekt nesoucí informaci obj tak, že obj contains information prop.

(=>
      (realization ?PROCESS ?PROP)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (containsInformation ?OBJ ?PROP))))

Jestliže number je instancí třídy racionální číslo, potom existují celé číslo int1,celé číslo int2 tak, že number se rovná "int1/int2".

(=>
      (instance ?NUMBER RationalNumber)
      (exists
            (?INT1 ?INT2)
            (and
                  (instance ?INT1 Integer)
                  (instance ?INT2 Integer)
                  (equal
                        ?NUMBER
                        (DivisionFn ?INT1 ?INT2)))))

"absolute value fn(number1)" se rovná number2 a number1 je instancí třídy reálné číslo a number2 je instancí třídy reálné číslo tehdy a jen tehdy pokud

number1 je instancí třídy nezáporné reálné číslo a number1 se rovná number2
number1 je instancí třídy záporné reálné číslo a number2 se rovná "(-number1)"

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

Jestliže "ceiling fn(number)" se rovná int, potom neexistuje celé číslo otherint tak, že otherint je větší než nebo roven number a otherint je menší než int.

(=>
      (equal
            (CeilingFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (greaterThanOrEqualTo ?OTHERINT ?NUMBER)
                        (lessThan ?OTHERINT ?INT)))))

Jestliže "floor fn(number)" se rovná int, potom neexistuje celé číslo otherint tak, že otherint je menší než nebo roven number a otherint je větší než int.

(=>
      (equal
            (FloorFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (lessThanOrEqualTo ?OTHERINT ?NUMBER)
                        (greaterThan ?OTHERINT ?INT)))))

Jestliže number je instancí třídy komplexní číslo, potom existují part1,part2 tak, že part1 se rovná "real number fn(number)" a part2 se rovná "imaginary part fn(number)".

(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?PART1 ?PART2)
            (and
                  (equal
                        ?PART1
                        (RealNumberFn ?NUMBER))
                  (equal
                        ?PART2
                        (ImaginaryPartFn ?NUMBER)))))

Jestliže number je instancí třídy veličina, potom "reciprocal fn(number)" se rovná "exponentiation fn(number,)".

(=>
      (instance ?NUMBER Quantity)
      (equal
            (ReciprocalFn ?NUMBER)
            (ExponentiationFn ?NUMBER -1)))

Jestliže number je instancí třídy veličina, potom se rovná "number*"reciprocal fn(number)"".

(=>
      (instance ?NUMBER Quantity)
      (equal
            1
            (MultiplicationFn
                  ?NUMBER
                  (ReciprocalFn ?NUMBER))))

Jestliže number je instancí třídy sudé celé číslo, potom "number mod " se rovná .

(=>
      (instance ?NUMBER EvenInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            0))

Jestliže number je instancí třídy liché celé číslo, potom "number mod " se rovná .

(=>
      (instance ?NUMBER OddInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            1))

jestliže prime je instancí třídy prvočíslo,
potom pro všechny number platí: jestliže "prime mod number" se rovná , potom number se rovná nebo number se rovná prime

(=>
      (instance ?PRIME PrimeNumber)
      (forall
            (?NUMBER)
            (=>
                  (equal
                        (RemainderFn ?PRIME ?NUMBER)
                        0)
                  (or
                        (equal ?NUMBER 1)
                        (equal ?NUMBER ?PRIME)))))

Jestliže number je instancí třídy nezáporné reálné číslo, potom "signum fn(number)" se rovná nebo "signum fn(number)" se rovná .

(=>
      (instance ?NUMBER NonnegativeRealNumber)
      (or
            (equal
                  (SignumFn ?NUMBER)
                  1)
            (equal
                  (SignumFn ?NUMBER)
                  0)))

Jestliže number je instancí třídy kladné reálné číslo, potom "signum fn(number)" se rovná .

(=>
      (instance ?NUMBER PositiveRealNumber)
      (equal
            (SignumFn ?NUMBER)
            1))

Jestliže number je instancí třídy záporné reálné číslo, potom "signum fn(number)" se rovná .

(=>
      (instance ?NUMBER NegativeRealNumber)
      (equal
            (SignumFn ?NUMBER)
            -1))

Jestliže degree je instancí třídy jednotka plošného úhlu, potom "tangent fn(degree)" se rovná ""sine fn(degree)"/"cosine fn(degree)"".

(=>
      (instance ?DEGREE PlaneAngleMeasure)
      (equal
            (TangentFn ?DEGREE)
            (DivisionFn
                  (SineFn ?DEGREE)
                  (CosineFn ?DEGREE))))

jestliže id je an identity element of function,
potom pro všechny inst platí: jestliže th argument of function je an instance of class a inst je instancí třídy class, potom "function(id,inst)" se rovná inst

(=>
      (identityElement ?FUNCTION ?ID)
      (forall
            (?INST)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?ID ?INST)
                        ?INST))))

Jestliže int je instancí třídy celé číslo, potom int je menší než "(int+1)".

(=>
      (instance ?INT Integer)
      (lessThan
            ?INT
            (SuccessorFn ?INT)))

Jestliže int1 je instancí třídy celé číslo a int2 je instancí třídy celé číslo, potom int1 není menší než int2 nebo int2 není menší než "(int1+1)".

(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT1 ?INT2)
                  (lessThan
                        ?INT2
                        (SuccessorFn ?INT1)))))

Jestliže int je instancí třídy celé číslo, potom int se rovná "("(int+2)"+1)".

(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (SuccessorFn
                  (PredecessorFn ?INT))))

Jestliže int je instancí třídy celé číslo, potom int se rovná "("(int+1)"+2)".

(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (PredecessorFn
                  (SuccessorFn ?INT))))

Jestliže int je instancí třídy celé číslo, potom int je větší než "(int+2)".

(=>
      (instance ?INT Integer)
      (greaterThan
            ?INT
            (PredecessorFn ?INT)))

Jestliže int1 je instancí třídy celé číslo a int2 je instancí třídy celé číslo, potom int2 není menší než int1 nebo "(int1+2)" není menší než int2.

(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT2 ?INT1)
                  (lessThan
                        (PredecessorFn ?INT1)
                        ?INT2))))

Jestliže set je instancí třídy konečná množina, potom existuje nezáporné celé číslo number tak, že number se rovná "cardinality fn(set)".

(=>
      (instance ?SET FiniteSet)
      (exists
            (?NUMBER)
            (and
                  (instance ?NUMBER NonnegativeInteger)
                  (equal
                        ?NUMBER
                        (CardinalityFn ?SET)))))

jestliže superclass je instancí třídy po dvou disjunktní třídy,
potom pro všechny class1,class2 platí: jestliže class1 je instancí třídy superclass a class2 je instancí třídy superclass, potom class1 se rovná class2 nebo class1 je disjoint from class2

(=>
      (instance ?SUPERCLASS PairwiseDisjointClass)
      (forall
            (?CLASS1 ?CLASS2)
            (=>
                  (and
                        (instance ?CLASS1 ?SUPERCLASS)
                        (instance ?CLASS2 ?SUPERCLASS))
                  (or
                        (equal ?CLASS1 ?CLASS2)
                        (disjoint ?CLASS1 ?CLASS2)))))

jestliže class je instancí třídy vzájemně disjunktní třídy,
potom pro všechny inst1,inst2 platí: jestliže inst1 je instancí třídy class a inst2 je instancí třídy inst1, potom existuje class inst3 tak, že inst2 není instancí třídy inst3

(=>
      (instance ?CLASS MutuallyDisjointClass)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?INST1))
                  (exists
                        (?INST3)
                        (and
                              (instance ?INST3 ?CLASS)
                              (not
                                    (instance ?INST2 ?INST3)))))))

Jestliže graph je instancí třídy graf a node1 je instancí třídy uzel grafu a node2 je instancí třídy uzel grafu a node1 je částí graph a node2 je částí graph a node1 se nerovná node2, potom existují arc,path tak, že

arc spojuje node1 a node2
- path je podgrafem graph
- path je instancí třídy cesta v grafu
- - "the beginning of path" se rovná node1 a "the end of path" se rovná node2
  - "the beginning of path" se rovná node2 a "the end of path" se rovná node1

(=>
      (and
            (instance ?GRAPH Graph)
            (instance ?NODE1 GraphNode)
            (instance ?NODE2 GraphNode)
            (graphPart ?NODE1 ?GRAPH)
            (graphPart ?NODE2 ?GRAPH)
            (not
                  (equal ?NODE1 ?NODE2)))
      (exists
            (?ARC ?PATH)
            (or
                  (links ?NODE1 ?NODE2 ?ARC)
                  (and
                        (subGraph ?PATH ?GRAPH)
                        (instance ?PATH GraphPath)
                        (or
                              (and
                                    (equal
                                          (BeginNodeFn ?PATH)
                                          ?NODE1)
                                    (equal
                                          (EndNodeFn ?PATH)
                                          ?NODE2))
                              (and
                                    (equal
                                          (BeginNodeFn ?PATH)
                                          ?NODE2)
                                    (equal
                                          (EndNodeFn ?PATH)
                                          ?NODE1)))))))

Jestliže graph je instancí třídy graf, potom existují node1,node2,node3,arc1,arc2 tak, že node1 je částí graph a node2 je částí graph a node3 je částí graph a arc1 je částí graph a arc2 je částí graph a node2 spojuje arc1 a node1 a node3 spojuje arc2 a node2 a node1 se nerovná node2 a node2 se nerovná node3 a node1 se nerovná node3 a arc1 se nerovná arc2.

(=>
      (instance ?GRAPH Graph)
      (exists
            (?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
            (and
                  (graphPart ?NODE1 ?GRAPH)
                  (graphPart ?NODE2 ?GRAPH)
                  (graphPart ?NODE3 ?GRAPH)
                  (graphPart ?ARC1 ?GRAPH)
                  (graphPart ?ARC2 ?GRAPH)
                  (links ?ARC1 ?NODE1 ?NODE2)
                  (links ?ARC2 ?NODE2 ?NODE3)
                  (not
                        (equal ?NODE1 ?NODE2))
                  (not
                        (equal ?NODE2 ?NODE3))
                  (not
                        (equal ?NODE1 ?NODE3))
                  (not
                        (equal ?ARC1 ?ARC2)))))

Jestliže graph je instancí třídy orientovaný graf a arc je instancí třídy hrana grafu a arc je částí graph, potom existují node1,node2 tak, že "initial node fn(arc)" se rovná node1 a "terminal node fn(arc)" se rovná node2.

(=>
      (and
            (instance ?GRAPH DirectedGraph)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (exists
            (?NODE1 ?NODE2)
            (and
                  (equal
                        (InitialNodeFn ?ARC)
                        ?NODE1)
                  (equal
                        (TerminalNodeFn ?ARC)
                        ?NODE2))))

Jestliže graph je instancí třídy strom, potom neexistuje smyčka grafu loop tak, že loop je částí graph.

(=>
      (instance ?GRAPH Tree)
      (not
            (exists
                  (?LOOP)
                  (and
                        (instance ?LOOP GraphLoop)
                        (graphPart ?LOOP ?GRAPH)))))

jestliže graph je instancí třídy cesta v grafu a arc je instancí třídy hrana grafu a arc je částí graph,
potom jestliže "initial node fn(arc)" se rovná node, potom neexistuje other tak, že "initial node fn(other)" se rovná node a other se nerovná arc

(=>
      (and
            (instance ?GRAPH GraphPath)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (=>
            (equal
                  (InitialNodeFn ?ARC)
                  ?NODE)
            (not
                  (exists
                        (?OTHER)
                        (and
                              (equal
                                    (InitialNodeFn ?OTHER)
                                    ?NODE)
                              (not
                                    (equal ?OTHER ?ARC)))))))

jestliže graph je instancí třídy cesta v grafu a arc je instancí třídy hrana grafu a arc je částí graph,
potom jestliže "terminal node fn(arc)" se rovná node, potom neexistuje other tak, že "terminal node fn(other)" se rovná node a other se nerovná arc

(=>
      (and
            (instance ?GRAPH GraphPath)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (=>
            (equal
                  (TerminalNodeFn ?ARC)
                  ?NODE)
            (not
                  (exists
                        (?OTHER)
                        (and
                              (equal
                                    (TerminalNodeFn ?OTHER)
                                    ?NODE)
                              (not
                                    (equal ?OTHER ?ARC)))))))

graph je instancí třídy cyklus tehdy a jen tehdy pokud existuje node tak, že "the beginning of graph" se rovná node a "the end of graph" se rovná node.

(<=>
      (instance ?GRAPH GraphCircuit)
      (exists
            (?NODE)
            (and
                  (equal
                        (BeginNodeFn ?GRAPH)
                        ?NODE)
                  (equal
                        (EndNodeFn ?GRAPH)
                        ?NODE))))

graph je instancí třídy multigraf tehdy a jen tehdy pokud existují arc1,arc2,node1,node2 tak, že arc1 je částí graph a arc2 je částí graph a node1 je částí graph a node2 je částí graph a arc1 spojuje node1 a node2 a arc2 spojuje node1 a node2 a arc1 se nerovná arc2.

(<=>
      (instance ?GRAPH MultiGraph)
      (exists
            (?ARC1 ?ARC2 ?NODE1 ?NODE2)
            (and
                  (graphPart ?ARC1 ?GRAPH)
                  (graphPart ?ARC2 ?GRAPH)
                  (graphPart ?NODE1 ?GRAPH)
                  (graphPart ?NODE2 ?GRAPH)
                  (links ?NODE1 ?NODE2 ?ARC1)
                  (links ?NODE1 ?NODE2 ?ARC2)
                  (not
                        (equal ?ARC1 ?ARC2)))))

graph je instancí třídy pseudograf tehdy a jen tehdy pokud existuje smyčka grafu loop tak, že loop je částí graph.

(<=>
      (instance ?GRAPH PseudoGraph)
      (exists
            (?LOOP)
            (and
                  (instance ?LOOP GraphLoop)
                  (graphPart ?LOOP ?GRAPH))))

Jestliže part je instancí třídy prvek grafu, potom existuje graf graph tak, že part je částí graph.

(=>
      (instance ?PART GraphElement)
      (exists
            (?GRAPH)
            (and
                  (instance ?GRAPH Graph)
                  (graphPart ?PART ?GRAPH))))

Jestliže node je instancí třídy uzel grafu, potom existují other,arc tak, že arc spojuje node a other.

(=>
      (instance ?NODE GraphNode)
      (exists
            (?OTHER ?ARC)
            (links ?NODE ?OTHER ?ARC)))

Jestliže arc je instancí třídy hrana grafu, potom existují node1,node2 tak, že arc spojuje node1 a node2.

(=>
      (instance ?ARC GraphArc)
      (exists
            (?NODE1 ?NODE2)
            (links ?NODE1 ?NODE2 ?ARC)))

loop je instancí třídy smyčka grafu tehdy a jen tehdy pokud existuje node tak, že loop spojuje node a node.

(<=>
      (instance ?LOOP GraphLoop)
      (exists
            (?NODE)
            (links ?NODE ?NODE ?LOOP)))

Jestliže "initial node fn(arc)" se rovná node a "terminal node fn(arc)" se rovná node, potom arc je instancí třídy smyčka grafu.

(=>
      (and
            (equal
                  (InitialNodeFn ?ARC)
                  ?NODE)
            (equal
                  (TerminalNodeFn ?ARC)
                  ?NODE))
      (instance ?ARC GraphLoop))

Jestliže "minimal weighted path fn(node1,node2)" se rovná path, potom path je instancí třídy "graph path fn(node1,node2)".

(=>
      (equal
            (MinimalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

jestliže "minimal weighted path fn(node1,node2)" se rovná path a "path weight fn(path)" se rovná number,
potom pro všechny path2 platí: jestliže path2 je instancí třídy "graph path fn(node1,node2)" a "path weight fn(path2)" se rovná number2, potom number2 je větší než nebo roven number1

(=>
      (and
            (equal
                  (MinimalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (greaterThanOrEqualTo ?NUMBER2 ?NUMBER1))))

Jestliže "maximal weighted path fn(node1,node2)" se rovná path, potom path je instancí třídy "graph path fn(node1,node2)".

(=>
      (equal
            (MaximalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

jestliže "maximal weighted path fn(node1,node2)" se rovná path a "path weight fn(path)" se rovná number,
potom pro všechny path2 platí: jestliže path2 je instancí třídy "graph path fn(node1,node2)" a "path weight fn(path2)" se rovná number2, potom number2 je menší než nebo roven number1

(=>
      (and
            (equal
                  (MaximalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

Jestliže path je částí graph a graph není instancí třídy orientovaný graf, potom "graph path fn(node1,node2)" se rovná path tehdy a jen tehdy pokud "graph path fn(node2,node1)" se rovná path.

(=>
      (and
            (graphPart ?PATH ?GRAPH)
            (not
                  (instance ?GRAPH DirectedGraph)))
      (<=>
            (equal
                  (GraphPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (GraphPathFn ?NODE2 ?NODE1)
                  ?PATH)))

Jestliže graph je instancí třídy graf, potom "minimal cut set fn(graph)" je podtřídou "cut set fn(graph)".

(=>
      (instance ?GRAPH Graph)
      (subclass
            (MinimalCutSetFn ?GRAPH)
            (CutSetFn ?GRAPH)))

jestliže "minimal cut set fn(graph)" se rovná pathclass,
potom existuje number tak, že pro všechny path platí: jestliže path je instancí třídy pathclass, potom délka path je number

(=>
      (equal
            (MinimalCutSetFn ?GRAPH)
            ?PATHCLASS)
      (exists
            (?NUMBER)
            (forall
                  (?PATH)
                  (=>
                        (instance ?PATH ?PATHCLASS)
                        (pathLength ?PATH ?NUMBER)))))

Neexistují cut set fn(graph) path1,minimal cut set fn(graph) path2 tak, že délka path1 je number1 a délka path2 je number2 a number1 je menší než number2.

(not
      (exists
            (?PATH1 ?PATH2)
            (and
                  (instance
                        ?PATH1
                        (CutSetFn ?GRAPH))
                  (instance
                        ?PATH2
                        (MinimalCutSetFn ?GRAPH))
                  (pathLength ?PATH1 ?NUMBER1)
                  (pathLength ?PATH2 ?NUMBER2)
                  (lessThan ?NUMBER1 ?NUMBER2))))

Jestliže "number unit(s)" se rovná quant a unit je podtřídou quanttype, potom quant je instancí třídy quanttype.

(=>
      (and
            (equal
                  (MeasureFn ?NUMBER ?UNIT)
                  ?QUANT)
            (subclass ?UNIT ?QUANTTYPE))
      (instance ?QUANT ?QUANTTYPE))

jestliže rel je instancí třídy relace rozšířená na veličiny a rel je instancí třídy terciální relace a number1 je instancí třídy reálné číslo a number2 je instancí třídy reálné číslo a rel(number1,number2,value) holds,
potom pro všechny unit platí: jestliže unit je instancí třídy měrná jednotka, potom rel("number1 unit(s)","number2 unit(s)","value unit(s)") holds

(=>
      (and
            (instance ?REL RelationExtendedToQuantities)
            (instance ?REL TernaryRelation)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber)
            (holds ?REL ?NUMBER1 ?NUMBER2 ?VALUE))
      (forall
            (?UNIT)
            (=>
                  (instance ?UNIT UnitOfMeasure)
                  (holds
                        ?REL
                        (MeasureFn ?NUMBER1 ?UNIT)
                        (MeasureFn ?NUMBER2 ?UNIT)
                        (MeasureFn ?VALUE ?UNIT)))))

jestliže rel je instancí třídy relace rozšířená na veličiny a rel je instancí třídy binární relace a number1 je instancí třídy reálné číslo a number2 je instancí třídy reálné číslo a rel(number1,number2) holds,
potom pro všechny unit platí: jestliže unit je instancí třídy měrná jednotka, potom rel("number1 unit(s)","number2 unit(s)") holds

(=>
      (and
            (instance ?REL RelationExtendedToQuantities)
            (instance ?REL BinaryRelation)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber)
            (holds ?REL ?NUMBER1 ?NUMBER2))
      (forall
            (?UNIT)
            (=>
                  (instance ?UNIT UnitOfMeasure)
                  (holds
                        ?REL
                        (MeasureFn ?NUMBER1 ?UNIT)
                        (MeasureFn ?NUMBER2 ?UNIT)))))

Jestliže unit je instancí třídy měrná jednotka, potom "kilo fn(unit)" se rovná " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (KiloFn ?UNIT)
            (MeasureFn 1000 ?UNIT)))

Jestliže unit je instancí třídy měrná jednotka, potom "mega fn(unit)" se rovná " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MegaFn ?UNIT)
            (MeasureFn 1000000 ?UNIT)))

Jestliže unit je instancí třídy měrná jednotka, potom "giga fn(unit)" se rovná " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (GigaFn ?UNIT)
            (MeasureFn 1000000000 ?UNIT)))

Jestliže unit je instancí třídy měrná jednotka, potom "tera fn(unit)" se rovná " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (TeraFn ?UNIT)
            (MeasureFn 1000000000000 ?UNIT)))

Jestliže unit je instancí třídy měrná jednotka, potom "milli fn(unit)" se rovná " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MilliFn ?UNIT)
            (MeasureFn 0.001 ?UNIT)))

Jestliže unit je instancí třídy měrná jednotka, potom "micro fn(unit)" se rovná " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MicroFn ?UNIT)
            (MeasureFn 0.000001 ?UNIT)))

Jestliže unit je instancí třídy měrná jednotka, potom "nano fn(unit)" se rovná " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (NanoFn ?UNIT)
            (MeasureFn 0.000000001 ?UNIT)))

Jestliže unit je instancí třídy měrná jednotka, potom "pico fn(unit)" se rovná " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (PicoFn ?UNIT)
            (MeasureFn 0.000000000001 ?UNIT)))

quantity je instancí třídy "interval fn(from,to)" tehdy a jen tehdy pokud quantity je větší než nebo roven from a quantity je menší než nebo roven to.

(<=>
      (instance
            ?QUANTITY
            (IntervalFn ?FROM ?TO))
      (and
            (greaterThanOrEqualTo ?QUANTITY ?FROM)
            (lessThanOrEqualTo ?QUANTITY ?TO)))

Jestliže number je instancí třídy reálné číslo a unit je instancí třídy měrná jednotka, potom "magnitude fn(number unit(s))" se rovná number.

(=>
      (and
            (instance ?NUMBER RealNumber)
            (instance ?UNIT UnitOfMeasure))
      (equal
            (MagnitudeFn
                  (MeasureFn ?NUMBER ?UNIT))
            ?NUMBER))

Jestliže number je instancí třídy reálné číslo, potom "number centimeter(s)" se rovná ""number*" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Centimeter)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  Meter)))

Jestliže number je instancí třídy reálné číslo, potom "number celsius degree(s)" se rovná ""(number-)" kelvin degree(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (SubtractionFn ?NUMBER 273.15)
                  KelvinDegree)))

Jestliže number je instancí třídy reálné číslo, potom "number celsius degree(s)" se rovná """(number-)"/" fahrenheit degree(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (DivisionFn
                        (SubtractionFn ?NUMBER 32)
                        1.8)
                  FahrenheitDegree)))

Jestliže number je instancí třídy reálné číslo, potom "number day duration(s)" se rovná ""number*" hour duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER DayDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 24)
                  HourDuration)))

Jestliže number je instancí třídy reálné číslo, potom "number hour duration(s)" se rovná ""number*" minute duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER HourDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  MinuteDuration)))

Jestliže number je instancí třídy reálné číslo, potom "number minute duration(s)" se rovná ""number*" second duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MinuteDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  SecondDuration)))

Jestliže number je instancí třídy reálné číslo, potom "number week duration(s)" se rovná ""number*" day duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER WeekDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 7)
                  DayDuration)))

Jestliže number je instancí třídy reálné číslo, potom "number year duration(s)" se rovná ""number*" day duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER YearDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 365)
                  DayDuration)))

Jestliže number je instancí třídy reálné číslo, potom "number amu(s)" se rovná ""number**" gram(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Amu)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.6605402 E-24)
                  Gram)))

Jestliže number je instancí třídy reálné číslo, potom "number electron volt(s)" se rovná ""number**" joule(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER ElectronVolt)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.60217733 E-19)
                  Joule)))

Jestliže number je instancí třídy reálné číslo, potom "number angstrom(s)" se rovná ""number**" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Angstrom)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.0 E-10)
                  Meter)))

Jestliže number je instancí třídy reálné číslo, potom "number foot(s)" se rovná ""number*" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Foot)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.3048)
                  Meter)))

Jestliže number je instancí třídy reálné číslo, potom "number inch(s)" se rovná ""number*" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Inch)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.0254)
                  Meter)))

Jestliže number je instancí třídy reálné číslo, potom "number mile(s)" se rovná ""number*" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Mile)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1609.344)
                  Meter)))

Jestliže number je instancí třídy reálné číslo, potom "number united states gallon(s)" se rovná ""number*" liter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 3.785411784)
                  Liter)))

Jestliže number je instancí třídy reálné číslo, potom "number quart(s)" se rovná ""number/" united states gallon(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Quart)
            (MeasureFn
                  (DivisionFn ?NUMBER 4)
                  UnitedStatesGallon)))

Jestliže number je instancí třídy reálné číslo, potom "number pint(s)" se rovná ""number/" quart(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Pint)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Quart)))

Jestliže number je instancí třídy reálné číslo, potom "number cup(s)" se rovná ""number/" pint(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Cup)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Pint)))

Jestliže number je instancí třídy reálné číslo, potom "number ounce(s)" se rovná ""number/" cup(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Ounce)
            (MeasureFn
                  (DivisionFn ?NUMBER 8)
                  Cup)))

Jestliže number je instancí třídy reálné číslo, potom "number united kingdom gallon(s)" se rovná ""number*" liter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedKingdomGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.54609)
                  Liter)))

Jestliže number je instancí třídy reálné číslo, potom "number pound mass(s)" se rovná ""number*" gram(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundMass)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 453.59237)
                  Gram)))

Jestliže number je instancí třídy reálné číslo, potom "number slug(s)" se rovná ""number*" gram(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Slug)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 14593.90)
                  Gram)))

Jestliže number je instancí třídy reálné číslo, potom "number rankine degree(s)" se rovná ""number*" kelvin degree(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER RankineDegree)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.8)
                  KelvinDegree)))

Jestliže number je instancí třídy reálné číslo, potom "number pound force(s)" se rovná ""number*" newton(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundForce)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.448222)
                  Newton)))

Jestliže number je instancí třídy reálné číslo, potom "number calorie(s)" se rovná ""number*" joule(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Calorie)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.1868)
                  Joule)))

Jestliže number je instancí třídy reálné číslo, potom "number british thermal unit(s)" se rovná ""number*" joule(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER BritishThermalUnit)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1055.05585262)
                  Joule)))

Jestliže number je instancí třídy reálné číslo, potom "number angular degree(s)" se rovná ""number*"pi/"" radian(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER AngularDegree)
            (MeasureFn
                  (MultiplicationFn
                        ?NUMBER
                        (DivisionFn Pi 180))
                  Radian)))

Jestliže number je instancí třídy reálné číslo, potom "number united states cent(s)" se rovná ""number*" united states dollar(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  UnitedStatesDollar)))

Jestliže number je instancí třídy reálné číslo, potom "number euro cent(s)" se rovná ""number*" euro dollar(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER EuroCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  EuroDollar)))

Jestliže number je instancí třídy reálné číslo, potom "number byte(s)" se rovná ""number*" bit(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Byte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 8)
                  Bit)))

Jestliže number je instancí třídy reálné číslo, potom "number kilo byte(s)" se rovná ""number*" byte(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER KiloByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  Byte)))

Jestliže number je instancí třídy reálné číslo, potom "number mega byte(s)" se rovná ""number*" kilo byte(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MegaByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  KiloByte)))

Jestliže point je instancí třídy okamžik a point se nerovná positive infinity, potom point happens before positive infinity.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (before ?POINT PositiveInfinity))

Jestliže point je instancí třídy okamžik a point se nerovná positive infinity, potom existuje otherpoint tak, že otherpoint je between point and positive infinity.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))

Jestliže point je instancí třídy okamžik a point se nerovná negative infinity, potom negative infinity happens before point.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (before NegativeInfinity ?POINT))

Jestliže point je instancí třídy okamžik a point se nerovná negative infinity, potom existuje otherpoint tak, že otherpoint je between negative infinity and point.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))

jestliže frequency(proc,time1) platí,
potom pro všechny time2 platí: jestliže duration of time2 je time1, potom existuje position tak, že position je a part of time2 a existuje inst tak, že inst je instancí třídy proc během position

(=>
      (frequency ?PROC ?TIME1)
      (forall
            (?TIME2)
            (=>
                  (duration ?TIME2 ?TIME1)
                  (exists
                        (?POSITION)
                        (and
                              (temporalPart ?POSITION ?TIME2)
                              (holdsDuring
                                    ?POSITION
                                    (exists
                                          (?INST)
                                          (instance ?INST ?PROC))))))))

Jestliže point je instancí třídy okamžik, potom existuje časový interval interval tak, že point je a part of interval.

(=>
      (instance ?POINT TimePoint)
      (exists
            (?INTERVAL)
            (and
                  (instance ?INTERVAL TimeInterval)
                  (temporalPart ?POINT ?INTERVAL))))

Jestliže interval je instancí třídy časový interval, potom existuje okamžik point tak, že point je a part of interval.

(=>
      (instance ?INTERVAL TimeInterval)
      (exists
            (?POINT)
            (and
                  (instance ?POINT TimePoint)
                  (temporalPart ?POINT ?INTERVAL))))

Jestliže rel(inst1,inst2) holds během interval a inst1 je instancí třídy fyzický objekt a inst2 je instancí třídy fyzický objekt, potom inst1 exists during interval a inst2 exists during interval.

(=>
      (and
            (holdsDuring
                  ?INTERVAL
                  (holds ?REL ?INST1 ?INST2))
            (instance ?INST1 Physical)
            (instance ?INST2 Physical))
      (and
            (time ?INST1 ?INTERVAL)
            (time ?INST2 ?INTERVAL)))

jestliže obj je instancí třídy objekt,
potom existují okamžik time1,okamžik time2 tak, že time1 happens before time2 a pro všechny time platí: jestliže time1 happen?{s} before or at time a time happen?{s} before or at time2, potom obj exists during time

(=>
      (instance ?OBJ Object)
      (exists
            (?TIME1 ?TIME2)
            (and
                  (instance ?TIME1 TimePoint)
                  (instance ?TIME2 TimePoint)
                  (before ?TIME1 ?TIME2)
                  (forall
                        (?TIME)
                        (=>
                              (and
                                    (beforeOrEqual ?TIME1 ?TIME)
                                    (beforeOrEqual ?TIME ?TIME2))
                              (time ?OBJ ?TIME))))))

phys exists during time a time je instancí třídy okamžik tehdy a jen tehdy pokud time je between or at "the beginning of doba existence phys" and "the end of doba existence phys".

(<=>
      (and
            (time ?PHYS ?TIME)
            (instance ?TIME TimePoint))
      (temporallyBetweenOrEqual
            (BeginFn
                  (WhenFn ?PHYS))
            ?TIME
            (EndFn
                  (WhenFn ?PHYS))))

interval2 overlaps interval1 tehdy a jen tehdy pokud existuje časový interval interval3 tak, že interval3 je a part of interval1 a interval3 je a part of interval2.

(<=>
      (overlapsTemporally ?INTERVAL1 ?INTERVAL2)
      (exists
            (?INTERVAL3)
            (and
                  (instance ?INTERVAL3 TimeInterval)
                  (temporalPart ?INTERVAL3 ?INTERVAL1)
                  (temporalPart ?INTERVAL3 ?INTERVAL2))))

Jestliže rel je instancí třídy prostorová relace a rel(obj1,obj2) holds, potom "doba existence obj2" overlaps "doba existence obj1".

(=>
      (and
            (instance ?REL SpatialRelation)
            (holds ?REL ?OBJ1 ?OBJ2))
      (overlapsTemporally
            (WhenFn ?OBJ1)
            (WhenFn ?OBJ2)))

Jestliže interval je instancí třídy "recurrent time interval fn(timeclass1,timeclass2)", potom existují timeclass1 time1,timeclass2 time2 tak, že time1 starts interval a time2 finishes interval.

(=>
      (instance
            ?INTERVAL
            (RecurrentTimeIntervalFn ?TIMECLASS1 ?TIMECLASS2))
      (exists
            (?TIME1 ?TIME2)
            (and
                  (instance ?TIME1 ?TIMECLASS1)
                  (instance ?TIME2 ?TIMECLASS2)
                  (starts ?TIME1 ?INTERVAL)
                  (finishes ?TIME2 ?INTERVAL))))

Jestliže thing je instancí třídy fyzický objekt, potom "the beginning of doba existence thing" happens before the end of doba existence thing.

(=>
      (instance ?THING Physical)
      (before
            (BeginFn
                  (WhenFn ?THING))
            (EndFn
                  (WhenFn ?THING))))

Jestliže thing je instancí třídy fyzický objekt, potom "před doba existence thing" meets "doba existence thing".

(=>
      (instance ?THING Physical)
      (meetsTemporally
            (PastFn
                  (WhenFn ?THING))
            (WhenFn ?THING)))

Jestliže process je instancí třídy fyzický objekt, potom "před doba existence process" se rovná "interval between negative infinity and "the beginning of doba existence process"".

(=>
      (instance ?PROCESS Physical)
      (equal
            (PastFn
                  (WhenFn ?PROCESS))
            (TimeIntervalFn
                  NegativeInfinity
                  (BeginFn
                        (WhenFn ?PROCESS)))))

Jestliže thing je instancí třídy fyzický objekt, potom "právě před doba existence thing" finishes "před doba existence thing".

(=>
      (instance ?THING Physical)
      (finishes
            (ImmediatePastFn
                  (WhenFn ?THING))
            (PastFn
                  (WhenFn ?THING))))

Jestliže thing je instancí třídy fyzický objekt, potom "doba existence thing" meets "po doba existence thing".

(=>
      (instance ?THING Physical)
      (meetsTemporally
            (WhenFn ?THING)
            (FutureFn
                  (WhenFn ?THING))))

Jestliže process je instancí třídy fyzický objekt, potom "po doba existence process" se rovná "interval between "the end of doba existence process" and positive infinity".

(=>
      (instance ?PROCESS Physical)
      (equal
            (FutureFn
                  (WhenFn ?PROCESS))
            (TimeIntervalFn
                  (EndFn
                        (WhenFn ?PROCESS))
                  PositiveInfinity)))

Jestliže thing je instancí třídy fyzický objekt, potom "právě po doba existence thing" starts "po doba existence thing".

(=>
      (instance ?THING Physical)
      (starts
            (ImmediateFutureFn
                  (WhenFn ?THING))
            (FutureFn
                  (WhenFn ?THING))))

Jestliže day je instancí třídy "number of month", potom number je menší než nebo roven .

(=>
      (instance
            ?DAY
            (DayFn ?NUMBER ?MONTH))
      (lessThanOrEqualTo ?NUMBER 31))

Jestliže day1 je instancí třídy "number1 of month" a day2 je instancí třídy "number2 of month" a "(number2-number1)" se rovná , potom day1 meets day2.

(=>
      (and
            (instance
                  ?DAY1
                  (DayFn ?NUMBER1 ?MONTH))
            (instance
                  ?DAY2
                  (DayFn ?NUMBER2 ?MONTH))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?DAY1 ?DAY2))

Jestliže hour je instancí třídy "number of day", potom number je menší než .

(=>
      (instance
            ?HOUR
            (HourFn ?NUMBER ?DAY))
      (lessThan ?NUMBER 24))

Jestliže hour1 je instancí třídy "number1 of day" a hour2 je instancí třídy "number2 of day" a "(number2-number1)" se rovná , potom hour1 meets hour2.

(=>
      (and
            (instance
                  ?HOUR1
                  (HourFn ?NUMBER1 ?DAY))
            (instance
                  ?HOUR2
                  (HourFn ?NUMBER2 ?DAY))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?HOUR1 ?HOUR2))

Jestliže minute je instancí třídy "number of hour", potom number je menší než .

(=>
      (instance
            ?MINUTE
            (MinuteFn ?NUMBER ?HOUR))
      (lessThan ?NUMBER 60))

Jestliže minute1 je instancí třídy "number1 of hour" a minute2 je instancí třídy "number2 of hour" a "(number2-number1)" se rovná , potom minute1 meets minute2.

(=>
      (and
            (instance
                  ?MINUTE1
                  (MinuteFn ?NUMBER1 ?HOUR))
            (instance
                  ?MINUTE2
                  (MinuteFn ?NUMBER2 ?HOUR))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?MINUTE1 ?MINUTE2))

Jestliže second je instancí třídy "number of minute", potom number je menší než .

(=>
      (instance
            ?SECOND
            (SecondFn ?NUMBER ?MINUTE))
      (lessThan ?NUMBER 60))

Jestliže second1 je instancí třídy "number1 of minute" a second2 je instancí třídy "number2 of minute" a "(number2-number1)" se rovná , potom second1 meets second2.

(=>
      (and
            (instance
                  ?SECOND1
                  (SecondFn ?NUMBER1 ?MINUTE))
            (instance
                  ?SECOND2
                  (SecondFn ?NUMBER2 ?MINUTE))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?SECOND1 ?SECOND2))

Jestliže year je instancí třídy rok, potom duration of year je " year duration(s)".

(=>
      (instance ?YEAR Year)
      (duration
            ?YEAR
            (MeasureFn 1 YearDuration)))

Jestliže year1 je instancí třídy rok a year2 je instancí třídy rok a "(year2-year1)" se rovná , potom year1 meets year2.

(=>
      (and
            (instance ?YEAR1 Year)
            (instance ?YEAR2 Year)
            (equal
                  (SubtractionFn ?YEAR2 ?YEAR1)
                  1))
      (meetsTemporally ?YEAR1 ?YEAR2))

Jestliže leap je instancí třídy přestupný rok a leap se rovná "number rok(s)", potom

"number mod " se rovná a "number mod " se nerovná
"number mod " se rovná

(=>
      (and
            (instance ?LEAP LeapYear)
            (equal
                  ?LEAP
                  (MeasureFn ?NUMBER Year)))
      (or
            (and
                  (equal
                        (RemainderFn ?NUMBER 4)
                        0)
                  (not
                        (equal
                              (RemainderFn ?NUMBER 100)
                              0)))
            (equal
                  (RemainderFn ?NUMBER 400)
                  0)))

Jestliže month je instancí třídy leden, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH January)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Jestliže "únor of year" se rovná month a year není instancí třídy přestupný rok, potom duration of month je " day duration(s)".

(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (not
                  (instance ?YEAR LeapYear)))
      (duration
            ?MONTH
            (MeasureFn 28 DayDuration)))

Jestliže "únor of year" se rovná month a year je instancí třídy přestupný rok, potom duration of month je " day duration(s)".

(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (instance ?YEAR LeapYear))
      (duration
            ?MONTH
            (MeasureFn 29 DayDuration)))

Jestliže month je instancí třídy březen, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH March)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Jestliže month je instancí třídy duben, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH April)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

Jestliže month je instancí třídy květen, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH May)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Jestliže month je instancí třídy červen, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH June)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

Jestliže month je instancí třídy červenec, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH July)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Jestliže month je instancí třídy srpen, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH August)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Jestliže month je instancí třídy září, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH September)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

Jestliže month je instancí třídy říjen, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH October)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Jestliže month je instancí třídy listopad, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH November)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

Jestliže month je instancí třídy prosinec, potom duration of month je " day duration(s)".

(=>
      (instance ?MONTH December)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Jestliže day je instancí třídy den, potom duration of day je " day duration(s)".

(=>
      (instance ?DAY Day)
      (duration
            ?DAY
            (MeasureFn 1 DayDuration)))

Jestliže day1 je instancí třídy pondělí a day2 je instancí třídy úterý a week je instancí třídy týren a day1 je a part of week a day2 je a part of week, potom day1 meets day2.

(=>
      (and
            (instance ?DAY1 Monday)
            (instance ?DAY2 Tuesday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Jestliže day1 je instancí třídy úterý a day2 je instancí třídy středa a week je instancí třídy týren a day1 je a part of week a day2 je a part of week, potom day1 meets day2.

(=>
      (and
            (instance ?DAY1 Tuesday)
            (instance ?DAY2 Wednesday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Jestliže day1 je instancí třídy středa a day2 je instancí třídy čtvrtek a week je instancí třídy týren a day1 je a part of week a day2 je a part of week, potom day1 meets day2.

(=>
      (and
            (instance ?DAY1 Wednesday)
            (instance ?DAY2 Thursday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Jestliže day1 je instancí třídy čtvrtek a day2 je instancí třídy pátek a week je instancí třídy týren a day1 je a part of week a day2 je a part of week, potom day1 meets day2.

(=>
      (and
            (instance ?DAY1 Thursday)
            (instance ?DAY2 Friday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Jestliže day1 je instancí třídy pátek a day2 je instancí třídy sobota a week je instancí třídy týren a day1 je a part of week a day2 je a part of week, potom day1 meets day2.

(=>
      (and
            (instance ?DAY1 Friday)
            (instance ?DAY2 Saturday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Jestliže day1 je instancí třídy sobota a day2 je instancí třídy neděle a week je instancí třídy týren a day1 je a part of week a day2 je a part of week, potom day1 meets day2.

(=>
      (and
            (instance ?DAY1 Saturday)
            (instance ?DAY2 Sunday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Jestliže day1 je instancí třídy neděle a day2 je instancí třídy pondělí a week1 je instancí třídy týren a week2 je instancí třídy týren a day1 je a part of week1 a day2 je a part of week2 a week1 meets week2, potom day1 meets day2.

(=>
      (and
            (instance ?DAY1 Sunday)
            (instance ?DAY2 Monday)
            (instance ?WEEK1 Week)
            (instance ?WEEK2 Week)
            (temporalPart ?DAY1 ?WEEK1)
            (temporalPart ?DAY2 ?WEEK2)
            (meetsTemporally ?WEEK1 ?WEEK2))
      (meetsTemporally ?DAY1 ?DAY2))

Jestliže week je instancí třídy týren, potom duration of week je " week duration(s)".

(=>
      (instance ?WEEK Week)
      (duration
            ?WEEK
            (MeasureFn 1 WeekDuration)))

Jestliže hour je instancí třídy hodina, potom duration of hour je " hour duration(s)".

(=>
      (instance ?HOUR Hour)
      (duration
            ?HOUR
            (MeasureFn 1 HourDuration)))

Jestliže minute je instancí třídy minuta, potom duration of minute je " minute duration(s)".

(=>
      (instance ?MINUTE Minute)
      (duration
            ?MINUTE
            (MeasureFn 1 MinuteDuration)))

Jestliže second je instancí třídy vteřina, potom duration of second je " second duration(s)".

(=>
      (instance ?SECOND Second)
      (duration
            ?SECOND
            (MeasureFn 1 SecondDuration)))

jestliže "decomposition of interval into ? interval-types" se rovná class,
potom pro všechny time1,time2 platí: jestliže time1 je instancí třídy interval-type a time2 je instancí třídy class, potom existuje duration tak, že duration of time1 je duration a duration of time2 je duration

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1 ?TIME2)
            (=>
                  (and
                        (instance ?TIME1 ?INTERVAL-TYPE)
                        (instance ?TIME2 ?CLASS))
                  (exists
                        (?DURATION)
                        (and
                              (duration ?TIME1 ?DURATION)
                              (duration ?TIME2 ?DURATION))))))

jestliže "decomposition of interval into ? interval-types" se rovná class,
potom pro všechny time1,time2 platí: jestliže time1 je instancí třídy class a time2 je instancí třídy class a time1 se nerovná time2, potom time1 meets time2 nebo time2 meets time1 nebo time1 happens earlier than time2 nebo time2 happens earlier than time1

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1 ?TIME2)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (instance ?TIME2 ?CLASS)
                        (not
                              (equal ?TIME1 ?TIME2)))
                  (or
                        (meetsTemporally ?TIME1 ?TIME2)
                        (meetsTemporally ?TIME2 ?TIME1)
                        (earlier ?TIME1 ?TIME2)
                        (earlier ?TIME2 ?TIME1)))))

Jestliže "decomposition of interval into ? interval-types" se rovná class, potom existuje class time tak, že time starts interval.

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (starts ?TIME ?INTERVAL))))

Jestliže "decomposition of interval into ? interval-types" se rovná class, potom existuje class time tak, že time finishes interval.

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (finishes ?TIME ?INTERVAL))))

jestliže "decomposition of interval into ? interval-types" se rovná class,
potom pro všechny time1 platí: jestliže time1 je instancí třídy class a time1 doesn't finish interval, potom existuje class time2 tak, že time1 meets time2

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (not
                              (finishes ?TIME1 ?INTERVAL)))
                  (exists
                        (?TIME2)
                        (and
                              (instance ?TIME2 ?CLASS)
                              (meetsTemporally ?TIME1 ?TIME2))))))

jestliže "decomposition of interval into ? interval-types" se rovná class,
potom pro všechny time1 platí: jestliže time1 je instancí třídy class a time1 doesn't start interval, potom existuje class time2 tak, že time2 meets time1

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (not
                              (starts ?TIME1 ?INTERVAL)))
                  (exists
                        (?TIME2)
                        (and
                              (instance ?TIME2 ?CLASS)
                              (meetsTemporally ?TIME2 ?TIME1))))))

jestliže "decomposition of interval into ? interval-types" se rovná class,
potom pro všechny time platí: jestliže time je instancí třídy okamžik a time je a part of interval, potom existuje class instance tak, že time je a part of instance

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME)
            (=>
                  (and
                        (instance ?TIME TimePoint)
                        (temporalPart ?TIME ?INTERVAL))
                  (exists
                        (?INSTANCE)
                        (and
                              (instance ?INSTANCE ?CLASS)
                              (temporalPart ?TIME ?INSTANCE))))))

Jestliže year je instancí třídy rok, potom "cardinality fn(decomposition of year into ? měsícs)" se rovná .

(=>
      (instance ?YEAR Year)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?YEAR Month))
            12))

Jestliže month je instancí třídy měsíc a duration of month je "number day duration(s)", potom "cardinality fn(decomposition of month into ? dens)" se rovná number.

(=>
      (and
            (instance ?MONTH Month)
            (duration
                  ?MONTH
                  (MeasureFn ?NUMBER DayDuration)))
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MONTH Day))
            ?NUMBER))

Jestliže week je instancí třídy týren, potom "cardinality fn(decomposition of week into ? dens)" se rovná .

(=>
      (instance ?WEEK Week)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?WEEK Day))
            7))

Jestliže day je instancí třídy den, potom "cardinality fn(decomposition of day into ? hodinas)" se rovná .

(=>
      (instance ?DAY Day)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?DAY Hour))
            24))

Jestliže hour je instancí třídy hodina, potom "cardinality fn(decomposition of hour into ? minutas)" se rovná .

(=>
      (instance ?HOUR Hour)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?HOUR Minute))
            60))

Jestliže minute je instancí třídy minuta, potom "cardinality fn(decomposition of minute into ? vteřinas)" se rovná .

(=>
      (instance ?MINUTE Minute)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MINUTE Second))
            60))

obj je instancí třídy spojitý objekt tehdy a jen tehdy pokud pro všechny part1,part2 platí: jestliže obj se rovná "mereological sum fn(part1,part2)", potom part1 je spojen s part2.

(<=>
      (instance ?OBJ SelfConnectedObject)
      (forall
            (?PART1 ?PART2)
            (=>
                  (equal
                        ?OBJ
                        (MereologicalSumFn ?PART1 ?PART2))
                  (connected ?PART1 ?PART2))))

Jestliže rel je instancí třídy case role a rel(process,obj) holds, potom existuje time tak, že "místo kde process byl v čase time" se překrývá s obj.

(=>
      (and
            (instance ?REL CaseRole)
            (holds ?REL ?PROCESS ?OBJ))
      (exists
            (?TIME)
            (overlapsSpatially
                  (WhereFn ?PROCESS ?TIME)
                  ?OBJ)))

hole je instancí třídy díra tehdy a jen tehdy pokud existuje obj tak, že hole je díra v obj.

(<=>
      (instance ?HOLE Hole)
      (exists
            (?OBJ)
            (hole ?HOLE ?OBJ)))

Jestliže hole je díra v obj, potom obj není instancí třídy díra.

(=>
      (hole ?HOLE ?OBJ)
      (not
            (instance ?OBJ Hole)))

Jestliže hole1 je instancí třídy díra, potom existuje hole2 tak, že hole2 je vlastní částí hole1.

(=>
      (instance ?HOLE1 Hole)
      (exists
            (?HOLE2)
            (properPart ?HOLE2 ?HOLE1)))

Jestliže hole1 je instancí třídy díra a hole2 je vlastní částí hole1, potom existuje obj tak, že hole1 se dotýká obj a hole2 se nedotýká obj.

(=>
      (and
            (instance ?HOLE1 Hole)
            (properPart ?HOLE2 ?HOLE1))
      (exists
            (?OBJ)
            (and
                  (meetsSpatially ?HOLE1 ?OBJ)
                  (not
                        (meetsSpatially ?HOLE2 ?OBJ)))))

fillable je atributem hole1 tehdy a jen tehdy pokud existuje díra hole2 tak, že hole1 je částí hole2.

(<=>
      (attribute ?HOLE1 Fillable)
      (exists
            (?HOLE2)
            (and
                  (instance ?HOLE2 Hole)
                  (part ?HOLE1 ?HOLE2))))

Jestliže proc je instancí třídy proces a subproc je a subprocess of proc, potom existuje time tak, že subproc exists during time.

(=>
      (and
            (instance ?PROC Process)
            (subProcess ?SUBPROC ?PROC))
      (exists
            (?TIME)
            (time ?SUBPROC ?TIME)))

Jestliže proc je instancí třídy biologický proces, potom existuje organismus obj tak, že proc je located at obj.

(=>
      (instance ?PROC BiologicalProcess)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ Organism)
                  (located ?PROC ?OBJ))))

Jestliže proc je instancí třídy biologický proces a org prodělává proc, potom org je instancí třídy organismus.

(=>
      (and
            (instance ?PROC BiologicalProcess)
            (experiencer ?PROC ?ORG))
      (instance ?ORG Organism))

Jestliže birth je instancí třídy narození a agent prodělává birth, potom existuje smrt death tak, že agent prodělává death.

(=>
      (and
            (instance ?BIRTH Birth)
            (experiencer ?BIRTH ?AGENT))
      (exists
            (?DEATH)
            (and
                  (instance ?DEATH Death)
                  (experiencer ?DEATH ?AGENT))))

Jestliže death je instancí třídy smrt a agent prodělává death, potom dead je atributem agent po doba existence death.

(=>
      (and
            (instance ?DEATH Death)
            (experiencer ?DEATH ?AGENT))
      (holdsDuring
            (FutureFn
                  (WhenFn ?DEATH))
            (attribute ?AGENT Dead)))

Jestliže death je instancí třídy smrt a birth je instancí třídy narození a agent prodělává death a agent prodělává birth, potom existuje time tak, že "doba existence birth" meets time a time meets "doba existence death" a living je atributem agent během time.

(=>
      (and
            (instance ?DEATH Death)
            (instance ?BIRTH Birth)
            (experiencer ?DEATH ?AGENT)
            (experiencer ?BIRTH ?AGENT))
      (exists
            (?TIME)
            (and
                  (meetsTemporally
                        (WhenFn ?BIRTH)
                        ?TIME)
                  (meetsTemporally
                        ?TIME
                        (WhenFn ?DEATH))
                  (holdsDuring
                        ?TIME
                        (attribute ?AGENT Living)))))

Jestliže act je instancí třídy zažívání a food je účastníkem act, potom food je instancí třídy jídlo.

(=>
      (and
            (instance ?ACT Ingesting)
            (patient ?ACT ?FOOD))
      (instance ?FOOD Food))

Jestliže act je instancí třídy jedení a food je účastníkem act, potom solid je atributem food.

(=>
      (and
            (instance ?ACT Eating)
            (patient ?ACT ?FOOD))
      (attribute ?FOOD Solid))

Jestliže digest je instancí třídy digesting a organism je původcem digest, potom existuje zažívání ingest tak, že organism je původcem ingest a "doba existence digest" overlaps "doba existence ingest".

(=>
      (and
            (instance ?DIGEST Digesting)
            (agent ?DIGEST ?ORGANISM))
      (exists
            (?INGEST)
            (and
                  (instance ?INGEST Ingesting)
                  (agent ?INGEST ?ORGANISM)
                  (overlapsTemporally
                        (WhenFn ?INGEST)
                        (WhenFn ?DIGEST)))))

Jestliže digest je instancí třídy digesting, potom existuje chemický rozklad decomp tak, že decomp je a subprocess of digest.

(=>
      (instance ?DIGEST Digesting)
      (exists
            (?DECOMP)
            (and
                  (instance ?DECOMP ChemicalDecomposition)
                  (subProcess ?DECOMP ?DIGEST))))

Jestliže rep je instancí třídy replikace a parent je původcem rep a child je výsledkem rep, potom parent je a parent of child.

(=>
      (and
            (instance ?REP Replication)
            (agent ?REP ?PARENT)
            (result ?REP ?CHILD))
      (parent ?CHILD ?PARENT))

Jestliže rep je instancí třídy replikace, potom existuje reprodukční struktura body tak, že body je výsledkem rep.

(=>
      (instance ?REP Replication)
      (exists
            (?BODY)
            (and
                  (instance ?BODY ReproductiveBody)
                  (result ?REP ?BODY))))

Jestliže rep je instancí třídy sexuální reprodukce a organism je výsledkem rep, potom neexistují mother,father tak, že mother je a mother of organism a father je a father of organism.

(=>
      (and
            (instance ?REP SexualReproduction)
            (result ?REP ?ORGANISM))
      (not
            (exists
                  (?MOTHER ?FATHER)
                  (and
                        (mother ?ORGANISM ?MOTHER)
                        (father ?ORGANISM ?FATHER)))))

Jestliže rep je instancí třídy asexuální reprodukce a organism je výsledkem rep, potom neexistují parent1,parent2 tak, že parent1 je a parent of organism a parent2 je a parent of organism a parent1 se nerovná parent2.

(=>
      (and
            (instance ?REP AsexualReproduction)
            (result ?REP ?ORGANISM))
      (not
            (exists
                  (?PARENT1 ?PARENT2)
                  (and
                        (parent ?ORGANISM ?PARENT1)
                        (parent ?ORGANISM ?PARENT2)
                        (not
                              (equal ?PARENT1 ?PARENT2))))))

Jestliže process je instancí třídy psychologický proces, potom existuje zvíře animal tak, že animal prodělává process.

(=>
      (instance ?PROCESS PsychologicalProcess)
      (exists
            (?ANIMAL)
            (and
                  (instance ?ANIMAL Animal)
                  (experiencer ?PROCESS ?ANIMAL))))

Jestliže proc je instancí třídy činnost orgánu nebo tkáně, potom existuje thing tak, že proc je located at thing a thing je instancí třídy orgán nebo thing je instancí třídy tkáň.

(=>
      (instance ?PROC OrganOrTissueProcess)
      (exists
            (?THING)
            (and
                  (located ?PROC ?THING)
                  (or
                        (instance ?THING Organ)
                        (instance ?THING Tissue)))))

Jestliže path je instancí třídy patologický proces a org prodělává path, potom existují part,nemoc disease tak, že part je částí org a disease je atributem part.

(=>
      (and
            (instance ?PATH PathologicProcess)
            (experiencer ?PATH ?ORG))
      (exists
            (?PART ?DISEASE)
            (and
                  (part ?PART ?ORG)
                  (instance ?DISEASE DiseaseOrSyndrome)
                  (attribute ?PART ?DISEASE))))

Jestliže inj je instancí třídy zranění, potom existuje anatomická struktura struct tak, že struct je účastníkem inj.

(=>
      (instance ?INJ Injuring)
      (exists
            (?STRUCT)
            (and
                  (instance ?STRUCT AnatomicalStructure)
                  (patient ?INJ ?STRUCT))))

inj je instancí třídy zranění tehdy a jen tehdy pokud inj je instancí třídy poškození a organismus je účastníkem inj.

(<=>
      (instance ?INJ Injuring)
      (and
            (instance ?INJ Damaging)
            (patient ?INJ Organism)))

Jestliže poison je instancí třídy otrávení, potom existuje thing tak, že thing je účastníkem poison a thing je instancí třídy organismus nebo thing je instancí třídy anatomická struktura.

(=>
      (instance ?POISON Poisoning)
      (exists
            (?THING)
            (and
                  (patient ?POISON ?THING)
                  (or
                        (instance ?THING Organism)
                        (instance ?THING AnatomicalStructure)))))

Jestliže poison je instancí třídy otrávení, potom existuje biologicky aktivní látka substance tak, že substance je nástrojem for poison.

(=>
      (instance ?POISON Poisoning)
      (exists
            (?SUBSTANCE)
            (and
                  (instance ?SUBSTANCE BiologicallyActiveSubstance)
                  (instrument ?POISON ?SUBSTANCE))))

Jestliže proc je instancí třídy záměrný proces a agent je původcem proc, potom existuje purp tak, že proc has purpose purp for agent.

(=>
      (and
            (instance ?PROC IntentionalProcess)
            (agent ?PROC ?AGENT))
      (exists
            (?PURP)
            (hasPurposeForAgent ?PROC ?PURP ?AGENT)))

Jestliže proc je instancí třídy záměrný proces, potom existuje myslící agent agent tak, že agent je původcem proc.

(=>
      (instance ?PROC IntentionalProcess)
      (exists
            (?AGENT)
            (and
                  (instance ?AGENT CognitiveAgent)
                  (agent ?PROC ?AGENT))))

Jestliže act je instancí třídy organizační proces a agent je původcem act, potom

agent je instancí třídy organizace
existuje organizace org tak, že agent je a členem org

(=>
      (and
            (instance ?ACT OrganizationalProcess)
            (agent ?ACT ?AGENT))
      (or
            (instance ?AGENT Organization)
            (exists
                  (?ORG)
                  (and
                        (instance ?ORG Organization)
                        (member ?AGENT ?ORG)))))

Jestliže act je instancí třídy náboženský proces a agent je původcem act, potom

agent je instancí třídy náboženská organizace
existuje náboženská organizace org tak, že agent je a členem org

(=>
      (and
            (instance ?ACT ReligiousProcess)
            (agent ?ACT ?AGENT))
      (or
            (instance ?AGENT ReligiousOrganization)
            (exists
                  (?ORG)
                  (and
                        (member ?AGENT ?ORG)
                        (instance ?ORG ReligiousOrganization)))))

Jestliže join je instancí třídy nastoupení do organizace a org je instancí třídy organizace a org je původcem join a person je účastníkem join, potom person je a členem org právě po doba existence join.

(=>
      (and
            (instance ?JOIN JoiningAnOrganization)
            (instance ?ORG Organization)
            (agent ?JOIN ?ORG)
            (patient ?JOIN ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?JOIN))
            (member ?PERSON ?ORG)))

Jestliže leave je instancí třídy opuštění organizace a org je instancí třídy organizace a org je původcem leave a person je účastníkem leave, potom person není a členem org právě po doba existence leave.

(=>
      (and
            (instance ?LEAVE LeavingAnOrganization)
            (instance ?ORG Organization)
            (agent ?LEAVE ?ORG)
            (patient ?LEAVE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?LEAVE))
            (not
                  (member ?PERSON ?ORG))))

Jestliže grad je instancí třídy graduování a org je původcem grad a person je účastníkem grad, potom org je instancí třídy vzdělávací organizace.

(=>
      (and
            (instance ?GRAD Graduation)
            (agent ?GRAD ?ORG)
            (patient ?GRAD ?PERSON))
      (instance ?ORG EducationalOrganization))

Jestliže mat je instancí třídy matrikulace a org je původcem mat a person je účastníkem mat, potom org je instancí třídy vzdělávací organizace.

(=>
      (and
            (instance ?MAT Matriculation)
            (agent ?MAT ?ORG)
            (patient ?MAT ?PERSON))
      (instance ?ORG EducationalOrganization))

Jestliže hire je instancí třídy najímání a org je instancí třídy organizace a org je původcem hire a person je účastníkem hire, potom org employs person právě po doba existence hire.

(=>
      (and
            (instance ?HIRE Hiring)
            (instance ?ORG Organization)
            (agent ?HIRE ?ORG)
            (patient ?HIRE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?HIRE))
            (employs ?ORG ?PERSON)))

Jestliže fire je instancí třídy ukončení pracovního poměru a org je instancí třídy organizace a org je původcem fire a person je účastníkem fire, potom org doesn't employ person právě po doba existence fire.

(=>
      (and
            (instance ?FIRE TerminatingEmployment)
            (instance ?ORG Organization)
            (agent ?FIRE ?ORG)
            (patient ?FIRE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?FIRE))
            (not
                  (employs ?ORG ?PERSON))))

Jestliže proc je instancí třídy politický proces, potom existuje vláda gov tak, že gov je původcem proc nebo gov je účastníkem proc.

(=>
      (instance ?PROC PoliticalProcess)
      (exists
            (?GOV)
            (and
                  (instance ?GOV Government)
                  (or
                        (agent ?PROC ?GOV)
                        (patient ?PROC ?GOV)))))

Jestliže increase je instancí třídy zvyšování parametru a obj je účastníkem increase, potom existují unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence increase a "obj unit(s)" se rovná quant2 právě po doba existence increase a quant2 je větší než quant1.

(=>
      (and
            (instance ?INCREASE Increasing)
            (patient ?INCREASE ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?INCREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?INCREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (greaterThan ?QUANT2 ?QUANT1))))

Jestliže heat je instancí třídy zahřívání a obj je účastníkem heat, potom existují jednotka teploty unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence heat a "obj unit(s)" se rovná quant2 právě po doba existence heat a quant2 je větší než quant1.

(=>
      (and
            (instance ?HEAT Heating)
            (patient ?HEAT ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (instance ?UNIT TemperatureMeasure)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?HEAT))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?HEAT))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (greaterThan ?QUANT2 ?QUANT1))))

Jestliže decrease je instancí třídy snižování parametru a obj je účastníkem decrease, potom existují unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence decrease a "obj unit(s)" se rovná quant2 právě po doba existence decrease a quant2 je menší než quant1.

(=>
      (and
            (instance ?DECREASE Decreasing)
            (patient ?DECREASE ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?DECREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?DECREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (lessThan ?QUANT2 ?QUANT1))))

Jestliže cool je instancí třídy ochlazování a obj je účastníkem cool, potom existují jednotka teploty unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence cool a "obj unit(s)" se rovná quant2 právě po doba existence cool a quant2 je menší než quant1.

(=>
      (and
            (instance ?COOL Cooling)
            (patient ?COOL ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (instance ?UNIT TemperatureMeasure)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COOL))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COOL))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (lessThan ?QUANT2 ?QUANT1))))

Jestliže motion je instancí třídy pohyb a obj je účastníkem motion a motion začíná v place, potom obj je located at place právě před doba existence motion.

(=>
      (and
            (instance ?MOTION Motion)
            (patient ?MOTION ?OBJ)
            (origin ?MOTION ?PLACE))
      (holdsDuring
            (ImmediatePastFn
                  (WhenFn ?MOTION))
            (located ?OBJ ?PLACE)))

Jestliže motion je instancí třídy pohyb a obj je účastníkem motion a motion končí v place, potom obj je located at place právě po doba existence motion.

(=>
      (and
            (instance ?MOTION Motion)
            (patient ?MOTION ?OBJ)
            (destination ?MOTION ?PLACE))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?MOTION))
            (located ?OBJ ?PLACE)))

Jestliže motion je instancí třídy tělesný pohyb, potom existují část těla obj,organismus agent tak, že obj je účastníkem motion a agent je původcem motion.

(=>
      (instance ?MOTION BodyMotion)
      (exists
            (?OBJ ?AGENT)
            (and
                  (instance ?OBJ BodyPart)
                  (patient ?MOTION ?OBJ)
                  (instance ?AGENT Organism)
                  (agent ?MOTION ?AGENT))))

Jestliže walk je instancí třídy chůze a agent je původcem walk, potom existuje souš area tak, že agent je located at area.

(=>
      (and
            (instance ?WALK Walking)
            (agent ?WALK ?AGENT))
      (exists
            (?AREA)
            (and
                  (instance ?AREA LandArea)
                  (located ?AGENT ?AREA))))

Jestliže swim je instancí třídy plavání a agent je původcem swim, potom existuje vodní plocha area tak, že agent je located at area.

(=>
      (and
            (instance ?SWIM Swimming)
            (agent ?SWIM ?AGENT))
      (exists
            (?AREA)
            (and
                  (instance ?AREA WaterArea)
                  (located ?AGENT ?AREA))))

Jestliže proc je instancí třídy změna směru, potom existuje směrový atribut attr tak, že

manner(proc,attr) platí právě před doba existence proc a manner(proc,attr) doesn't hold právě po doba existence proc
manner(proc,attr) platí právě po doba existence proc a manner(proc,attr) doesn't hold právě před doba existence proc

(=>
      (instance ?PROC DirectionChange)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR DirectionalAttribute)
                  (or
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?PROC))
                                    (manner ?PROC ?ATTR))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?PROC))
                                    (not
                                          (manner ?PROC ?ATTR))))
                        (and
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?PROC))
                                    (manner ?PROC ?ATTR))
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?PROC))
                                    (not
                                          (manner ?PROC ?ATTR))))))))

Jestliže transfer je instancí třídy přeprava a agent je původcem transfer a patient je účastníkem transfer, potom agent se nerovná patient.

(=>
      (and
            (instance ?TRANSFER Transfer)
            (agent ?TRANSFER ?AGENT)
            (patient ?TRANSFER ?PATIENT))
      (not
            (equal ?AGENT ?PATIENT)))

Jestliže remove je instancí třídy odstranění a remove začíná v place a obj je účastníkem remove, potom obj je located at place právě před doba existence remove a obj není located at place právě po doba existence remove.

(=>
      (and
            (instance ?REMOVE Removing)
            (origin ?REMOVE ?PLACE)
            (patient ?REMOVE ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?REMOVE))
                  (located ?OBJ ?PLACE))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?REMOVE))
                  (not
                        (located ?OBJ ?PLACE)))))

Jestliže put je instancí třídy uložení a put končí v place a obj je účastníkem put, potom obj není located at place právě před doba existence put a obj je located at place právě po doba existence put.

(=>
      (and
            (instance ?PUT Putting)
            (destination ?PUT ?PLACE)
            (patient ?PUT ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?PUT))
                  (not
                        (located ?OBJ ?PLACE)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?PUT))
                  (located ?OBJ ?PLACE))))

Jestliže sub je instancí třídy záměna, potom existují uložení put,odstranění remove,obj1,obj2,place tak, že put je a subprocess of sub a remove je a subprocess of sub a obj1 je účastníkem remove a remove začíná v place a obj2 je účastníkem put a put končí v place a obj1 se nerovná obj2.

(=>
      (instance ?SUB Substituting)
      (exists
            (?PUT ?REMOVE ?OBJ1 ?OBJ2 ?PLACE)
            (and
                  (instance ?PUT Putting)
                  (instance ?REMOVE Removing)
                  (subProcess ?PUT ?SUB)
                  (subProcess ?REMOVE ?SUB)
                  (patient ?REMOVE ?OBJ1)
                  (origin ?REMOVE ?PLACE)
                  (patient ?PUT ?OBJ2)
                  (destination ?PUT ?PLACE)
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

Jestliže touch je instancí třídy dotyk a obj1 je původcem touch a obj2 je účastníkem touch, potom obj1 je spojen s obj2 právě po doba existence touch.

(=>
      (and
            (instance ?TOUCH Touching)
            (agent ?TOUCH ?OBJ1)
            (patient ?TOUCH ?OBJ2))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?TOUCH))
            (connected ?OBJ1 ?OBJ2)))

Jestliže impact je instancí třídy náraz a obj je účastníkem impact, potom existuje let impel tak, že obj je účastníkem impel a "doba existence impel" happens earlier than "doba existence impact".

(=>
      (and
            (instance ?IMPACT Impacting)
            (patient ?IMPACT ?OBJ))
      (exists
            (?IMPEL)
            (and
                  (instance ?IMPEL Impelling)
                  (patient ?IMPEL ?OBJ)
                  (earlier
                        (WhenFn ?IMPEL)
                        (WhenFn ?IMPACT)))))

Jestliže trans je instancí třídy transport, potom existuje transportní zařízení device tak, že device je nástrojem for trans.

(=>
      (instance ?TRANS Transportation)
      (exists
            (?DEVICE)
            (and
                  (instance ?DEVICE TransportationDevice)
                  (instrument ?TRANS ?DEVICE))))

Jestliže steer je instancí třídy řízení, potom existuje transportní zařízení vehicle tak, že vehicle je účastníkem steer.

(=>
      (instance ?STEER Steering)
      (exists
            (?VEHICLE)
            (and
                  (instance ?VEHICLE TransportationDevice)
                  (patient ?STEER ?VEHICLE))))

Jestliže education je instancí třídy vzdělávací proces a person je účastníkem education, potom education has purpose "existuje učení se learn tak, že person je účastníkem learn".

(=>
      (and
            (instance ?EDUCATION EducationalProcess)
            (patient ?EDUCATION ?PERSON))
      (hasPurpose
            ?EDUCATION
            (exists
                  (?LEARN)
                  (and
                        (instance ?LEARN Learning)
                        (patient ?LEARN ?PERSON)))))

Jestliže change je instancí třídy změna vlastnictví a obj je účastníkem change a agent1 posesses obj právě před doba existence change a agent2 posesses obj právě po doba existence change, potom agent1 se nerovná agent2.

(=>
      (and
            (instance ?CHANGE ChangeOfPossession)
            (patient ?CHANGE ?OBJ)
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT2 ?OBJ)))
      (not
            (equal ?AGENT1 ?AGENT2)))

Jestliže change je instancí třídy změna vlastnictví a change začíná v agent1 a change končí v agent2 a agent2 je instancí třídy původce a obj je účastníkem change, potom agent1 posesses obj právě před doba existence change a agent2 posesses obj právě po doba existence change.

(=>
      (and
            (instance ?CHANGE ChangeOfPossession)
            (origin ?CHANGE ?AGENT1)
            (destination ?CHANGE ?AGENT2)
            (instance ?AGENT2 Agent)
            (patient ?CHANGE ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT2 ?OBJ))))

Jestliže give je instancí třídy dávání a agent1 je původcem give a give končí v agent2 a agent2 je instancí třídy původce a obj je účastníkem give, potom existuje braní get tak, že agent2 je původcem get a get začíná v agent1 a obj je účastníkem get.

(=>
      (and
            (instance ?GIVE Giving)
            (agent ?GIVE ?AGENT1)
            (destination ?GIVE ?AGENT2)
            (instance ?AGENT2 Agent)
            (patient ?GIVE ?OBJ))
      (exists
            (?GET)
            (and
                  (instance ?GET Getting)
                  (agent ?GET ?AGENT2)
                  (origin ?GET ?AGENT1)
                  (patient ?GET ?OBJ))))

Jestliže give je instancí třídy dávání a agent je původcem give, potom give začíná v agent.

(=>
      (and
            (instance ?GIVE Giving)
            (agent ?GIVE ?AGENT))
      (origin ?GIVE ?AGENT))

Jestliže give je instancí třídy jednosměrné dávání, potom neexistuje transakce trans tak, že give je a subprocess of trans.

(=>
      (instance ?GIVE UnilateralGiving)
      (not
            (exists
                  (?TRANS)
                  (and
                        (instance ?TRANS Transaction)
                        (subProcess ?GIVE ?TRANS)))))

Existuje půjčování si borrow tak, že agent1 je původcem borrow a borrow začíná v agent2 a object je účastníkem borrow tehdy a jen tehdy pokud existuje půjčování lend tak, že agent2 je původcem lend a lend končí v agent1 a object je účastníkem lend.

(<=>
      (exists
            (?BORROW)
            (and
                  (instance ?BORROW Borrowing)
                  (agent ?BORROW ?AGENT1)
                  (origin ?BORROW ?AGENT2)
                  (patient ?BORROW ?OBJECT)))
      (exists
            (?LEND)
            (and
                  (instance ?LEND Lending)
                  (agent ?LEND ?AGENT2)
                  (destination ?LEND ?AGENT1)
                  (patient ?LEND ?OBJECT))))

Jestliže get je instancí třídy braní a agent je původcem get, potom get končí v agent.

(=>
      (and
            (instance ?GET Getting)
            (agent ?GET ?AGENT))
      (destination ?GET ?AGENT))

Jestliže get je instancí třídy jednosměrné braní, potom neexistuje transakce trans tak, že get je a subprocess of trans.

(=>
      (instance ?GET UnilateralGetting)
      (not
            (exists
                  (?TRANS)
                  (and
                        (instance ?TRANS Transaction)
                        (subProcess ?GET ?TRANS)))))

Jestliže trans je instancí třídy transakce, potom existují agent1,agent2,dávání give1,dávání give2,obj1,obj2 tak, že give1 je a subprocess of trans a give2 je a subprocess of trans a agent1 je původcem give1 a agent2 je původcem give2 a obj1 je účastníkem give1 a obj2 je účastníkem give2 a give1 končí v agent2 a give2 končí v agent1 a agent1 se nerovná agent2 a obj1 se nerovná obj2.

(=>
      (instance ?TRANS Transaction)
      (exists
            (?AGENT1 ?AGENT2 ?GIVE1 ?GIVE2 ?OBJ1 ?OBJ2)
            (and
                  (instance ?GIVE1 Giving)
                  (instance ?GIVE2 Giving)
                  (subProcess ?GIVE1 ?TRANS)
                  (subProcess ?GIVE2 ?TRANS)
                  (agent ?GIVE1 ?AGENT1)
                  (agent ?GIVE2 ?AGENT2)
                  (patient ?GIVE1 ?OBJ1)
                  (patient ?GIVE2 ?OBJ2)
                  (destination ?GIVE1 ?AGENT2)
                  (destination ?GIVE2 ?AGENT1)
                  (not
                        (equal ?AGENT1 ?AGENT2))
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

Jestliže trans je instancí třídy finanční transakce, potom existuje jednotka měny obj tak, že obj je účastníkem trans.

(=>
      (instance ?TRANS FinancialTransaction)
      (exists
            (?OBJ)
            (and
                  (patient ?TRANS ?OBJ)
                  (instance ?OBJ CurrencyMeasure))))

Jestliže buy je instancí třídy kupování a agent je původcem buy, potom buy končí v agent.

(=>
      (and
            (instance ?BUY Buying)
            (agent ?BUY ?AGENT))
      (destination ?BUY ?AGENT))

Existuje kupování buy tak, že agent1 je původcem buy a buy začíná v agent2 a object je účastníkem buy tehdy a jen tehdy pokud existuje prodávání sell tak, že agent2 je původcem sell a sell končí v agent1 a object je účastníkem sell.

(<=>
      (exists
            (?BUY)
            (and
                  (instance ?BUY Buying)
                  (agent ?BUY ?AGENT1)
                  (origin ?BUY ?AGENT2)
                  (patient ?BUY ?OBJECT)))
      (exists
            (?SELL)
            (and
                  (instance ?SELL Selling)
                  (agent ?SELL ?AGENT2)
                  (destination ?SELL ?AGENT1)
                  (patient ?SELL ?OBJECT))))

Jestliže sell je instancí třídy prodávání a agent je původcem sell, potom sell začíná v agent.

(=>
      (and
            (instance ?SELL Selling)
            (agent ?SELL ?AGENT))
      (origin ?SELL ?AGENT))

Jestliže learn je instancí třídy učení se a agent je původcem learn, potom agent je instancí třídy myslící agent.

(=>
      (and
            (instance ?LEARN Learning)
            (agent ?LEARN ?AGENT))
      (instance ?AGENT CognitiveAgent))

Jestliže existuje učení se learn tak, že agent je původcem learn a prop je účastníkem learn během time, potom agent believes prop právě po time.

(=>
      (holdsDuring
            ?TIME
            (exists
                  (?LEARN)
                  (and
                        (instance ?LEARN Learning)
                        (agent ?LEARN ?AGENT)
                        (patient ?LEARN ?PROP))))
      (holdsDuring
            (ImmediateFutureFn ?TIME)
            (believes ?AGENT ?PROP)))

Jestliže agent je instancí třídy myslící agent, potom agent je capable to do usuzování in role agent.

(=>
      (instance ?AGENT CognitiveAgent)
      (capability Reasoning agent ?AGENT))

Jestliže meas je instancí třídy měření a agent je původcem meas a obj je účastníkem meas, potom existují quant,unit tak, že agent knows "the measure of obj je "quant unit(s)"" právě po doba existence meas.

(=>
      (and
            (instance ?MEAS Measuring)
            (agent ?MEAS ?AGENT)
            (patient ?MEAS ?OBJ))
      (exists
            (?QUANT ?UNIT)
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?MEAS))
                  (knows
                        ?AGENT
                        (measure
                              ?OBJ
                              (MeasureFn ?QUANT ?UNIT))))))

Jestliže count je instancí třídy sčítání a agent je původcem count a entity je účastníkem count, potom existuje number tak, že agent knows ""cardinality fn(entity)" se rovná number".

(=>
      (and
            (instance ?COUNT Counting)
            (agent ?COUNT ?AGENT)
            (patient ?COUNT ?ENTITY))
      (exists
            (?NUMBER)
            (knows
                  ?AGENT
                  (equal
                        (CardinalityFn ?ENTITY)
                        ?NUMBER))))

Jestliže predict je instancí třídy předpovídání a formula je účastníkem predict, potom existuje time tak, že formula platí během time a time happens before doba existence predict nebo time happens earlier than "doba existence predict".

(=>
      (and
            (instance ?PREDICT Predicting)
            (patient ?PREDICT ?FORMULA))
      (exists
            (?TIME)
            (and
                  (holdsDuring ?TIME ?FORMULA)
                  (or
                        (before
                              ?TIME
                              (WhenFn ?PREDICT))
                        (earlier
                              ?TIME
                              (WhenFn ?PREDICT))))))

Jestliže remember je instancí třídy zapamatování a formula je účastníkem remember, potom existuje time tak, že formula platí během time a time happens before doba existence remember nebo time happens earlier than "doba existence remember".

(=>
      (and
            (instance ?REMEMBER Remembering)
            (patient ?REMEMBER ?FORMULA))
      (exists
            (?TIME)
            (and
                  (holdsDuring ?TIME ?FORMULA)
                  (or
                        (before
                              ?TIME
                              (WhenFn ?REMEMBER))
                        (earlier
                              ?TIME
                              (WhenFn ?REMEMBER))))))

Jestliže keep je instancí třídy držení a agent je původcem keep a obj je účastníkem keep, potom existuje uložení put tak, že agent je původcem put a obj je účastníkem put a "doba existence put" happens earlier than "doba existence keep".

(=>
      (and
            (instance ?KEEP Keeping)
            (agent ?KEEP ?AGENT)
            (patient ?KEEP ?OBJ))
      (exists
            (?PUT)
            (and
                  (instance ?PUT Putting)
                  (agent ?PUT ?AGENT)
                  (patient ?PUT ?OBJ)
                  (earlier
                        (WhenFn ?PUT)
                        (WhenFn ?KEEP)))))

jestliže keep je instancí třídy držení a obj je účastníkem keep,
potom existuje place tak, že pro všechny time platí: jestliže time je a part of doba existence keep, potom obj je located at place během time

(=>
      (and
            (instance ?KEEP Keeping)
            (patient ?KEEP ?OBJ))
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (temporalPart
                              ?TIME
                              (WhenFn ?KEEP))
                        (holdsDuring
                              ?TIME
                              (located ?OBJ ?PLACE))))))

Jestliže confine je instancí třídy věznění, potom existuje člověk human tak, že human je účastníkem confine.

(=>
      (instance ?CONFINE Confining)
      (exists
            (?HUMAN)
            (and
                  (instance ?HUMAN Human)
                  (patient ?CONFINE ?HUMAN))))

Jestliže confine je instancí třídy věznění a person je účastníkem confine, potom person doesn't desire "person je účastníkem confine".

(=>
      (and
            (instance ?CONFINE Confining)
            (patient ?CONFINE ?PERSON))
      (not
            (desires
                  ?PERSON
                  (patient ?CONFINE ?PERSON))))

Jestliže repair je instancí třídy oprava a obj je účastníkem repair, potom existuje poškození damage tak, že obj je účastníkem damage a "doba existence damage" happens earlier than "doba existence repair".

(=>
      (and
            (instance ?REPAIR Repairing)
            (patient ?REPAIR ?OBJ))
      (exists
            (?DAMAGE)
            (and
                  (instance ?DAMAGE Damaging)
                  (patient ?DAMAGE ?OBJ)
                  (earlier
                        (WhenFn ?DAMAGE)
                        (WhenFn ?REPAIR)))))

Jestliže proc je instancí třídy terapie a bio je účastníkem proc, potom

bio je instancí třídy organismus
existuje organismus org tak, že bio je částí org

(=>
      (and
            (instance ?PROC TherapeuticProcess)
            (patient ?PROC ?BIO))
      (or
            (instance ?BIO Organism)
            (exists
                  (?ORG)
                  (and
                        (instance ?ORG Organism)
                        (part ?BIO ?ORG)))))

Jestliže act je instancí třídy chirurgie a animal je účastníkem act, potom existuje řezání subact tak, že animal je instancí třídy zvíře a cutting je účastníkem animal a subact je a subprocess of act.

(=>
      (and
            (instance ?ACT Surgery)
            (patient ?ACT ?ANIMAL))
      (exists
            (?SUBACT)
            (and
                  (instance ?SUBACT Cutting)
                  (instance ?ANIMAL Animal)
                  (patient ?ANIMAL ?CUTTING)
                  (subProcess ?SUBACT ?ACT))))

process je instancí třídy zničení tehdy a jen tehdy pokud existuje patient tak, že patient je účastníkem process a patient exists during "právě před doba existence process" a patient doesn't exist during "právě po doba existence process".

(<=>
      (instance ?PROCESS Destruction)
      (exists
            (?PATIENT)
            (and
                  (patient ?PROCESS ?PATIENT)
                  (time
                        ?PATIENT
                        (ImmediatePastFn
                              (WhenFn ?PROCESS)))
                  (not
                        (time
                              ?PATIENT
                              (ImmediateFutureFn
                                    (WhenFn ?PROCESS)))))))

Jestliže kill je instancí třídy zabití a agent je původcem kill a patient je účastníkem kill, potom agent je instancí třídy organismus a patient je instancí třídy organismus.

(=>
      (and
            (instance ?KILL Killing)
            (agent ?KILL ?AGENT)
            (patient ?KILL ?PATIENT))
      (and
            (instance ?AGENT Organism)
            (instance ?PATIENT Organism)))

Jestliže kill je instancí třídy zabití a patient je účastníkem kill, potom living je atributem patient právě před doba existence kill a dead je atributem patient po doba existence kill.

(=>
      (and
            (instance ?KILL Killing)
            (patient ?KILL ?PATIENT))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?KILL))
                  (attribute ?PATIENT Living))
            (holdsDuring
                  (FutureFn
                        (WhenFn ?KILL))
                  (attribute ?PATIENT Dead))))

Jestliže poke je instancí třídy propíchnutí a agent je původcem poke a obj je účastníkem poke a inst je nástrojem for poke, potom inst spojuje agent a obj doba existence poke.

(=>
      (and
            (instance ?POKE Poking)
            (agent ?POKE ?AGENT)
            (patient ?POKE ?OBJ)
            (instrument ?POKE ?INST))
      (holdsDuring
            (WhenFn ?POKE)
            (connects ?INST ?AGENT ?OBJ)))

Jestliže attach je instancí třídy připojení a obj1 je účastníkem attach a obj2 je účastníkem attach, potom obj1 není spojen s obj2 právě před doba existence attach a obj1 je spojen s obj2 právě po doba existence attach.

(=>
      (and
            (instance ?ATTACH Attaching)
            (patient ?ATTACH ?OBJ1)
            (patient ?ATTACH ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?ATTACH))
                  (not
                        (connected ?OBJ1 ?OBJ2)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?ATTACH))
                  (connected ?OBJ1 ?OBJ2))))

Jestliže detach je instancí třídy odpojení a obj1 je účastníkem detach a obj2 je účastníkem detach, potom obj1 je spojen s obj2 právě před doba existence detach a obj1 není spojen s obj2 právě po doba existence detach.

(=>
      (and
            (instance ?DETACH Detaching)
            (patient ?DETACH ?OBJ1)
            (patient ?DETACH ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?DETACH))
                  (connected ?OBJ1 ?OBJ2))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?DETACH))
                  (not
                        (connected ?OBJ1 ?OBJ2)))))

combine je instancí třídy spojení a obj1 je nástrojem pro combine a obj2 je výsledkem combine tehdy a jen tehdy pokud obj1 není částí obj2 právě před doba existence combine a obj1 je částí obj2 právě po doba existence combine.

(<=>
      (and
            (instance ?COMBINE Combining)
            (resource ?COMBINE ?OBJ1)
            (result ?COMBINE ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?COMBINE))
                  (not
                        (part ?OBJ1 ?OBJ2)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?COMBINE))
                  (part ?OBJ1 ?OBJ2))))

Jestliže

proc je instancí třídy chemický proces
stuff je nástrojem pro proc nebo stuff je výsledkem proc

, potom stuff je instancí třídy čistá látka.

(=>
      (and
            (instance ?PROC ChemicalProcess)
            (or
                  (resource ?PROC ?STUFF)
                  (result ?PROC ?STUFF)))
      (instance ?STUFF PureSubstance))

Jestliže substance1 je nástrojem pro proc a substance2 je výsledkem proc a substance1 je instancí třídy elementární látka a substance2 je instancí třídy sloučenina, potom proc je instancí třídy chemická syntéza.

(=>
      (and
            (resource ?PROC ?SUBSTANCE1)
            (result ?PROC ?SUBSTANCE2)
            (instance ?SUBSTANCE1 ElementalSubstance)
            (instance ?SUBSTANCE2 CompoundSubstance))
      (instance ?PROC ChemicalSynthesis))

compound je instancí třídy sloučenina tehdy a jen tehdy pokud existují elementární látka element1,elementární látka element2,chemická syntéza process tak, že element1 se nerovná element2 a element1 je nástrojem pro process a element2 je nástrojem pro process a compound je výsledkem process.

(<=>
      (instance ?COMPOUND CompoundSubstance)
      (exists
            (?ELEMENT1 ?ELEMENT2 ?PROCESS)
            (and
                  (instance ?ELEMENT1 ElementalSubstance)
                  (instance ?ELEMENT2 ElementalSubstance)
                  (not
                        (equal ?ELEMENT1 ?ELEMENT2))
                  (instance ?PROCESS ChemicalSynthesis)
                  (resource ?PROCESS ?ELEMENT1)
                  (resource ?PROCESS ?ELEMENT2)
                  (result ?PROCESS ?COMPOUND))))

Jestliže substance1 je nástrojem pro proc a substance2 je výsledkem proc a substance1 je instancí třídy sloučenina a substance2 je instancí třídy elementární látka, potom proc je instancí třídy chemický rozklad.

(=>
      (and
            (resource ?PROC ?SUBSTANCE1)
            (result ?PROC ?SUBSTANCE2)
            (instance ?SUBSTANCE1 CompoundSubstance)
            (instance ?SUBSTANCE2 ElementalSubstance))
      (instance ?PROC ChemicalDecomposition))

Jestliže combustion je instancí třídy hoření, potom existují zahřívání heat,vyzařování světla light tak, že heat je a subprocess of combustion a light je a subprocess of combustion.

(=>
      (instance ?COMBUSTION Combustion)
      (exists
            (?HEAT ?LIGHT)
            (and
                  (instance ?HEAT Heating)
                  (instance ?LIGHT RadiatingLight)
                  (subProcess ?HEAT ?COMBUSTION)
                  (subProcess ?LIGHT ?COMBUSTION))))

Jestliže change je instancí třídy interní změna a obj je účastníkem change, potom existuje property tak, že

property je atributem obj právě před doba existence change a property není atributem obj právě po doba existence change
property není atributem obj právě před doba existence change a property je atributem obj právě po doba existence change

(=>
      (and
            (instance ?CHANGE InternalChange)
            (patient ?CHANGE ?OBJ))
      (exists
            (?PROPERTY)
            (or
                  (and
                        (holdsDuring
                              (ImmediatePastFn
                                    (WhenFn ?CHANGE))
                              (attribute ?OBJ ?PROPERTY))
                        (holdsDuring
                              (ImmediateFutureFn
                                    (WhenFn ?CHANGE))
                              (not
                                    (attribute ?OBJ ?PROPERTY))))
                  (and
                        (holdsDuring
                              (ImmediatePastFn
                                    (WhenFn ?CHANGE))
                              (not
                                    (attribute ?OBJ ?PROPERTY)))
                        (holdsDuring
                              (ImmediateFutureFn
                                    (WhenFn ?CHANGE))
                              (attribute ?OBJ ?PROPERTY))))))

Jestliže alt je instancí třídy změna povrchu a obj je účastníkem alt, potom existují part,property tak, že part je a minimální částí obj a property je atributem part právě před doba existence alt a property není atributem part právě po doba existence alt.

(=>
      (and
            (instance ?ALT SurfaceChange)
            (patient ?ALT ?OBJ))
      (exists
            (?PART ?PROPERTY)
            (and
                  (superficialPart ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?ALT))
                        (attribute ?PART ?PROPERTY))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?ALT))
                        (not
                              (attribute ?PART ?PROPERTY))))))

Jestliže alt je instancí třídy změna tvaru a obj je účastníkem alt, potom existuje tvar property tak, že

property je atributem obj právě před doba existence alt a property není atributem obj právě po doba existence alt
property není atributem obj právě před doba existence alt a property je atributem obj právě po doba existence alt

(=>
      (and
            (instance ?ALT ShapeChange)
            (patient ?ALT ?OBJ))
      (exists
            (?PROPERTY)
            (and
                  (instance ?PROPERTY ShapeAttribute)
                  (or
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?ALT))
                                    (attribute ?OBJ ?PROPERTY))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?ALT))
                                    (not
                                          (attribute ?OBJ ?PROPERTY))))
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?ALT))
                                    (not
                                          (attribute ?OBJ ?PROPERTY)))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?ALT))
                                    (attribute ?OBJ ?PROPERTY)))))))

Jestliže coloring je instancí třídy barvení a obj je účastníkem coloring, potom existuje atribut barvy property tak, že property je atributem obj právě před doba existence coloring a property není atributem obj právě po doba existence coloring.

(=>
      (and
            (instance ?COLORING Coloring)
            (patient ?COLORING ?OBJ))
      (exists
            (?PROPERTY)
            (and
                  (instance ?PROPERTY ColorAttribute)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COLORING))
                        (attribute ?OBJ ?PROPERTY))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COLORING))
                        (not
                              (attribute ?OBJ ?PROPERTY))))))

Jestliže develop je instancí třídy tvorba obsahu, potom existuje objekt nesoucí informaci obj tak, že obj je účastníkem develop.

(=>
      (instance ?DEVELOP ContentDevelopment)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (patient ?DEVELOP ?OBJ))))

Jestliže read je instancí třídy čtení, potom existují text text,prop tak, že text contains information prop a realization(read,prop) platí.

(=>
      (instance ?READ Reading)
      (exists
            (?TEXT ?PROP)
            (and
                  (instance ?TEXT Text)
                  (containsInformation ?TEXT ?PROP)
                  (realization ?READ ?PROP))))

Jestliže decode je instancí třídy dekódování a doc1 je účastníkem decode, potom existují encode,doc2,time tak, že doc2 contains information prop a doc1 contains information prop a time je a part of před doba existence decode a encode je instancí třídy kódování a doc2 je účastníkem encode během time.

(=>
      (and
            (instance ?DECODE Decoding)
            (patient ?DECODE ?DOC1))
      (exists
            (?ENCODE ?DOC2 ?TIME)
            (and
                  (containsInformation ?DOC2 ?PROP)
                  (containsInformation ?DOC1 ?PROP)
                  (temporalPart
                        ?TIME
                        (PastFn
                              (WhenFn ?DECODE)))
                  (holdsDuring
                        ?TIME
                        (and
                              (instance ?ENCODE Encoding)
                              (patient ?ENCODE ?DOC2))))))

Jestliže wet je instancí třídy zvlhčování a obj je účastníkem wet, potom wet je atributem obj nebo damp je atributem obj právě po doba existence wet.

(=>
      (and
            (instance ?WET Wetting)
            (patient ?WET ?OBJ))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?WET))
            (or
                  (attribute ?OBJ Wet)
                  (attribute ?OBJ Damp))))

Jestliže wet je instancí třídy zvlhčování, potom existuje obj tak, že liquid je atributem obj a obj je účastníkem wet.

(=>
      (instance ?WET Wetting)
      (exists
            (?OBJ)
            (and
                  (attribute ?OBJ Liquid)
                  (patient ?WET ?OBJ))))

Jestliže dry je instancí třídy sušení a obj je účastníkem dry, potom dry je atributem obj právě po doba existence dry.

(=>
      (and
            (instance ?DRY Drying)
            (patient ?DRY ?OBJ))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?DRY))
            (attribute ?OBJ Dry)))

Jestliže action je instancí třídy vytváření, potom existuje result tak, že result je výsledkem action.

(=>
      (instance ?ACTION Creation)
      (exists
            (?RESULT)
            (result ?ACTION ?RESULT)))

process je instancí třídy vytváření tehdy a jen tehdy pokud existuje patient tak, že patient je účastníkem process a patient exists during "právě po doba existence process" a patient doesn't exist during "právě před doba existence process".

(<=>
      (instance ?PROCESS Creation)
      (exists
            (?PATIENT)
            (and
                  (patient ?PROCESS ?PATIENT)
                  (time
                        ?PATIENT
                        (ImmediateFutureFn
                              (WhenFn ?PROCESS)))
                  (not
                        (time
                              ?PATIENT
                              (ImmediatePastFn
                                    (WhenFn ?PROCESS)))))))

Existuje konstrukce build tak, že artifact je výsledkem build tehdy a jen tehdy pokud artifact je instancí třídy nemovitost.

(<=>
      (exists
            (?BUILD)
            (and
                  (instance ?BUILD Constructing)
                  (result ?BUILD ?ARTIFACT)))
      (instance ?ARTIFACT StationaryArtifact))

Jestliže pub je instancí třídy publikování a text je účastníkem pub, potom text je podtřídou text.

(=>
      (and
            (instance ?PUB Publication)
            (patient ?PUB ?TEXT))
      (subclass ?TEXT Text))

Jestliže cook je instancí třídy vaření, potom existuje jídlo food tak, že food je výsledkem cook.

(=>
      (instance ?COOK Cooking)
      (exists
            (?FOOD)
            (and
                  (instance ?FOOD Food)
                  (result ?COOK ?FOOD))))

Jestliže search je instancí třídy hledání a agent je původcem search a entity je účastníkem search, potom agent je interested in entity.

(=>
      (and
            (instance ?SEARCH Searching)
            (agent ?SEARCH ?AGENT)
            (patient ?SEARCH ?ENTITY))
      (inScopeOfInterest ?AGENT ?ENTITY))

Jestliže pursue je instancí třídy sledování a agent je původcem pursue a obj je účastníkem pursue, potom agent wants obj během pursue.

(=>
      (and
            (instance ?PURSUE Pursuing)
            (agent ?PURSUE ?AGENT)
            (patient ?PURSUE ?OBJ))
      (holdsDuring
            ?PURSUE
            (wants ?AGENT ?OBJ)))

Jestliže pursue je instancí třídy sledování a agent je původcem pursue a obj je účastníkem pursue, potom agent doesn't posess obj během pursue.

(=>
      (and
            (instance ?PURSUE Pursuing)
            (agent ?PURSUE ?AGENT)
            (patient ?PURSUE ?OBJ))
      (holdsDuring
            ?PURSUE
            (not
                  (possesses ?AGENT ?OBJ))))

Jestliže investigate je instancí třídy vyšetřování a prop je účastníkem investigate, potom prop je instancí třídy formule.

(=>
      (and
            (instance ?INVESTIGATE Investigating)
            (patient ?INVESTIGATE ?PROP))
      (instance ?PROP Formula))

Jestliže investigate je instancí třídy vyšetřování a agent je původcem investigate a prop je účastníkem investigate, potom agent doesn't know prop doba existence investigate.

(=>
      (and
            (instance ?INVESTIGATE Investigating)
            (agent ?INVESTIGATE ?AGENT)
            (patient ?INVESTIGATE ?PROP))
      (holdsDuring
            (WhenFn ?INVESTIGATE)
            (not
                  (knows ?AGENT ?PROP))))

Jestliže proc je instancí třídy diagnostický proces a agent je původcem proc, potom existuje cause tak, že proc has purpose "agent knows "cause causes proc"" for agent.

(=>
      (and
            (instance ?PROC DiagnosticProcess)
            (agent ?PROC ?AGENT))
      (exists
            (?CAUSE)
            (hasPurposeForAgent
                  ?PROC
                  (knows
                        ?AGENT
                        (causes ?CAUSE ?PROC))
                  ?AGENT)))

Jestliže interaction je instancí třídy sociální interakce, potom existují agent1,agent2 tak, že agent1 je původcem interaction a agent2 je původcem interaction a agent1 se nerovná agent2.

(=>
      (instance ?INTERACTION SocialInteraction)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (agent ?INTERACTION ?AGENT1)
                  (agent ?INTERACTION ?AGENT2)
                  (not
                        (equal ?AGENT1 ?AGENT2)))))

Jestliže pretend je instancí třídy předstírání, potom existují person,prop tak, že pretend has purpose "person believes prop" a prop is true.

(=>
      (instance ?PRETEND Pretending)
      (exists
            (?PERSON ?PROP)
            (and
                  (hasPurpose
                        ?PRETEND
                        (believes ?PERSON ?PROP))
                  (true ?PROP True))))

Jestliže communicate je instancí třídy komunikace, potom existují objekt nesoucí informaci obj,myslící agent agent1,myslící agent agent2 tak, že obj je účastníkem communicate a agent1 je původcem communicate a communicate končí v agent2.

(=>
      (instance ?COMMUNICATE Communication)
      (exists
            (?OBJ ?AGENT1 ?AGENT2)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (patient ?COMMUNICATE ?OBJ)
                  (instance ?AGENT1 CognitiveAgent)
                  (agent ?COMMUNICATE ?AGENT1)
                  (instance ?AGENT2 CognitiveAgent)
                  (destination ?COMMUNICATE ?AGENT2))))

Jestliže disseminate je instancí třídy šíření, potom existují myslící agent agent1,myslící agent agent2 tak, že disseminate končí v agent1 a disseminate končí v agent2 a agent1 se nerovná agent2.

(=>
      (instance ?DISSEMINATE Disseminating)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (destination ?DISSEMINATE ?AGENT1)
                  (instance ?AGENT1 CognitiveAgent)
                  (destination ?DISSEMINATE ?AGENT2)
                  (instance ?AGENT2 CognitiveAgent)
                  (not
                        (equal ?AGENT1 ?AGENT2)))))

Jestliže advert je instancí třídy propagace, potom existuje obj tak, že refers(advert,obj) platí a advert has purpose "existuje prodávání sale tak, že obj je účastníkem sale".

(=>
      (instance ?ADVERT Advertising)
      (exists
            (?OBJ)
            (and
                  (refers ?ADVERT ?OBJ)
                  (hasPurpose
                        ?ADVERT
                        (exists
                              (?SALE)
                              (and
                                    (instance ?SALE Selling)
                                    (patient ?SALE ?OBJ)))))))

Jestliže communicate je instancí třídy linguistic communication, potom existuje lingvistický výraz obj tak, že obj je účastníkem communicate.

(=>
      (instance ?COMMUNICATE LinguisticCommunication)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ LinguisticExpression)
                  (patient ?COMMUNICATE ?OBJ))))

Jestliže state je instancí třídy tvrzení a agent je původcem state a formula je účastníkem state a formula je instancí třídy formule, potom agent believes formula doba existence state.

(=>
      (and
            (instance ?STATE Stating)
            (agent ?STATE ?AGENT)
            (patient ?STATE ?FORMULA)
            (instance ?FORMULA Formula))
      (holdsDuring
            (WhenFn ?STATE)
            (believes ?AGENT ?FORMULA)))

Jestliže order je instancí třídy příkaz a formula je účastníkem order, potom modal attribute(formula,obligation) platí.

(=>
      (and
            (instance ?ORDER Ordering)
            (patient ?ORDER ?FORMULA))
      (modalAttribute ?FORMULA Obligation))

Jestliže request je instancí třídy požadavek a agent je původcem request a formula je účastníkem request a formula je instancí třídy formule, potom agent desires formula.

(=>
      (and
            (instance ?REQUEST Requesting)
            (agent ?REQUEST ?AGENT)
            (patient ?REQUEST ?FORMULA)
            (instance ?FORMULA Formula))
      (desires ?AGENT ?FORMULA))

Jestliže question je instancí třídy dotaz a agent je původcem question a formula je účastníkem question a formula je instancí třídy formule, potom agent doesn't know formula doba existence question.

(=>
      (and
            (instance ?QUESTION Questioning)
            (agent ?QUESTION ?AGENT)
            (patient ?QUESTION ?FORMULA)
            (instance ?FORMULA Formula))
      (holdsDuring
            (WhenFn ?QUESTION)
            (not
                  (knows ?AGENT ?FORMULA))))

Jestliže commit je instancí třídy závazek a formula je účastníkem commit a formula je instancí třídy formule, potom modal attribute(formula,promise) platí.

(=>
      (and
            (instance ?COMMIT Committing)
            (patient ?COMMIT ?FORMULA)
            (instance ?FORMULA Formula))
      (modalAttribute ?FORMULA Promise))

Jestliže express je instancí třídy vyjádření a agent je původcem express, potom existuje stav mysli state tak, že state je atributem agent a represents(express,state) platí.

(=>
      (and
            (instance ?EXPRESS Expressing)
            (agent ?EXPRESS ?AGENT))
      (exists
            (?STATE)
            (and
                  (instance ?STATE StateOfMind)
                  (attribute ?AGENT ?STATE)
                  (represents ?EXPRESS ?STATE))))

Jestliže declare je instancí třídy deklarace a agent1 je původcem declare, potom existují proc,agent2 tak, že confers right(proc,declare,agent2) platí nebo confers obligation(proc,declare,agent2) platí.

(=>
      (and
            (instance ?DECLARE Declaring)
            (agent ?DECLARE ?AGENT1))
      (exists
            (?PROC ?AGENT2)
            (or
                  (confersRight ?PROC ?DECLARE ?AGENT2)
                  (confersObligation ?PROC ?DECLARE ?AGENT2))))

jestliže cooperate je instancí třídy spolupráce,
potom existuje purp tak, že pro všechny agent platí: jestliže agent je původcem cooperate, potom cooperate has purpose purp for agent

(=>
      (instance ?COOPERATE Cooperation)
      (exists
            (?PURP)
            (forall
                  (?AGENT)
                  (=>
                        (agent ?COOPERATE ?AGENT)
                        (hasPurposeForAgent ?COOPERATE ?PURP ?AGENT)))))

Jestliže meet je instancí třídy setkání a agent1 je původcem meet a agent2 je původcem meet, potom agent1 je near vzhledem k agent2 doba existence meet.

(=>
      (and
            (instance ?MEET Meeting)
            (agent ?MEET ?AGENT1)
            (agent ?MEET ?AGENT2))
      (holdsDuring
            (WhenFn ?MEET)
            (orientation ?AGENT1 ?AGENT2 Near)))

Jestliže meet je instancí třídy setkání, potom existují agent1,agent2 tak, že agent1 je původcem meet a agent2 je původcem meet a meet has purpose "existuje komunikace comm tak, že agent1 je původcem comm a agent2 je původcem comm".

(=>
      (instance ?MEET Meeting)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (agent ?MEET ?AGENT1)
                  (agent ?MEET ?AGENT2)
                  (hasPurpose
                        ?MEET
                        (exists
                              (?COMM)
                              (and
                                    (instance ?COMM Communication)
                                    (agent ?COMM ?AGENT1)
                                    (agent ?COMM ?AGENT2)))))))

Jestliže contest je instancí třídy soutěž, potom existují agent1,agent2,purp1,purp2 tak, že agent1 je původcem contest a agent2 je původcem contest a contest has purpose purp1 for agent1 a contest has purpose purp2 for agent2 a agent1 se nerovná agent2 a purp1 se nerovná purp2.

(=>
      (instance ?CONTEST Contest)
      (exists
            (?AGENT1 ?AGENT2 ?PURP1 ?PURP2)
            (and
                  (agent ?CONTEST ?AGENT1)
                  (agent ?CONTEST ?AGENT2)
                  (hasPurposeForAgent ?CONTEST ?PURP1 ?AGENT1)
                  (hasPurposeForAgent ?CONTEST ?PURP2 ?AGENT2)
                  (not
                        (equal ?AGENT1 ?AGENT2))
                  (not
                        (equal ?PURP1 ?PURP2)))))

Jestliže war je instancí třídy válka, potom existuje bitva battle tak, že battle je a subprocess of war.

(=>
      (instance ?WAR War)
      (exists
            (?BATTLE)
            (and
                  (instance ?BATTLE Battle)
                  (subProcess ?BATTLE ?WAR))))

jestliže war je instancí třídy válka a agent je původcem war,
potom
- agent je instancí třídy národ
- - agent je instancí třídy organizace
  - pro všechny member platí: jestliže member je a členem agent, potom member je instancí třídy národ

(=>
      (and
            (instance ?WAR War)
            (agent ?WAR ?AGENT))
      (or
            (instance ?AGENT Nation)
            (and
                  (instance ?AGENT Organization)
                  (forall
                        (?MEMBER)
                        (=>
                              (member ?MEMBER ?AGENT)
                              (instance ?MEMBER Nation))))))

Jestliže battle je instancí třídy bitva, potom existuje válka war tak, že battle je a subprocess of war.

(=>
      (instance ?BATTLE Battle)
      (exists
            (?WAR)
            (and
                  (instance ?WAR War)
                  (subProcess ?BATTLE ?WAR))))

Jestliže battle je instancí třídy bitva, potom existuje násilná soutěž attack tak, že attack je a subprocess of battle.

(=>
      (instance ?BATTLE Battle)
      (exists
            (?ATTACK)
            (and
                  (instance ?ATTACK ViolentContest)
                  (subProcess ?ATTACK ?BATTLE))))

Jestliže move je instancí třídy manévr, potom existuje soutěž contest tak, že move je a subprocess of contest.

(=>
      (instance ?MOVE Maneuver)
      (exists
            (?CONTEST)
            (and
                  (instance ?CONTEST Contest)
                  (subProcess ?MOVE ?CONTEST))))

Jestliže percept je instancí třídy vnímání a agent je původcem percept, potom agent je instancí třídy zvíře.

(=>
      (and
            (instance ?PERCEPT Perception)
            (agent ?PERCEPT ?AGENT))
      (instance ?AGENT Animal))

Jestliže percept je instancí třídy vnímání a agent je původcem percept a object je účastníkem percept, potom agent notices object.

(=>
      (and
            (instance ?PERCEPT Perception)
            (agent ?PERCEPT ?AGENT)
            (patient ?PERCEPT ?OBJECT))
      (notices ?AGENT ?OBJECT))

Jestliže agent je instancí třídy vnímavý agent, potom agent je capable to do vnímání in role experiencer.

(=>
      (instance ?AGENT SentientAgent)
      (capability Perception experiencer ?AGENT))

Jestliže see je instancí třídy vidění a agent je původcem see a obj je účastníkem see, potom

illuminated je atributem obj
existuje atribut barvy prop tak, že agent knows "prop je atributem obj"

(=>
      (and
            (instance ?SEE Seeing)
            (agent ?SEE ?AGENT)
            (patient ?SEE ?OBJ))
      (and
            (attribute ?OBJ Illuminated)
            (exists
                  (?PROP)
                  (and
                        (instance ?PROP ColorAttribute)
                        (knows
                              ?AGENT
                              (attribute ?OBJ ?PROP))))))

Jestliže smell je instancí třídy cítění a obj je účastníkem smell, potom existuje pach attr tak, že attr je atributem obj.

(=>
      (and
            (instance ?SMELL Smelling)
            (patient ?SMELL ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR OlfactoryAttribute)
                  (attribute ?OBJ ?ATTR))))

Jestliže taste je instancí třídy ochutnání a obj je účastníkem taste, potom existuje chuť attr tak, že attr je atributem obj.

(=>
      (and
            (instance ?TASTE Tasting)
            (patient ?TASTE ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR TasteAttribute)
                  (attribute ?OBJ ?ATTR))))

Jestliže hear je instancí třídy slyšení a obj je účastníkem hear, potom existuje zvuk attr tak, že attr je atributem obj.

(=>
      (and
            (instance ?HEAR Hearing)
            (patient ?HEAR ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SoundAttribute)
                  (attribute ?OBJ ?ATTR))))

Jestliže tactile je instancí třídy hmat, potom existuje dotyk touch tak, že touch je a subprocess of tactile.

(=>
      (instance ?TACTILE TactilePerception)
      (exists
            (?TOUCH)
            (and
                  (instance ?TOUCH Touching)
                  (subProcess ?TOUCH ?TACTILE))))

Existuje vyzařování světla emit tak, že region je účastníkem emit a region je instancí třídy oblast tehdy a jen tehdy pokud illuminated je atributem region.

(<=>
      (exists
            (?EMIT)
            (and
                  (instance ?EMIT RadiatingLight)
                  (patient ?EMIT ?REGION)
                  (instance ?REGION Region)))
      (attribute ?REGION Illuminated))

Jestliže emit je instancí třídy vyzařování zvuku a sound je původcem emit, potom existuje zvuk attr tak, že attr je atributem sound.

(=>
      (and
            (instance ?EMIT RadiatingSound)
            (agent ?EMIT ?SOUND))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SoundAttribute)
                  (attribute ?SOUND ?ATTR))))

Jestliže process je instancí třídy změna skupenství a obj je účastníkem process, potom existují part,skupenství state1,skupenství state2 tak, že part je částí obj a state1 se nerovná state2 a state1 je atributem part právě před doba existence process a state2 je atributem part právě po doba existence freeze.

(=>
      (and
            (instance ?PROCESS StateChange)
            (patient ?PROCESS ?OBJ))
      (exists
            (?PART ?STATE1 ?STATE2)
            (and
                  (part ?PART ?OBJ)
                  (instance ?STATE1 PhysicalState)
                  (instance ?STATE2 PhysicalState)
                  (not
                        (equal ?STATE1 ?STATE2))
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?PROCESS))
                        (attribute ?PART ?STATE1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART ?STATE2)))))

Jestliže melt je instancí třídy tání, potom existuje zahřívání heat tak, že heat je a subprocess of melt.

(=>
      (instance ?MELT Melting)
      (exists
            (?HEAT)
            (and
                  (instance ?HEAT Heating)
                  (subProcess ?HEAT ?MELT))))

Jestliže melt je instancí třídy tání a obj je účastníkem melt, potom existuje part tak, že part je částí obj a solid je atributem part právě před doba existence melt a liquid je atributem part právě po doba existence melt.

(=>
      (and
            (instance ?MELT Melting)
            (patient ?MELT ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?MELT))
                        (attribute ?PART Solid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?MELT))
                        (attribute ?PART Liquid)))))

Jestliže boil je instancí třídy var, potom existuje zahřívání heat tak, že heat je a subprocess of boil.

(=>
      (instance ?BOIL Boiling)
      (exists
            (?HEAT)
            (and
                  (instance ?HEAT Heating)
                  (subProcess ?HEAT ?BOIL))))

Jestliže boil je instancí třídy var a obj je účastníkem boil, potom existuje part tak, že part je částí obj a liquid je atributem part právě před doba existence boil a gas je atributem part právě po doba existence boil.

(=>
      (and
            (instance ?BOIL Boiling)
            (patient ?BOIL ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?BOIL))
                        (attribute ?PART Liquid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?BOIL))
                        (attribute ?PART Gas)))))

Jestliže cond je instancí třídy kondenzace, potom existuje ochlazování cool tak, že cool je a subprocess of cond.

(=>
      (instance ?COND Condensing)
      (exists
            (?COOL)
            (and
                  (instance ?COOL Cooling)
                  (subProcess ?COOL ?COND))))

Jestliže cond je instancí třídy kondenzace a obj je účastníkem cond, potom existuje part tak, že part je částí obj a gas je atributem part právě před doba existence cond a liquid je atributem part právě po doba existence cond.

(=>
      (and
            (instance ?COND Condensing)
            (patient ?COND ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COND))
                        (attribute ?PART Gas))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COND))
                        (attribute ?PART Liquid)))))

Jestliže freeze je instancí třídy tuhnutí, potom existuje ochlazování cool tak, že cool je a subprocess of freeze.

(=>
      (instance ?FREEZE Freezing)
      (exists
            (?COOL)
            (and
                  (instance ?COOL Cooling)
                  (subProcess ?COOL ?FREEZE))))

Jestliže freeze je instancí třídy tuhnutí a obj je účastníkem freeze, potom existuje part tak, že part je částí obj a liquid je atributem part právě před doba existence freeze a solid je atributem part právě po doba existence freeze.

(=>
      (and
            (instance ?FREEZE Freezing)
            (patient ?FREEZE ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART Liquid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART Solid)))))

Jestliže area je instancí třídy vodní plocha, potom existují bed,hole,voda water tak, že "principal host fn(hole)" se rovná bed a water přesně zaplňuje hole a "mereological sum fn(bed,water)" se rovná area.

(=>
      (instance ?AREA WaterArea)
      (exists
            (?BED ?HOLE ?WATER)
            (and
                  (equal
                        (PrincipalHostFn ?HOLE)
                        ?BED)
                  (instance ?WATER Water)
                  (properlyFills ?WATER ?HOLE)
                  (equal
                        (MereologicalSumFn ?BED ?WATER)
                        ?AREA))))

Jestliže land1 je instancí třídy souš, potom existuje land2 tak, že land1 je částí land2 a land2 je instancí třídy kontinent nebo land2 je instancí třídy ostrov.

(=>
      (instance ?LAND1 LandArea)
      (exists
            (?LAND2)
            (and
                  (part ?LAND1 ?LAND2)
                  (or
                        (instance ?LAND2 Continent)
                        (instance ?LAND2 Island)))))

Jestliže island je instancí třídy ostrov, potom neexistují souš area,part1,part2 tak, že part1 je částí island a part2 je částí area a island není částí area a area není částí island a part1 je spojen s part2.

(=>
      (instance ?ISLAND Island)
      (not
            (exists
                  (?AREA ?PART1 ?PART2)
                  (and
                        (instance ?AREA LandArea)
                        (part ?PART1 ?ISLAND)
                        (part ?PART2 ?AREA)
                        (not
                              (part ?ISLAND ?AREA))
                        (not
                              (part ?AREA ?ISLAND))
                        (connected ?PART1 ?PART2)))))

Jestliže state je instancí třídy stát nebo provincie, potom existuje národ land tak, že state je vlastní částí land.

(=>
      (instance ?STATE StateOrProvince)
      (exists
            (?LAND)
            (and
                  (instance ?LAND Nation)
                  (properPart ?STATE ?LAND))))

Jestliže organism je instancí třídy organismus, potom existuje narození birth tak, že organism prodělává birth.

(=>
      (instance ?ORGANISM Organism)
      (exists
            (?BIRTH)
            (and
                  (instance ?BIRTH Birth)
                  (experiencer ?BIRTH ?ORGANISM))))

Jestliže parent je a parent of child a class je podtřídou organismus a parent je instancí třídy class, potom child je instancí třídy class.

(=>
      (and
            (parent ?CHILD ?PARENT)
            (subclass ?CLASS Organism)
            (instance ?PARENT ?CLASS))
      (instance ?CHILD ?CLASS))

Jestliže organism je instancí třídy organismus, potom existuje parent tak, že parent je a parent of organism.

(=>
      (instance ?ORGANISM Organism)
      (exists
            (?PARENT)
            (parent ?ORGANISM ?PARENT)))

Jestliže alga je instancí třídy řasa, potom existuje voda water tak, že alga lives in water.

(=>
      (instance ?ALGA Alga)
      (exists
            (?WATER)
            (and
                  (inhabits ?ALGA ?WATER)
                  (instance ?WATER Water))))

Jestliže fungus je instancí třídy houba a fungus lives in obj, potom obj je instancí třídy organismus.

(=>
      (and
            (instance ?FUNGUS Fungus)
            (inhabits ?FUNGUS ?OBJ))
      (instance ?OBJ Organism))

jestliže bacterium je instancí třídy bakterie,
potom existuje buňka cell1 tak, že cell1 je a component of bacterium a pro všechny cell2 platí: jestliže cell2 je a component of bacterium a cell2 je instancí třídy buňka, potom cell1 se rovná cell2

(=>
      (instance ?BACTERIUM Bacterium)
      (exists
            (?CELL1)
            (and
                  (component ?CELL1 ?BACTERIUM)
                  (instance ?CELL1 Cell)
                  (forall
                        (?CELL2)
                        (=>
                              (and
                                    (component ?CELL2 ?BACTERIUM)
                                    (instance ?CELL2 Cell))
                              (equal ?CELL1 ?CELL2))))))

Jestliže bacterium je instancí třídy bakterie a bacterium lives in obj, potom obj je instancí třídy organismus.

(=>
      (and
            (instance ?BACTERIUM Bacterium)
            (inhabits ?BACTERIUM ?OBJ))
      (instance ?OBJ Organism))

jestliže virus je instancí třídy virus,
potom existuje molekula mol1 tak, že mol1 je a component of virus a pro všechny mol2 platí: jestliže mol2 je a component of virus a mol2 je instancí třídy molekula, potom mol1 se rovná mol2

(=>
      (instance ?VIRUS Virus)
      (exists
            (?MOL1)
            (and
                  (component ?MOL1 ?VIRUS)
                  (instance ?MOL1 Molecule)
                  (forall
                        (?MOL2)
                        (=>
                              (and
                                    (component ?MOL2 ?VIRUS)
                                    (instance ?MOL2 Molecule))
                              (equal ?MOL1 ?MOL2))))))

Jestliže virus je instancí třídy virus a virus lives in obj, potom obj je instancí třídy organismus.

(=>
      (and
            (instance ?VIRUS Virus)
            (inhabits ?VIRUS ?OBJ))
      (instance ?OBJ Organism))

Jestliže virus je instancí třídy virus a proc je instancí třídy replikace a virus je původcem proc, potom existuje buňka cell tak, že proc je located at cell.

(=>
      (and
            (instance ?VIRUS Virus)
            (instance ?PROC Replication)
            (agent ?PROC ?VIRUS))
      (exists
            (?CELL)
            (and
                  (located ?PROC ?CELL)
                  (instance ?CELL Cell))))

Jestliže fish je instancí třídy ryba, potom existuje voda water tak, že fish lives in water.

(=>
      (instance ?FISH Fish)
      (exists
            (?WATER)
            (and
                  (inhabits ?FISH ?WATER)
                  (instance ?WATER Water))))

Jestliže organism je instancí třídy toxický organismus, potom existuje biologicky aktivní látka substance tak, že substance je částí organism.

(=>
      (instance ?ORGANISM ToxicOrganism)
      (exists
            (?SUBSTANCE)
            (and
                  (instance ?SUBSTANCE BiologicallyActiveSubstance)
                  (part ?SUBSTANCE ?ORGANISM))))

Jestliže food je instancí třídy jídlo, potom existuje živina nutrient tak, že nutrient je částí food.

(=>
      (instance ?FOOD Food)
      (exists
            (?NUTRIENT)
            (and
                  (instance ?NUTRIENT Nutrient)
                  (part ?NUTRIENT ?FOOD))))

jestliže food je instancí třídy jídlo,
potom pro všechny part1 platí: jestliže part1 je částí food, potom existují part2,zvíře animal tak, že part1 je částí part2 a part2 je částí animal

(=>
      (instance ?FOOD Food)
      (forall
            (?PART1)
            (=>
                  (part ?PART1 ?FOOD)
                  (exists
                        (?PART2 ?ANIMAL)
                        (and
                              (part ?PART1 ?PART2)
                              (part ?PART2 ?ANIMAL)
                              (instance ?ANIMAL Animal))))))

jestliže meat je instancí třídy maso,
potom pro všechny part platí: jestliže part je částí meat, potom existují subpart,time,animal tak, že subpart je částí part a animal je instancí třídy zvíře a subpart je částí animal během time

(=>
      (instance ?MEAT Meat)
      (forall
            (?PART)
            (=>
                  (part ?PART ?MEAT)
                  (exists
                        (?SUBPART ?TIME ?ANIMAL)
                        (and
                              (part ?SUBPART ?PART)
                              (holdsDuring
                                    ?TIME
                                    (and
                                          (instance ?ANIMAL Animal)
                                          (part ?SUBPART ?ANIMAL))))))))

jestliže veg je instancí třídy ovoce a zelenina,
potom pro všechny part platí: jestliže part je částí veg, potom existují subpart,time,plant tak, že subpart je částí part a plant je instancí třídy rostlina a subpart je částí plant během time

(=>
      (instance ?VEG FruitOrVegetable)
      (forall
            (?PART)
            (=>
                  (part ?PART ?VEG)
                  (exists
                        (?SUBPART ?TIME ?PLANT)
                        (and
                              (part ?SUBPART ?PART)
                              (holdsDuring
                                    ?TIME
                                    (and
                                          (instance ?PLANT Plant)
                                          (part ?SUBPART ?PLANT))))))))

Jestliže bev je instancí třídy nápoj, potom liquid je atributem bev.

(=>
      (instance ?BEV Beverage)
      (attribute ?BEV Liquid))

Jestliže drink je instancí třídy pití a bev je účastníkem drink, potom bev je instancí třídy nápoj.

(=>
      (and
            (instance ?DRINK Drinking)
            (patient ?DRINK ?BEV))
      (instance ?BEV Beverage))

Jestliže anat je instancí třídy anatomická struktura, potom existuje organismus organism tak, že anat je částí organism.

(=>
      (instance ?ANAT AnatomicalStructure)
      (exists
            (?ORGANISM)
            (and
                  (instance ?ORGANISM Organism)
                  (part ?ANAT ?ORGANISM))))

Jestliže part je instancí třídy anatomická struktura, potom existuje buňka cell tak, že cell je částí part.

(=>
      (instance ?PART AnatomicalStructure)
      (exists
            (?CELL)
            (and
                  (instance ?CELL Cell)
                  (part ?CELL ?PART))))

Jestliže part je instancí třídy část těla, potom neexistuje patologický proces proc tak, že part je výsledkem proc.

(=>
      (instance ?PART BodyPart)
      (not
            (exists
                  (?PROC)
                  (and
                        (instance ?PROC PathologicProcess)
                        (result ?PROC ?PART)))))

Jestliže cover je instancí třídy pokožka, potom existuje body tak, že cover je a minimální částí body a body je instancí třídy organismus nebo body je instancí třídy část těla.

(=>
      (instance ?COVER BodyCovering)
      (exists
            (?BODY)
            (and
                  (superficialPart ?COVER ?BODY)
                  (or
                        (instance ?BODY Organism)
                        (instance ?BODY BodyPart)))))

Jestliže junct je instancí třídy tělní kloub, potom existuje část těla struct tak, že junct je a component of struct.

(=>
      (instance ?JUNCT BodyJunction)
      (exists
            (?STRUCT)
            (and
                  (instance ?STRUCT BodyPart)
                  (component ?JUNCT ?STRUCT))))

Jestliže junct je instancí třídy tělní kloub, potom existují část těla struct1,část těla struct2 tak, že junct je spojen s struct1 a junct je spojen s struct2 a struct1 se nerovná struct2.

(=>
      (instance ?JUNCT BodyJunction)
      (exists
            (?STRUCT1 ?STRUCT2)
            (and
                  (connected ?JUNCT ?STRUCT1)
                  (connected ?JUNCT ?STRUCT2)
                  (instance ?STRUCT1 BodyPart)
                  (instance ?STRUCT2 BodyPart)
                  (not
                        (equal ?STRUCT1 ?STRUCT2)))))

Jestliže organ je instancí třídy orgán, potom existuje purp tak, že organ has purpose purp.

(=>
      (instance ?ORGAN Organ)
      (exists
            (?PURP)
            (hasPurpose ?ORGAN ?PURP)))

Jestliže stuff je instancí třídy tkáň, potom existuje buňka part tak, že part je částí stuff.

(=>
      (instance ?STUFF Tissue)
      (exists
            (?PART)
            (and
                  (instance ?PART Cell)
                  (part ?PART ?STUFF))))

Jestliže stuff je instancí třídy tkáň, potom existuje organismus organism tak, že stuff je částí organism.

(=>
      (instance ?STUFF Tissue)
      (exists
            (?ORGANISM)
            (and
                  (instance ?ORGANISM Organism)
                  (part ?STUFF ?ORGANISM))))

Jestliže bone je instancí třídy kost, potom existuje obratlovec vert tak, že bone je částí vert.

(=>
      (instance ?BONE Bone)
      (exists
            (?VERT)
            (and
                  (instance ?VERT Vertebrate)
                  (part ?BONE ?VERT))))

Jestliže morph je instancí třídy morfém, potom neexistuje morfém othermorph tak, že othermorph je částí morph a othermorph se nerovná morph.

(=>
      (instance ?MORPH Morpheme)
      (not
            (exists
                  (?OTHERMORPH)
                  (and
                        (instance ?OTHERMORPH Morpheme)
                        (part ?OTHERMORPH ?MORPH)
                        (not
                              (equal ?OTHERMORPH ?MORPH))))))

Jestliže morph je instancí třídy morfém, potom existuje slovo word tak, že morph je částí word.

(=>
      (instance ?MORPH Morpheme)
      (exists
            (?WORD)
            (and
                  (instance ?WORD Word)
                  (part ?MORPH ?WORD))))

Jestliže word je instancí třídy slovo, potom existuje morfém part tak, že part je částí word.

(=>
      (instance ?WORD Word)
      (exists
            (?PART)
            (and
                  (part ?PART ?WORD)
                  (instance ?PART Morpheme))))

Jestliže phrase je instancí třídy fráze, potom existují slovo part1,slovo part2 tak, že part1 je částí phrase a part2 je částí phrase a part1 se nerovná part2.

(=>
      (instance ?PHRASE Phrase)
      (exists
            (?PART1 ?PART2)
            (and
                  (part ?PART1 ?PHRASE)
                  (part ?PART2 ?PHRASE)
                  (instance ?PART1 Word)
                  (instance ?PART2 Word)
                  (not
                        (equal ?PART1 ?PART2)))))

Jestliže sentence je instancí třídy věta, potom existují rozvité podstatné jméno phrase1,rozvité sloveso phrase2 tak, že phrase1 je částí sentence a phrase2 je částí sentence.

(=>
      (instance ?SENTENCE Sentence)
      (exists
            (?PHRASE1 ?PHRASE2)
            (and
                  (instance ?PHRASE1 NounPhrase)
                  (instance ?PHRASE2 VerbPhrase)
                  (part ?PHRASE1 ?SENTENCE)
                  (part ?PHRASE2 ?SENTENCE))))

Jestliže text je instancí třídy text, potom existuje výrok prop tak, že text contains information prop.

(=>
      (instance ?TEXT Text)
      (exists
            (?PROP)
            (and
                  (instance ?PROP Proposition)
                  (containsInformation ?TEXT ?PROP))))

Jestliže text je instancí třídy text, potom existuje věta part tak, že part je částí text.

(=>
      (instance ?TEXT Text)
      (exists
            (?PART)
            (and
                  (part ?PART ?TEXT)
                  (instance ?PART Sentence))))

Jestliže text je instancí třídy text, potom existuje psaní write tak, že text je výsledkem write.

(=>
      (instance ?TEXT Text)
      (exists
            (?WRITE)
            (and
                  (instance ?WRITE Writing)
                  (result ?WRITE ?TEXT))))

Jestliže sent je instancí třídy věta, potom existují rozvité podstatné jméno noun,rozvité sloveso verb tak, že noun je částí sent a verb je částí sent.

(=>
      (instance ?SENT Sentence)
      (exists
            (?NOUN ?VERB)
            (and
                  (instance ?NOUN NounPhrase)
                  (instance ?VERB VerbPhrase)
                  (part ?NOUN ?SENT)
                  (part ?VERB ?SENT))))

Jestliže authors(agent,text) platí, potom existují process,text instance tak, že agent je původcem process a text je výsledkem process.

(=>
      (authors ?AGENT ?TEXT)
      (exists
            (?PROCESS ?INSTANCE)
            (and
                  (agent ?PROCESS ?AGENT)
                  (instance ?INSTANCE ?TEXT)
                  (result ?PROCESS ?TEXT))))

publishes(org,text) platí tehdy a jen tehdy pokud existuje publikování pub tak, že org je původcem pub a text je účastníkem pub.

(<=>
      (publishes ?ORG ?TEXT)
      (exists
            (?PUB)
            (and
                  (instance ?PUB Publication)
                  (agent ?PUB ?ORG)
                  (patient ?PUB ?TEXT))))

Jestliže "edition fn(text,int1)" se rovná edition1 a "edition fn(text,int2)" se rovná edition2 a int2 je větší než int1 a pub1 je instancí třídy publikování a pub2 je instancí třídy publikování a edition1 je účastníkem pub1 a edition2 je účastníkem pub2 a date of pub1 je date1 a date of pub2 je date2, potom "the end of date1" happens before the end of date2.

(=>
      (and
            (equal
                  (EditionFn ?TEXT ?INT1)
                  ?EDITION1)
            (equal
                  (EditionFn ?TEXT ?INT2)
                  ?EDITION2)
            (greaterThan ?INT2 ?INT1)
            (instance ?PUB1 Publication)
            (instance ?PUB2 Publication)
            (patient ?PUB1 ?EDITION1)
            (patient ?PUB2 ?EDITION2)
            (date ?PUB1 ?DATE1)
            (date ?PUB2 ?DATE2))
      (before
            (EndFn ?DATE1)
            (EndFn ?DATE2)))

Jestliže text je podtřídou periodikum a "series volume fn(text,int1)" se rovná volume1 a "series volume fn(text,int2)" se rovná volume2 a int2 je větší než int1 a pub1 je instancí třídy publikování a pub2 je instancí třídy publikování a volume1 je účastníkem pub1 a volume2 je účastníkem pub2 a date of pub1 je date1 a date of pub2 je date2, potom "the end of date1" happens before the end of date2.

(=>
      (and
            (subclass ?TEXT Periodical)
            (equal
                  (SeriesVolumeFn ?TEXT ?INT1)
                  ?VOLUME1)
            (equal
                  (SeriesVolumeFn ?TEXT ?INT2)
                  ?VOLUME2)
            (greaterThan ?INT2 ?INT1)
            (instance ?PUB1 Publication)
            (instance ?PUB2 Publication)
            (patient ?PUB1 ?VOLUME1)
            (patient ?PUB2 ?VOLUME2)
            (date ?PUB1 ?DATE1)
            (date ?PUB2 ?DATE2))
      (before
            (EndFn ?DATE1)
            (EndFn ?DATE2)))

Jestliže text je instancí třídy shrnutí, potom existuje text text2 tak, že subsumes content instance(text2,text) platí.

(=>
      (instance ?TEXT Summary)
      (exists
            (?TEXT2)
            (and
                  (instance ?TEXT2 Text)
                  (subsumesContentInstance ?TEXT2 ?TEXT))))

Jestliže series je instancí třídy řada, potom existují kniha book1,kniha book2 tak, že subsumes content instance(series,book1) platí a subsumes content instance(series,book2) platí a book1 se nerovná book2.

(=>
      (instance ?SERIES Series)
      (exists
            (?BOOK1 ?BOOK2)
            (and
                  (instance ?BOOK1 Book)
                  (instance ?BOOK2 Book)
                  (subsumesContentInstance ?SERIES ?BOOK1)
                  (subsumesContentInstance ?SERIES ?BOOK2)
                  (not
                        (equal ?BOOK1 ?BOOK2)))))

Jestliže article je instancí třídy článek, potom existuje kniha book tak, že subsumes content instance(book,article) platí.

(=>
      (instance ?ARTICLE Article)
      (exists
            (?BOOK)
            (and
                  (instance ?BOOK Book)
                  (subsumesContentInstance ?BOOK ?ARTICLE))))

Jestliže doc je instancí třídy certifikát a agent posesses doc, potom existuje proc tak, že confers right(proc,doc,agent) platí nebo confers obligation(proc,doc,agent) platí.

(=>
      (and
            (instance ?DOC Certificate)
            (possesses ?AGENT ?DOC))
      (exists
            (?PROC)
            (or
                  (confersRight ?PROC ?DOC ?AGENT)
                  (confersObligation ?PROC ?DOC ?AGENT))))

Jestliže mole je instancí třídy molekula, potom existují atom atom1,atom atom2 tak, že atom1 je částí mole a atom2 je částí mole a atom1 se nerovná atom2.

(=>
      (instance ?MOLE Molecule)
      (exists
            (?ATOM1 ?ATOM2)
            (and
                  (instance ?ATOM1 Atom)
                  (instance ?ATOM2 Atom)
                  (part ?ATOM1 ?MOLE)
                  (part ?ATOM2 ?MOLE)
                  (not
                        (equal ?ATOM1 ?ATOM2)))))

artifact je instancí třídy artefakt tehdy a jen tehdy pokud existuje tvorba making tak, že artifact je výsledkem making.

(<=>
      (instance ?ARTIFACT Artifact)
      (exists
            (?MAKING)
            (and
                  (instance ?MAKING Making)
                  (result ?MAKING ?ARTIFACT))))

Jestliže product je instancí třídy produkt, potom existuje výroba manufacture tak, že product je výsledkem manufacture.

(=>
      (instance ?PRODUCT Product)
      (exists
            (?MANUFACTURE)
            (and
                  (instance ?MANUFACTURE Manufacture)
                  (result ?MANUFACTURE ?PRODUCT))))

jestliže artifact je instancí třídy nemovitost,
potom existuje place tak, že pro všechny time platí: jestliže time happen?{s} before or at "the end of doba existence artifact" a "the beginning of doba existence artifact" happen?{s} before or at time, potom "místo kde artifact byl v čase time" se rovná place

(=>
      (instance ?ARTIFACT StationaryArtifact)
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (and
                              (beforeOrEqual
                                    ?TIME
                                    (EndFn
                                          (WhenFn ?ARTIFACT)))
                              (beforeOrEqual
                                    (BeginFn
                                          (WhenFn ?ARTIFACT))
                                    ?TIME))
                        (equal
                              (WhereFn ?ARTIFACT ?TIME)
                              ?PLACE)))))

Jestliže building je instancí třídy budova, potom existuje člověk human tak, že

human lives in building
existuje act tak, že human je původcem act a act je located at building

(=>
      (instance ?BUILDING Building)
      (exists
            (?HUMAN)
            (and
                  (instance ?HUMAN Human)
                  (or
                        (inhabits ?HUMAN ?BUILDING)
                        (exists
                              (?ACT)
                              (and
                                    (agent ?ACT ?HUMAN)
                                    (located ?ACT ?BUILDING)))))))

Jestliže room je instancí třídy pokoj, potom existuje budova build tak, že room je vlastní částí build.

(=>
      (instance ?ROOM Room)
      (exists
            (?BUILD)
            (and
                  (instance ?BUILD Building)
                  (properPart ?ROOM ?BUILD))))

Jestliže clothing je instancí třídy ošacení, potom existuje tkanina fabric tak, že fabric je částí clothing.

(=>
      (instance ?CLOTHING Clothing)
      (exists
            (?FABRIC)
            (and
                  (instance ?FABRIC Fabric)
                  (part ?FABRIC ?CLOTHING))))

Jestliže device je instancí třídy zařízení, potom existuje proces proc tak, že device je capable to do proc in role instrument.

(=>
      (instance ?DEVICE Device)
      (exists
            (?PROC)
            (and
                  (subclass ?PROC Process)
                  (capability ?PROC instrument ?DEVICE))))

Jestliže device je instancí třídy zařízení, potom existuje proces proc tak, že device has purpose "device je capable to do proc in role instrument".

(=>
      (instance ?DEVICE Device)
      (exists
            (?PROC)
            (and
                  (subclass ?PROC Process)
                  (hasPurpose
                        ?DEVICE
                        (capability ?PROC instrument ?DEVICE)))))

Jestliže instrument je instancí třídy hudební nástroj, potom instrument je capable to do hudba in role instrument.

(=>
      (instance ?INSTRUMENT MusicalInstrument)
      (capability Music instrument ?INSTRUMENT))

Jestliže device je instancí třídy transportní zařízení, potom device je capable to do transport in role instrument.

(=>
      (instance ?DEVICE TransportationDevice)
      (capability Transportation instrument ?DEVICE))

Jestliže weapon je instancí třídy zbraň, potom weapon je capable to do poškození in role instrument.

(=>
      (instance ?WEAPON Weapon)
      (capability Damaging instrument ?WEAPON))

Jestliže weapon je instancí třídy zbraň, potom weapon has purpose "existují poškození dest,patient tak, že patient je účastníkem dest a

patient je instancí třídy nemovitost
patient je instancí třídy zvíře
existuje zvíře animal tak, že animal lives in patient

(=>
      (instance ?WEAPON Weapon)
      (hasPurpose
            ?WEAPON
            (exists
                  (?DEST ?PATIENT)
                  (and
                        (instance ?DEST Damaging)
                        (patient ?DEST ?PATIENT)
                        (or
                              (instance ?PATIENT StationaryArtifact)
                              (instance ?PATIENT Animal)
                              (exists
                                    (?ANIMAL)
                                    (and
                                          (instance ?ANIMAL Animal)
                                          (inhabits ?ANIMAL ?PATIENT))))))))

jestliže machine je instancí třídy stroj,
potom pro všechny proc platí: jestliže machine je nástrojem for proc, potom existují resource,result tak, že resource je nástrojem pro proc a result je výsledkem proc

(=>
      (instance ?MACHINE Machine)
      (forall
            (?PROC)
            (=>
                  (instrument ?PROC ?MACHINE)
                  (exists
                        (?RESOURCE ?RESULT)
                        (and
                              (resource ?PROC ?RESOURCE)
                              (result ?PROC ?RESULT))))))

Jestliže comp je instancí třídy inženýrská komponenta, potom existuje zařízení device tak, že comp je a component of device.

(=>
      (instance ?COMP EngineeringComponent)
      (exists
            (?DEVICE)
            (and
                  (instance ?DEVICE Device)
                  (component ?COMP ?DEVICE))))

Jestliže connected engineering components(comp1,comp2) platí, potom comp1 není instancí třídy spojení inženýrských komponent a comp2 není instancí třídy spojení inženýrských komponent.

(=>
      (connectedEngineeringComponents ?COMP1 ?COMP2)
      (not
            (or
                  (instance ?COMP1 EngineeringConnection)
                  (instance ?COMP2 EngineeringConnection))))

Jestliže connection je instancí třídy spojení inženýrských komponent, potom existují comp1,comp2 tak, že connects engineering components(connection,comp1,comp2) platí.

(=>
      (instance ?CONNECTION EngineeringConnection)
      (exists
            (?COMP1 ?COMP2)
            (connectsEngineeringComponents ?CONNECTION ?COMP1 ?COMP2)))

Jestliže group je instancí třídy skupina a memb je a členem group, potom memb je instancí třídy původce.

(=>
      (and
            (instance ?GROUP Group)
            (member ?MEMB ?GROUP))
      (instance ?MEMB Agent))

jestliže group je instancí třídy věková skupina,
potom pro všechny memb1,memb2,age1,age2 platí: jestliže memb1 je a členem group a memb2 je a členem group a age(memb1,age1) platí a age(memb2,age2) platí, potom age1 se rovná age2

(=>
      (instance ?GROUP AgeGroup)
      (forall
            (?MEMB1 ?MEMB2 ?AGE1 ?AGE2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP)
                        (age ?MEMB1 ?AGE1)
                        (age ?MEMB2 ?AGE2))
                  (equal ?AGE1 ?AGE2))))

jestliže group je instancí třídy rodinná skupina,
potom pro všechny memb1,memb2 platí: jestliže memb1 je a členem group a memb2 je a členem group, potom family relation(memb1,memb2) platí

(=>
      (instance ?GROUP FamilyGroup)
      (forall
            (?MEMB1 ?MEMB2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP))
                  (familyRelation ?MEMB1 ?MEMB2))))

Jestliže "organization fn(unit)" se rovná org a attr je instancí třídy objektivní atribut, potom attr je atributem unit tehdy a jen tehdy pokud attr je atributem org.

(=>
      (and
            (equal
                  (OrganizationFn ?UNIT)
                  ?ORG)
            (instance ?ATTR NormativeAttribute))
      (<=>
            (attribute ?UNIT ?ATTR)
            (attribute ?ORG ?ATTR)))

Jestliže pol je instancí třídy politická organizace, potom existuje politický proces proc tak, že pol je původcem proc.

(=>
      (instance ?POL PoliticalOrganization)
      (exists
            (?PROC)
            (and
                  (instance ?PROC PoliticalProcess)
                  (agent ?PROC ?POL))))

Jestliže plan je instancí třídy plán a obj je instancí třídy objekt nesoucí informaci a obj contains information plan, potom existuje plánování planning tak, že obj je výsledkem planning.

(=>
      (and
            (instance ?PLAN Plan)
            (instance ?OBJ ContentBearingObject)
            (containsInformation ?OBJ ?PLAN))
      (exists
            (?PLANNING)
            (and
                  (instance ?PLANNING Planning)
                  (result ?PLANNING ?OBJ))))

Jestliže plan je instancí třídy plán, potom existuje purp tak, že plan has purpose purp.

(=>
      (instance ?PLAN Plan)
      (exists
            (?PURP)
            (hasPurpose ?PLAN ?PURP)))

Jestliže item má atribut value a value je instancí třídy pravdivostní hodnota, potom item je instancí třídy věta nebo item je instancí třídy výrok.

(=>
      (and
            (property ?ITEM ?VALUE)
            (instance ?VALUE TruthValue))
      (or
            (instance ?ITEM Sentence)
            (instance ?ITEM Proposition)))

Jestliže obj1 je attr1 vzhledem k obj2 a attr1 je instancí třídy směrový atribut a attr2 je instancí třídy směrový atribut a attr1 se nerovná attr2, potom obj1 není attr2 vzhledem k obj2.

(=>
      (and
            (orientation ?OBJ1 ?OBJ2 ?ATTR1)
            (instance ?ATTR1 DirectionalAttribute)
            (instance ?ATTR2 DirectionalAttribute)
            (not
                  (equal ?ATTR1 ?ATTR2)))
      (not
            (orientation ?OBJ1 ?OBJ2 ?ATTR2)))

Jestliže direct je instancí třídy směrový atribut a obj1 je direct vzhledem k obj2 a obj2 je direct vzhledem k obj3, potom obj2 je mezi obj1 a obj33.

(=>
      (and
            (instance ?DIRECT DirectionalAttribute)
            (orientation ?OBJ1 ?OBJ2 ?DIRECT)
            (orientation ?OBJ2 ?OBJ3 ?DIRECT))
      (between ?OBJ1 ?OBJ2 ?OBJ33))

Jestliže attribute je atributem person a attribute je instancí třídy sociální role, potom person je instancí třídy člověk.

(=>
      (and
            (attribute ?PERSON ?ATTRIBUTE)
            (instance ?ATTRIBUTE SocialRole))
      (instance ?PERSON Human))

Pro všechny org platí: org doesn't employ person a person je instancí třídy člověk tehdy a jen tehdy pokud unemployed je atributem person.

(<=>
      (forall
            (?ORG)
            (and
                  (not
                        (employs ?ORG ?PERSON))
                  (instance ?PERSON Human)))
      (attribute ?PERSON Unemployed))

Jestliže holds obligation(process,agent) platí, potom modal attribute(existuje process instance tak, že agent je původcem instance,obligation) platí.

(=>
      (holdsObligation ?PROCESS ?AGENT)
      (modalAttribute
            (exists
                  (?INSTANCE)
                  (and
                        (instance ?INSTANCE ?PROCESS)
                        (agent ?INSTANCE ?AGENT)))
            Obligation))

Jestliže agent has the right to perform process, potom modal attribute(existuje process instance tak, že agent je původcem instance,permission) platí.

(=>
      (holdsRight ?PROCESS ?AGENT)
      (modalAttribute
            (exists
                  (?INSTANCE)
                  (and
                        (instance ?INSTANCE ?PROCESS)
                        (agent ?INSTANCE ?AGENT)))
            Permission))

Jestliže attr je atributem obj a attr je instancí třídy soutěžní atribut, potom existuje soutěž contest tak, že obj je původcem contest nebo obj je účastníkem contest.

(=>
      (and
            (attribute ?OBJ ?ATTR)
            (instance ?ATTR ContestAttribute))
      (exists
            (?CONTEST)
            (and
                  (instance ?CONTEST Contest)
                  (or
                        (agent ?CONTEST ?OBJ)
                        (patient ?CONTEST ?OBJ)))))

Jestliže obj je instancí třídy roztok, potom liquid je atributem obj.

(=>
      (instance ?OBJ Solution)
      (attribute ?OBJ Liquid))

obj je instancí třídy látka tehdy a jen tehdy pokud existuje skupenství attr tak, že attr je atributem obj.

(<=>
      (instance ?OBJ Substance)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR PhysicalState)
                  (attribute ?OBJ ?ATTR))))

Jestliže perception je instancí třídy vnímání a obj je účastníkem perception, potom existuje vnímatelný attribut prop tak, že prop je atributem obj.

(=>
      (and
            (instance ?PERCEPTION Perception)
            (patient ?PERCEPTION ?OBJ))
      (exists
            (?PROP)
            (and
                  (instance ?PROP PerceptualAttribute)
                  (attribute ?OBJ ?PROP))))

Jestliže obj je instancí třídy jídlo, potom existuje chuť attr tak, že attr je atributem obj.

(=>
      (instance ?OBJ Food)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR TasteAttribute)
                  (attribute ?OBJ ?ATTR))))

jestliže monochromatic je atributem obj a part je a minimální částí obj a color je atributem part a color je instancí třídy základní barva,
potom pro všechny element platí: jestliže element je a minimální částí obj, potom color je atributem element

(=>
      (and
            (attribute ?OBJ Monochromatic)
            (superficialPart ?PART ?OBJ)
            (attribute ?PART ?COLOR)
            (instance ?COLOR PrimaryColor))
      (forall
            (?ELEMENT)
            (=>
                  (superficialPart ?ELEMENT ?OBJ)
                  (attribute ?ELEMENT ?COLOR))))

Jestliže obj je instancí třídy objekt, potom monochromatic je atributem obj nebo polychromatic je atributem obj.

(=>
      (instance ?OBJ Object)
      (or
            (attribute ?OBJ Monochromatic)
            (attribute ?OBJ Polychromatic)))

Jestliže polychromatic je atributem obj, potom existují part1,part2,atribut barvy color1,atribut barvy color2 tak, že part1 je a minimální částí obj a part2 je a minimální částí obj a color1 je atributem part1 a color2 je atributem part2 a color1 se nerovná color2.

(=>
      (attribute ?OBJ Polychromatic)
      (exists
            (?PART1 ?PART2 ?COLOR1 ?COLOR2)
            (and
                  (superficialPart ?PART1 ?OBJ)
                  (superficialPart ?PART2 ?OBJ)
                  (attribute ?PART1 ?COLOR1)
                  (attribute ?PART2 ?COLOR2)
                  (instance ?COLOR1 ColorAttribute)
                  (instance ?COLOR2 ColorAttribute)
                  (not
                        (equal ?COLOR1 ?COLOR2)))))

Jestliže existuje změna tvaru change tak, že obj je účastníkem change, potom pliable je atributem obj.

(=>
      (exists
            (?CHANGE)
            (and
                  (instance ?CHANGE ShapeChange)
                  (patient ?CHANGE ?OBJ)))
      (attribute ?OBJ Pliable))

Jestliže obj je instancí třídy spojitý objekt, potom pliable je atributem obj nebo rigid je atributem obj.

(=>
      (instance ?OBJ SelfConnectedObject)
      (or
            (attribute ?OBJ Pliable)
            (attribute ?OBJ Rigid)))

Jestliže attribute je instancí třídy textura a attribute je atributem obj a surface je povrchem obj, potom attribute je atributem surface.

(=>
      (and
            (instance ?ATTRIBUTE TextureAttribute)
            (attribute ?OBJ ?ATTRIBUTE)
            (surface ?SURFACE ?OBJ))
      (attribute ?SURFACE ?ATTRIBUTE))

Jestliže unbreakable je atributem obj, potom neexistuje poškození damage tak, že obj je účastníkem damage.

(=>
      (attribute ?OBJ Unbreakable)
      (not
            (exists
                  (?DAMAGE)
                  (and
                        (instance ?DAMAGE Damaging)
                        (patient ?DAMAGE ?OBJ)))))

Jestliže att je atributem org a att je instancí třídy biologický attribut, potom org je instancí třídy organismus.

(=>
      (and
            (attribute ?ORG ?ATT)
            (instance ?ATT BiologicalAttribute))
      (instance ?ORG Organism))

Jestliže organism je instancí třídy organismus a organism je původcem process, potom living je atributem organism doba existence process.

(=>
      (and
            (instance ?ORGANISM Organism)
            (agent ?PROCESS ?ORGANISM))
      (holdsDuring
            (WhenFn ?PROCESS)
            (attribute ?ORGANISM Living)))

Jestliže org je instancí třídy organismus, potom existuje attribut života attr tak, že attr je atributem org.

(=>
      (instance ?ORG Organism)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR AnimacyAttribute)
                  (attribute ?ORG ?ATTR))))

Jestliže body je instancí třídy reprodukční struktura a body je částí org a org je instancí třídy organismus, potom female je atributem org.

(=>
      (and
            (instance ?BODY ReproductiveBody)
            (part ?BODY ?ORG)
            (instance ?ORG Organism))
      (attribute ?ORG Female))

Jestliže animal je instancí třídy zvíře, potom existuje pohlaví attr tak, že attr je atributem animal.

(=>
      (instance ?ANIMAL Animal)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SexAttribute)
                  (attribute ?ANIMAL ?ATTR))))

Jestliže fully formed je atributem obj, potom existuje růst growth tak, že obj prodělává growth a non fully formed je atributem obj the beginning of doba existence obj.

(=>
      (attribute ?OBJ FullyFormed)
      (exists
            (?GROWTH)
            (and
                  (instance ?GROWTH Growth)
                  (experiencer ?GROWTH ?OBJ)
                  (holdsDuring
                        (BeginFn
                              (WhenFn ?OBJ))
                        (attribute ?OBJ NonFullyFormed)))))

Jestliže org je instancí třídy organismus, potom existuje attribut stupně vývoje attr tak, že attr je atributem org.

(=>
      (instance ?ORG Organism)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR DevelopmentalAttribute)
                  (attribute ?ORG ?ATTR))))

Jestliže larval je atributem org během time, potom existuje narození birth tak, že org prodělává birth před time.

(=>
      (holdsDuring
            ?TIME
            (attribute ?ORG Larval))
      (holdsDuring
            (PastFn ?TIME)
            (exists
                  (?BIRTH)
                  (and
                        (instance ?BIRTH Birth)
                        (experiencer ?BIRTH ?ORG)))))

Jestliže embryonic je atributem org, potom existuje reprodukční struktura body tak, že org je located at body.

(=>
      (attribute ?ORG Embryonic)
      (exists
            (?BODY)
            (and
                  (instance ?BODY ReproductiveBody)
                  (located ?ORG ?BODY))))

Jestliže embryonic je atributem org během time, potom neexistuje narození birth tak, že org prodělává birth během time.

(=>
      (holdsDuring
            ?TIME
            (attribute ?ORG Embryonic))
      (holdsDuring
            ?TIME
            (not
                  (exists
                        (?BIRTH)
                        (and
                              (instance ?BIRTH Birth)
                              (experiencer ?BIRTH ?ORG))))))

jestliže attr je instancí třídy fyziologický atribut,
potom jestliže attr je atributem organism během time, potom living je atributem organism během time

(=>
      (instance ?ATTR PsychologicalAttribute)
      (=>
            (holdsDuring
                  ?TIME
                  (attribute ?ORGANISM ?ATTR))
            (holdsDuring
                  ?TIME
                  (attribute ?ORGANISM Living))))

Jestliže attr je instancí třídy fyziologický atribut a attr je atributem agent, potom agent je instancí třídy vnímavý agent.

(=>
      (and
            (instance ?ATTR PsychologicalAttribute)
            (attribute ?AGENT ?ATTR))
      (instance ?AGENT SentientAgent))

agent je instancí třídy vnímavý agent a living je atributem agent tehdy a jen tehdy pokud existuje stav vědomí attr tak, že attr je atributem agent.

(<=>
      (and
            (instance ?AGENT SentientAgent)
            (attribute ?AGENT Living))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR ConsciousnessAttribute)
                  (attribute ?AGENT ?ATTR))))

entity je instancí třídy "union fn(class1,class2)" tehdy a jen tehdy pokud entity je instancí třídy class1 nebo entity je instancí třídy class2.

(<=>
      (instance
            ?ENTITY
            (UnionFn ?CLASS1 ?CLASS2))
      (or
            (instance ?ENTITY ?CLASS1)
            (instance ?ENTITY ?CLASS2)))

entity je instancí třídy "intersection fn(class1,class2)" tehdy a jen tehdy pokud entity je instancí třídy class1 a entity je instancí třídy class2.

(<=>
      (instance
            ?ENTITY
            (IntersectionFn ?CLASS1 ?CLASS2))
      (and
            (instance ?ENTITY ?CLASS1)
            (instance ?ENTITY ?CLASS2)))

entity je instancí třídy "complement fn(class)" tehdy a jen tehdy pokud entity není instancí třídy class.

(<=>
      (instance
            ?ENTITY
            (ComplementFn ?CLASS))
      (not
            (instance ?ENTITY ?CLASS)))

Jestliže class1 je instancí třídy množina nebo třída a class2 je instancí třídy množina nebo třída, potom "relative complement fn(class1,class2)" se rovná "intersection fn(class1,complement fn(class2))".

(=>
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass))
      (equal
            (RelativeComplementFn ?CLASS1 ?CLASS2)
            (IntersectionFn
                  ?CLASS1
                  (ComplementFn ?CLASS2))))

entity je instancí třídy "generalized union fn(superclass)" tehdy a jen tehdy pokud existuje superclass class tak, že entity je instancí třídy class.

(<=>
      (instance
            ?ENTITY
            (GeneralizedUnionFn ?SUPERCLASS))
      (exists
            (?CLASS)
            (and
                  (instance ?CLASS ?SUPERCLASS)
                  (instance ?ENTITY ?CLASS))))

entity je instancí třídy "generalized intersection fn(superclass)" tehdy a jen tehdy pokud pro všechny class platí: jestliže class je instancí třídy superclass, potom entity je instancí třídy class.

(<=>
      (instance
            ?ENTITY
            (GeneralizedIntersectionFn ?SUPERCLASS))
      (forall
            (?CLASS)
            (=>
                  (instance ?CLASS ?SUPERCLASS)
                  (instance ?ENTITY ?CLASS))))

subclass je instancí třídy "all subclasses of class" tehdy a jen tehdy pokud subclass je podtřídou class.

(<=>
      (instance
            ?SUBCLASS
            (PowerSetFn ?CLASS))
      (subclass ?SUBCLASS ?CLASS))