forall (forall)

The universal quantifier of predicate logic.

Ontologie

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

logický operátor

forall

Související termín(y)

<=> => and entails exists not or

Typy argumentů

forall(seznam, formule)

Related WordNet synsets

See more related synsets on a separate page.

Axiomy (114)

Jestliže rel1 je inverzní k rel2, potom pro všechny inst1,inst2 platí: rel1(inst1,inst2) holds tehdy a jen tehdy pokud rel2(inst2,inst1) holds.

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

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 thing1 se rovná thing2, potom pro všechny attr platí: thing1 má atribut attr tehdy a jen tehdy pokud thing2 má atribut attr.

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

Jestliže attr1 se rovná attr2, potom pro všechny thing platí: thing má atribut attr1 tehdy a jen tehdy pokud thing má atribut attr2.

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

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 rel1 se rovná rel2, potom pro všechny platí: rel1() holds tehdy a jen tehdy pokud rel2() holds.

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

jestliže list1 se rovná list2,
potom jestliže list1 se rovná "()" a list2 se rovná "()", potom pro všechny number platí: "numberth element of "()"" se rovná "numberth element of "()""

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

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 contrary attribute() platí,
potom pro všechny attr1,attr2 platí:
- jestliže attr1 se rovná "number1th element of "()"" a attr2 se rovná "number2th element of "()"" a number1 se nerovná number2,
- potom jestliže obj má atribut attr1, potom obj nemá atribut attr2

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

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 attr1 je a subattribute of attr2,
potom pro všechny obj platí: jestliže obj má atribut attr1, potom obj má atribut attr2

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

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

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

"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))))

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 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 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 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 class je disjointly decomposed into ,
potom pro všechny item platí: jestliže item je a member of "()", potom item je podtřídou class

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

jestliže class je disjointly decomposed into ,
potom pro všechny item1,item2 platí: jestliže item1 je a member of "()" a item2 je a member of "()" a item1 se nerovná item2, potom item1 je disjoint from item2

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

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 "length of list" se rovná number1, potom pro všechny number2 platí: existuje item tak, že "number2th element of list" se rovná item tehdy a jen tehdy pokud number2 je menší než nebo roven number1.

(=>
      (equal
            (ListLengthFn ?LIST)
            ?NUMBER1)
      (forall
            (?NUMBER2)
            (<=>
                  (exists
                        (?ITEM)
                        (equal
                              (ListOrderFn ?LIST ?NUMBER2)
                              ?ITEM))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

jestliže rel has number argument(s),
potom pro všechny platí: jestliže rel() holds, potom "length of "()"" se rovná number

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

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 list1 je a sublist of list2,
potom pro všechny item platí: jestliže item je a member of list1, potom item je a member of list2

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

jestliže list1 je a sublist of list2,
potom existuje number3 tak, že pro všechny item platí: jestliže item je a member of list1, potom existují number1,number2 tak, že "number1th element of list1" se rovná item a "number2th element of list2" se rovná item a number2 se rovná "(number1+number3)"

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

jestliže list1 starts list2,
potom pro všechny number1,number2 platí: jestliže "length of list1" se rovná number1 a number2 je menší než nebo roven number1, potom "number2th element of list1" se rovná "number2th element of list2"

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

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 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 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 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 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 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 obj1 je an exact copy of obj2,
potom pro všechny attr platí: jestliže attr je atributem obj1, potom attr je atributem obj2

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

jestliže obj je located at region,
potom pro všechny subobj platí: jestliže subobj je částí obj, potom subobj je located at region

(=>
      (located ?OBJ ?REGION)
      (forall
            (?SUBOBJ)
            (=>
                  (part ?SUBOBJ ?OBJ)
                  (located ?SUBOBJ ?REGION))))

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

subsumes content instance(obj1,obj2) platí tehdy a jen tehdy pokud pro všechny info platí: jestliže obj2 contains information info, potom obj1 contains information info.

(<=>
      (subsumesContentInstance ?OBJ1 ?OBJ2)
      (forall
            (?INFO)
            (=>
                  (containsInformation ?OBJ2 ?INFO)
                  (containsInformation ?OBJ1 ?INFO))))

jestliže sub proposition(prop1,prop2) platí,
potom pro všechny obj1,obj2 platí: jestliže obj1 contains information prop1 a obj2 contains information prop2, potom subsumes content instance(obj2,obj1) platí

(=>
      (subProposition ?PROP1 ?PROP2)
      (forall
            (?OBJ1 ?OBJ2)
            (=>
                  (and
                        (containsInformation ?OBJ1 ?PROP1)
                        (containsInformation ?OBJ2 ?PROP2))
                  (subsumesContentInstance ?OBJ2 ?OBJ1))))

jestliže "greatest common divisor fn()" se rovná number,
potom pro všechny element platí: jestliže element je a member of "()", potom "element mod number" se rovná

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?ELEMENT ?NUMBER)
                        0))))

jestliže "greatest common divisor fn()" se rovná number,
potom neexistuje greater tak, že greater je větší než number a pro všechny element platí: jestliže element je a member of "()", potom "element mod greater" se rovná

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?GREATER)
                  (and
                        (greaterThan ?GREATER ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?ELEMENT ?GREATER)
                                          0)))))))

jestliže "least common multiple fn()" se rovná number,
potom pro všechny element platí: jestliže element je a member of "()", potom "number mod element" se rovná

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?NUMBER ?ELEMENT)
                        0))))

jestliže "least common multiple fn()" se rovná number,
potom neexistuje less tak, že less je menší než number a pro všechny element platí: jestliže element je a member of "()", potom "less mod element" se rovná

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?LESS)
                  (and
                        (lessThan ?LESS ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?LESS ?ELEMENT)
                                          0)))))))

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 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 subset je a subset of set,
potom pro všechny element platí: jestliže element je an element of subset, potom element je an element of set

(=>
      (subset ?SUBSET ?SET)
      (forall
            (?ELEMENT)
            (=>
                  (element ?ELEMENT ?SUBSET)
                  (element ?ELEMENT ?SET))))

Jestliže pro všechny element platí: element je an element of set1 tehdy a jen tehdy pokud element je an element of set2, potom set1 se rovná set2.

(=>
      (forall
            (?ELEMENT)
            (<=>
                  (element ?ELEMENT ?SET1)
                  (element ?ELEMENT ?SET2)))
      (equal ?SET1 ?SET2))

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
- "path weight fn(path)" se rovná sum
- subpath je podgrafem path
- arc1 je částí path
- arc weight(arc1,number1) platí
- pro všechny arc2 platí: jestliže arc2 je částí path, potom arc2 je částí subpath nebo arc2 se rovná arc1
,
potom sum se rovná "("path weight fn(subpath)"+number1)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (subGraph ?SUBPATH ?PATH)
            (graphPart ?ARC1 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (forall
                  (?ARC2)
                  (=>
                        (graphPart ?ARC2 ?PATH)
                        (or
                              (graphPart ?ARC2 ?SUBPATH)
                              (equal ?ARC2 ?ARC1)))))
      (equal
            ?SUM
            (AdditionFn
                  (PathWeightFn ?SUBPATH)
                  ?NUMBER1)))

jestliže
- "path weight fn(path)" se rovná sum
- arc1 je částí path
- arc2 je částí path
- arc weight(arc1,number1) platí
- arc weight(arc2,number2) platí
- pro všechny arc3 platí: jestliže arc3 je částí path, potom arc3 se rovná arc1 nebo arc3 se rovná arc2
,
potom "path weight fn(path)" se rovná "(number1+number2)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (graphPart ?ARC1 ?PATH)
            (graphPart ?ARC2 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (arcWeight ?ARC2 ?NUMBER2)
            (forall
                  (?ARC3)
                  (=>
                        (graphPart ?ARC3 ?PATH)
                        (or
                              (equal ?ARC3 ?ARC1)
                              (equal ?ARC3 ?ARC2)))))
      (equal
            (PathWeightFn ?PATH)
            (AdditionFn ?NUMBER1 ?NUMBER2)))

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 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 "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)))))

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 obj1 je larger than obj2,
potom pro všechny quant1,quant2 platí: jestliže the measure of obj1 je "quant1 délková jednotka(s)" a the measure of obj2 je "quant2 délková jednotka(s)", potom quant1 je větší než quant2

(=>
      (larger ?OBJ1 ?OBJ2)
      (forall
            (?QUANT1 ?QUANT2)
            (=>
                  (and
                        (measure
                              ?OBJ1
                              (MeasureFn ?QUANT1 LengthMeasure))
                        (measure
                              ?OBJ2
                              (MeasureFn ?QUANT2 LengthMeasure)))
                  (greaterThan ?QUANT1 ?QUANT2))))

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 "the beginning of interval" se rovná point,
potom pro všechny otherpoint platí: jestliže otherpoint je a part of interval a otherpoint se nerovná point, potom point happens before otherpoint

(=>
      (equal
            (BeginFn ?INTERVAL)
            ?POINT)
      (forall
            (?OTHERPOINT)
            (=>
                  (and
                        (temporalPart ?OTHERPOINT ?INTERVAL)
                        (not
                              (equal ?OTHERPOINT ?POINT)))
                  (before ?POINT ?OTHERPOINT))))

jestliže "the end of interval" se rovná point,
potom pro všechny otherpoint platí: jestliže otherpoint je a part of interval a otherpoint se nerovná point, potom otherpoint happens before point

(=>
      (equal
            (EndFn ?INTERVAL)
            ?POINT)
      (forall
            (?OTHERPOINT)
            (=>
                  (and
                        (temporalPart ?OTHERPOINT ?INTERVAL)
                        (not
                              (equal ?OTHERPOINT ?POINT)))
                  (before ?OTHERPOINT ?POINT))))

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

jestliže obj je výsledkem proc,
potom pro všechny time platí: jestliže time happens before the beginning of doba existence proc, potom obj doesn't exist during time

(=>
      (result ?PROC ?OBJ)
      (forall
            (?TIME)
            (=>
                  (before
                        ?TIME
                        (BeginFn
                              (WhenFn ?PROC)))
                  (not
                        (time ?OBJ ?TIME)))))

Jestliže "interval between point1 and point2" se rovná interval, potom pro všechny point platí: point je between or at point1 and point2 tehdy a jen tehdy pokud point je a part of interval.

(=>
      (equal
            (TimeIntervalFn ?POINT1 ?POINT2)
            ?INTERVAL)
      (forall
            (?POINT)
            (<=>
                  (temporallyBetweenOrEqual ?POINT1 ?POINT ?POINT2)
                  (temporalPart ?POINT ?INTERVAL))))

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

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 obj1 je povrchem obj2,
potom pro všechny obj3 platí: jestliže obj3 je a minimální částí obj2, potom obj3 je částí obj1

(=>
      (surface ?OBJ1 ?OBJ2)
      (forall
            (?OBJ3)
            (=>
                  (superficialPart ?OBJ3 ?OBJ2)
                  (part ?OBJ3 ?OBJ1))))

jestliže obj1 je a interior part of obj2,
potom pro všechny part platí: jestliže part je a minimální částí obj2, potom obj1 se nepřekrývá s part

(=>
      (interiorPart ?OBJ1 ?OBJ2)
      (forall
            (?PART)
            (=>
                  (superficialPart ?PART ?OBJ2)
                  (not
                        (overlapsSpatially ?OBJ1 ?PART)))))

Jestliže obj3 se rovná "mereological sum fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 nebo part je částí obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalSumFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (or
                        (part ?PART ?OBJ1)
                        (part ?PART ?OBJ2)))))

Jestliže obj3 se rovná "mereological product fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 a part je částí obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalProductFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (part ?PART ?OBJ2)))))

Jestliže obj3 se rovná "mereological difference fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 a part není částí obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalDifferenceFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (not
                              (part ?PART ?OBJ2))))))

jestliže hole1 je díra v obj a hole2 je díra v obj,
potom pro všechny hole3 platí: jestliže hole3 je částí "mereological sum fn(hole1,hole2)", potom hole3 je díra v obj

(=>
      (and
            (hole ?HOLE1 ?OBJ)
            (hole ?HOLE2 ?OBJ))
      (forall
            (?HOLE3)
            (=>
                  (part
                        ?HOLE3
                        (MereologicalSumFn ?HOLE1 ?HOLE2))
                  (hole ?HOLE3 ?OBJ))))

Jestliže obj1 se rovná "principal host fn(hole)", potom pro všechny obj2 platí: obj2 se překrývá s obj1 tehdy a jen tehdy pokud existuje obj3 tak, že hole je díra v obj3 a obj2 se překrývá s obj3.

(=>
      (equal
            ?OBJ1
            (PrincipalHostFn ?HOLE))
      (forall
            (?OBJ2)
            (<=>
                  (overlapsSpatially ?OBJ2 ?OBJ1)
                  (exists
                        (?OBJ3)
                        (and
                              (hole ?HOLE ?OBJ3)
                              (overlapsSpatially ?OBJ2 ?OBJ3))))))

jestliže obj1 zcela zaplňuje hole,
potom pro všechny obj2 platí: jestliže obj2 je spojen s hole, potom obj2 je spojen s obj1

(=>
      (completelyFills ?OBJ1 ?HOLE)
      (forall
            (?OBJ2)
            (=>
                  (connected ?OBJ2 ?HOLE)
                  (connected ?OBJ2 ?OBJ1))))

Jestliže obj1 se rovná "skin fn(hole)", potom pro všechny obj2 platí: obj2 se překrývá s obj1 tehdy a jen tehdy pokud existuje obj3 tak, že obj3 je a minimální částí "principal host fn(hole)" a hole se dotýká obj3 a obj2 se překrývá s obj3.

(=>
      (equal
            ?OBJ1
            (SkinFn ?HOLE))
      (forall
            (?OBJ2)
            (<=>
                  (overlapsSpatially ?OBJ2 ?OBJ1)
                  (exists
                        (?OBJ3)
                        (and
                              (superficialPart
                                    ?OBJ3
                                    (PrincipalHostFn ?HOLE))
                              (meetsSpatially ?HOLE ?OBJ3)
                              (overlapsSpatially ?OBJ2 ?OBJ3))))))

jestliže subproc je a subprocess of proc,
potom pro všechny region platí: jestliže proc je located at region, potom subproc je located at region

(=>
      (subProcess ?SUBPROC ?PROC)
      (forall
            (?REGION)
            (=>
                  (located ?PROC ?REGION)
                  (located ?SUBPROC ?REGION))))

jestliže
- path1 je cesta podél které se vyskytuje process
- process začíná v source
- process končí v dest
- délka path1 je measure1
- neexistují path2,measure2 tak, že path2 je cesta podél které se vyskytuje process a process začíná v origin a process končí v dest a délka path2 je measure2 a measure2 je menší než measure1
,
potom pro všechny obj platí: jestliže obj je částí path1, potom obj je mezi source a dest

(=>
      (and
            (path ?PROCESS ?PATH1)
            (origin ?PROCESS ?SOURCE)
            (destination ?PROCESS ?DEST)
            (length ?PATH1 ?MEASURE1)
            (not
                  (exists
                        (?PATH2 ?MEASURE2)
                        (and
                              (path ?PROCESS ?PATH2)
                              (origin ?PROCESS ?ORIGIN)
                              (destination ?PROCESS ?DEST)
                              (length ?PATH2 ?MEASURE2)
                              (lessThan ?MEASURE2 ?MEASURE1)))))
      (forall
            (?OBJ)
            (=>
                  (part ?OBJ ?PATH1)
                  (between ?SOURCE ?OBJ ?DEST))))

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 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 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 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 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 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 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 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 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 direction(proc,attr1) platí během time,
potom pro všechny attr2 platí: jestliže direction(proc,attr2) platí během time, potom attr2 se rovná attr1

(=>
      (holdsDuring
            ?TIME
            (direction ?PROC ?ATTR1))
      (forall
            (?ATTR2)
            (=>
                  (holdsDuring
                        ?TIME
                        (direction ?PROC ?ATTR2))
                  (equal ?ATTR2 ?ATTR1))))

jestliže faces(proc,attr1) platí během time,
potom pro všechny attr2 platí: jestliže faces(proc,attr2) platí během time, potom attr2 se rovná attr1

(=>
      (holdsDuring
            ?TIME
            (faces ?PROC ?ATTR1))
      (forall
            (?ATTR2)
            (=>
                  (holdsDuring
                        ?TIME
                        (faces ?PROC ?ATTR2))
                  (equal ?ATTR2 ?ATTR1))))

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 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 wet je atributem obj,
potom pro všechny part platí: jestliže part je částí obj, potom existuje subpart tak, že subpart je částí part a liquid je atributem subpart

(=>
      (attribute ?OBJ Wet)
      (forall
            (?PART)
            (=>
                  (part ?PART ?OBJ)
                  (exists
                        (?SUBPART)
                        (and
                              (part ?SUBPART ?PART)
                              (attribute ?SUBPART Liquid))))))

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