forall (forall)

The universal quantifier of predicate logic.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

OperatoreLogico

forall

Coordinate term(s)

<=> => and entails exists not or

Type restrictions

forall(Lista, Formula)

Related WordNet synsets

See more related synsets on a separate page.

Axioms (114)

Se rel1 é un inverso di rel2, allora per ogni inst1,inst2 vale: rel1(inst1,inst2 vales se e solo se rel2(inst2,inst1 vales.

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

subclass é una sottoclasse di class se e solo se

subclass é un' istanza di InsiemeOClasse
class é un' istanza di InsiemeOClasse
per ogni inst vale: se inst é un' istanza di subclass, allora inst é un' istanza di class

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

Se thing1 is uguale a thing2, allora per ogni attr vale: thing1 ha un attributo attr se e solo se thing2 ha un attributo attr.

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

Se attr1 is uguale a attr2, allora per ogni thing vale: thing ha un attributo attr1 se e solo se thing ha un attributo attr2.

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

Se thing1 is uguale a thing2, allora per ogni class vale: thing1 é un' istanza di class se e solo se thing2 é un' istanza di class.

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

Se class1 is uguale a class2, allora per ogni thing vale: thing é un' istanza di class1 se e solo se thing é un' istanza di class2.

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

Se rel1 is uguale a rel2, allora per ogni vale: rel1( vales se e solo se rel2( vales.

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

se list1 is uguale a list2,
allora se list1 is uguale a "(" e list2 is uguale a "(", allora per ogni number vale: "numberth elemento di "("" is uguale a "numberth elemento di "(""

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

class1 é disgiunto da class2 se e solo se

class1 é un' istanza di InsiemeOClasse
class2 é un' istanza di InsiemeOClasse
per ogni inst vale: inst é not un' istanza di class1 o inst é not un' istanza di class2

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

se é opposto a ?,
allora per ogni attr1,attr2 vale:
- se attr1 is uguale a "number1th elemento di "("" e attr2 is uguale a "number2th elemento di "("" e number1 is not uguale a number2,
- allora se obj ha un attributo attr1, allora obj ha not un attributo 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))))))

se exhaustive attribute(class,) vale,
allora per ogni obj vale: se attr1 é un' istanza di class, allora esiste attr2 tale che attr2 é un é membro di "(" e attr1 is uguale a attr2

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

se attr1 é un sottoattributo di attr2,
allora per ogni obj vale: se obj ha un attributo attr1, allora obj ha un attributo attr2

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

se substance1 é un membro di substance2,
allora per ogni class vale: se substance1 é un' istanza di class, allora substance2 é un' istanza di class

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

se atom é un' istanza di Atomo,
allora per ogni nucleus1,nucleus2 vale: se nucleus1 é un componente diatom e nucleus2 é un componente diatom e nucleus1 é un' istanza di NucleoAtomico e nucleus2 é un' istanza di NucleoAtomico, allora nucleus1 is uguale a nucleus2

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

coll1 é sottoinsieme un proprio coll2 se e solo se

coll1 é un' istanza di InsiemeConcreto
coll2 é un' istanza di InsiemeConcreto
per ogni member vale: se member é un membro di coll1, allora member é un membro di coll2

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

"la descrizione di class" is uguale a attr se e solo se per ogni inst vale: inst é un' istanza di class se e solo se inst ha un attributo attr.

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

rel é un' istanza di RelazioneMonovalente se e solo se per ogni ,item1,item2 vale: se rel(,item1 vales e rel(,item2 vales, allora item1 is uguale a item2.

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

rel é un' istanza di RelazioneAValoreTotale se e solo se esiste valence tale che rel é un' istanza di Relazione e rel %&ha valence argomento(s e

se per ogni number,element,class vale: se number é meno divalence e il numero number argomenti di rel é un istanza di class e element is uguale a "numberth elemento di "("", allora element é un' istanza di class,
allora esiste item tale che rel(,item vales

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

Se rel é un' istanza di RelazioneNonRiflessiva, allora per ogni inst vale: rel(inst,inst non vale.

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

se rel é un' istanza di RelazioneSimmetrica,
allora per ogni inst1,inst2 vale: se rel(inst1,inst2 vales, allora rel(inst2,inst1 vales

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

se rel é un' istanza di RelazioneAntisimmetrica,
allora per ogni inst1,inst2 vale: se rel(inst1,inst2 vales e rel(inst2,inst1 vales, allora inst1 is uguale a inst2

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

Se rel é un' istanza di RelazioneTricotomizzante, allora per ogni inst1,inst2 vale: rel(inst1,inst2 vales o inst1 is uguale a inst2 o rel(inst2,inst1 vales.

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

se rel é un' istanza di RelazioneTransitiva,
allora per ogni inst1,inst2,inst3 vale: se rel(inst1,inst2 vales e rel(inst2,inst3 vales, allora rel(inst1,inst3 vales

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

se rel é un' istanza di RelazioneIntransitiva,
allora per ogni inst1,inst2,inst3 vale: se rel(inst1,inst2 vales e rel(inst2,inst3 vales, allora rel(inst1,inst3 non vale

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

Se rel é un' istanza di RelazioneDiOrdineTotale, allora per ogni inst1,inst2 vale: rel(inst1,inst2 vales o rel(inst2,inst1 vales.

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

se list é un' istanza di Lista,
allora esiste number1 tale che esiste item1 tale che "number1th elemento di list" is not uguale a item1 e per ogni number2 vale: se number2 é un' istanza di NumeroInteroPositivo e number2 é meno dinumber1, allora esiste item2 tale che "number2th elemento di list" is uguale a 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 é un' istanza di ListaUnica se e solo se per ogni number1,number2 vale: se "number1th elemento di list" is uguale a "number2th elemento di list", allora number1 is uguale a number2.

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

se class é coperto da ,
allora per ogni obj vale: se obj é un' istanza di class, allora esiste item tale che item é un é membro di "(" e obj é un' istanza di item

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

se class é scomposto disgiuntivamente in ,
allora per ogni item vale: se item é un é membro di "(", allora item é una sottoclasse di class

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

se class é scomposto disgiuntivamente in ,
allora per ogni item1,item2 vale: se item1 é un é membro di "(" e item2 é un é membro di "(" e item1 is not uguale a item2, allora item1 é disgiunto da item2

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

Se list1 é un' istanza di Lista e list2 é un' istanza di Lista e per ogni number vale: "numberth elemento di list1" is uguale a "numberth elemento di list2", allora list1 is uguale a list2.

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

Se "lunghezza di list" is uguale a number1, allora per ogni number2 vale: esiste item tale che "number2th elemento di list" is uguale a item se e solo se number2 é minore o uguale a number1.

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

se rel %&ha number argomento(s,
allora per ogni vale: se rel( vales, allora "lunghezza di "("" is uguale a number

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

list3 is uguale a "la lista composta di list1 e list2" se e solo se per ogni number1,number2 vale: se number1 é minore o uguale a "lunghezza di list1" e number2 é minore o uguale a "lunghezza di list2" e number1 é un' istanza di NumeroInteroPositivo e number2 é un' istanza di NumeroInteroPositivo, allora "number1th elemento di list3" is uguale a "number1th elemento di list1" e ""("lunghezza di list1"+number2"th elemento di list3" is uguale a "number2th elemento di 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))))))

se list1 é una sottolista di list2,
allora per ogni item vale: se item é un é membro di list1, allora item é un é membro di list2

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

se list1 é una sottolista di list2,
allora esiste number3 tale che per ogni item vale: se item é un é membro di list1, allora esiste number1,number2 tale che "number1th elemento di list1" is uguale a item e "number2th elemento di list2" is uguale a item e number2 is uguale a "(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))))))))

se list1 inizias list2,
allora per ogni number1,number2 vale: se "lunghezza di list1" is uguale a number1 e number2 é minore o uguale a number1, allora "number2th elemento di list1" is uguale a "number2th elemento di list2"

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

se fun é un' istanza di FunzioneUnoAUno,
allora per ogni arg1,arg2 vale: se il numero argomenti di fun é un istanza di class e arg1 é un' istanza di class e arg2 é un' istanza di class e arg1 is not uguale a arg2, allora "fun(arg1" is not uguale a "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))))))

se function é un' istanza di FunzioneAssociativa,
allora per ogni inst1,inst2,inst3 vale: se il numero argomenti di function é un istanza di class e inst1 é un' istanza di class e inst2 é un' istanza di class e inst3 é un' istanza di class, allora "function(inst1,"function(inst2,inst3"" is uguale a "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)))))

se function é un' istanza di FunzioneCommutativa,
allora per ogni inst1,inst2 vale: se il numero argomenti di function é un istanza di class e inst1 é un' istanza di class e inst2 é un' istanza di class, allora "function(inst1,inst2" is uguale a "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)))))

se function is closed on class e function é un' istanza di FunzioneUnaria,
allora per ogni inst vale: se inst é un' istanza di class, allora "function(inst" é un' istanza di class

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

se function is closed on class e function é un' istanza di FunzioneBinaria,
allora per ogni inst1,inst2 vale: se inst1 é un' istanza di class e inst2 é un' istanza di class, allora "function(inst1,inst2" é un' istanza di class

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

se relation é riflessivo su class,
allora per ogni inst vale: se inst é un' istanza di class, allora relation(inst,inst vales

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

se relation é irriflessivo su class,
allora per ogni inst vale: se inst é un' istanza di class, allora relation(inst,inst non vale

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

se relation é tricotomizzante su class,
allora per ogni inst1,inst2 vale: se inst1 é un' istanza di class e inst2 é un' istanza di class, allora relation(inst1,inst2 vales o relation(inst2,inst1 vales o inst1 is uguale a 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)))))

se function1 é distributivo su function2,
allora per ogni inst1,inst2,inst3 vale: se il numero argomenti di function1 é un istanza di class1 e inst1 é un' istanza di class1 e inst2 é un' istanza di class1 e inst3 é un' istanza di class1 e il numero argomenti di function2 é un istanza di class2 e inst1 é un' istanza di class2 e inst2 é un' istanza di class2 e inst3 é un' istanza di class2, allora "function1(inst1,"function2(inst2,inst3"" is uguale a "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))))))

se causes subclass(proc1,proc2) vale,
allora per ogni inst2 vale: se inst2 é un' istanza di proc2, allora esiste proc1 inst1 tale che inst1 causas inst2

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

se obj1 é un esatta copia di obj2,
allora per ogni attr vale: se attr is an attribute of obj1, allora attr is an attribute of obj2

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

se obj é localizzato in region,
allora per ogni subobj vale: se subobj é una parte di obj, allora subobj é localizzato in region

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

se person possiedees obj,
allora esiste type tale che type ha il diritto di compiere person e per ogni process vale: se process é un' istanza di type, allora obj é un paziente di process

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

Se proc1 inibisce proc2, allora per ogni time,place vale: ""esiste proc1 inst1 tale che inst1 é localizzato in place" vales durante time" decreases likelihood of ""esiste proc2 inst2 tale che inst2 é localizzato in place" vales durante 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)))))))

se proc1 impedisce l'occorrenza di proc2,
allora per ogni time,place vale: se "esiste proc1 inst1 tale che inst1 é localizzato in place" vales durante time, allora "esiste proc2 inst2 tale che inst2 é localizzato in place" non vale durante 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))))))))

class1 sussume il contenuto di class2 se e solo se per ogni obj2,info vale: se obj2 é un' istanza di class2 e obj2 contienes informazione info, allora esiste class1 obj1 tale che obj1 contienes informazione info.

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

obj1 sussume il contenuto di obj2 se e solo se per ogni info vale: se obj2 contienes informazione info, allora obj1 contienes informazione info.

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

se prop1 é una sottoproposizione prop2,
allora per ogni obj1,obj2 vale: se obj1 contienes informazione prop1 e obj2 contienes informazione prop2, allora obj2 sussume il contenuto di obj1

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

se "il massimo comune divisore di" is uguale a number,
allora per ogni element vale: se element é un é membro di "(", allora "element mod number" is uguale a

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

se "il massimo comune divisore di" is uguale a number,
allora non esiste greater tale che greater é più grande di number e per ogni element vale: se element é un é membro di "(", allora "element mod greater" is uguale a

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

se "il minimo comune multiplo di " is uguale a number,
allora per ogni element vale: se element é un é membro di "(", allora "number mod element" is uguale a

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

se "il minimo comune multiplo di " is uguale a number,
allora non esiste less tale che less é meno dinumber e per ogni element vale: se element é un é membro di "(", allora "less mod element" is uguale a

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

se prime é un' istanza di NumeroPrimo,
allora per ogni number vale: se "prime mod number" is uguale a , allora number is uguale a o number is uguale a prime

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

se id é un elemento di identitá di function,
allora per ogni inst vale: se il numero argomenti di function é un istanza di class e inst é un' istanza di class, allora "function(id,inst" is uguale a inst

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

se subset é un sottoinsieme di set,
allora per ogni element vale: se ?é un elemento di subset, allora ?é un elemento di set

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

Se per ogni element vale: ?é un elemento di set1 se e solo se ?é un elemento di set2, allora set1 is uguale a set2.

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

se superclass é un' istanza di ClasseDisgiuntaACoppie,
allora per ogni class1,class2 vale: se class1 é un' istanza di superclass e class2 é un' istanza di superclass, allora class1 is uguale a class2 o class1 é disgiunto da class2

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

se class é un' istanza di ClasseMutualmenteDisgiunta,
allora per ogni inst1,inst2 vale: se inst1 é un' istanza di class e inst2 é un' istanza di inst1, allora esiste class inst3 tale che inst2 é not un' istanza di inst3

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

se
- "il valore di path" is uguale a sum
- subpath é un sottografo di path
- arc1 é una parte di path
- il valore diarc1 énumber1
- per ogni arc2 vale: se arc2 é una parte di path, allora arc2 é una parte di subpath o arc2 is uguale a arc1
,
allora sum is uguale a "("il valore di 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)))

se
- "il valore di path" is uguale a sum
- arc1 é una parte di path
- arc2 é una parte di path
- il valore diarc1 énumber1
- il valore diarc2 énumber2
- per ogni arc3 vale: se arc3 é una parte di path, allora arc3 is uguale a arc1 o arc3 is uguale a arc2
,
allora "il valore di path" is uguale a "(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)))

se "il cammino col minor costo tra node1 e node2" is uguale a path e "il valore di path" is uguale a number,
allora per ogni path2 vale: se path2 é un' istanza di "l' insieme di cammini tra node1 e node2" e "il valore di path2" is uguale a number2, allora number2 é più grande di o uguale a 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))))

se "il il cammino col costo maggiore tra node1 e node2" is uguale a path e "il valore di path" is uguale a number,
allora per ogni path2 vale: se path2 é un' istanza di "l' insieme di cammini tra node1 e node2" e "il valore di path2" is uguale a number2, allora number2 é minore o uguale a 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))))

se "l' insieme di cammini minimi che partiziona graphin due separati grafi" is uguale a pathclass,
allora esiste number tale che per ogni path vale: se path é un' istanza di pathclass, allora la lunghezza di path é number

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

se rel é un' istanza di RelazioneEstesaAQuantitá e rel é un' istanza di RelazioneTernaria e number1 é un' istanza di NumeroReale e number2 é un' istanza di NumeroReale e rel(number1,number2,value vales,
allora per ogni unit vale: se unit é un' istanza di UnitáDiMisura, allora rel("number1 unit(s","number2 unit(s","value unit(s" vales

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

se rel é un' istanza di RelazioneEstesaAQuantitá e rel é un' istanza di RelazioneBinaria e number1 é un' istanza di NumeroReale e number2 é un' istanza di NumeroReale e rel(number1,number2 vales,
allora per ogni unit vale: se unit é un' istanza di UnitáDiMisura, allora rel("number1 unit(s","number2 unit(s" vales

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

se obj1 é più largo diobj2,
allora per ogni quant1,quant2 vale: se lamisura obj1 é "quant1 MisuraDiLunghezza(s" e lamisura obj2 é "quant2 MisuraDiLunghezza(s", allora quant1 é più grande di quant2

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

se proc ricorre ogni time1,
allora per ogni time2 vale: se durata di time2 é time1, allora esiste position tale che position é una parte ditime2 e "esiste inst tale che inst é un' istanza di proc" vales durante position

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

se "l' inizio di interval" is uguale a point,
allora per ogni otherpoint vale: se otherpoint é una parte diinterval e otherpoint is not uguale a point, allora point succede?{s} prima di otherpoint

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

se "la fine di interval" is uguale a point,
allora per ogni otherpoint vale: se otherpoint é una parte diinterval e otherpoint is not uguale a point, allora otherpoint succede?{s} prima di point

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

se obj é un' istanza di Oggetto,
allora esiste PuntoTemporale time1,PuntoTemporale time2 tale che time1 succede?{s} prima di time2 e per ogni time vale: se time1 succede?{s} prima di o con time e time succede?{s} prima di o con time2, allora obj esistes durante 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))))))

se obj é un risultato di proc,
allora per ogni time vale: se time succede?{s} prima di "l' inizio di "il tempo di esistenza di proc"", allora obj non esiste durante time

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

Se "intervallo tra point1 e point2" is uguale a interval, allora per ogni point vale: point é tra o in point1 e point2 se e solo se point é una parte diinterval.

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

se "decomposizione di interval in ? interval-types" is uguale a class,
allora per ogni time1,time2 vale: se time1 é un' istanza di interval-type e time2 é un' istanza di class, allora esiste duration tale che durata di time1 é duration e durata di time2 é 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))))))

se "decomposizione di interval in ? interval-types" is uguale a class,
allora per ogni time1,time2 vale: se time1 é un' istanza di class e time2 é un' istanza di class e time1 is not uguale a time2, allora time1 incontras time2 o time2 incontras time1 o time1 accades prima di time2 o time2 accades prima di 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)))))

se "decomposizione di interval in ? interval-types" is uguale a class,
allora per ogni time1 vale: se time1 é un' istanza di class e time1 non finisce interval, allora esiste class time2 tale che time1 incontras 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))))))

se "decomposizione di interval in ? interval-types" is uguale a class,
allora per ogni time1 vale: se time1 é un' istanza di class e time1 non inizia interval, allora esiste class time2 tale che time2 incontras 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))))))

se "decomposizione di interval in ? interval-types" is uguale a class,
allora per ogni time vale: se time é un' istanza di PuntoTemporale e time é una parte diinterval, allora esiste class instance tale che time é una parte diinstance

(=>
      (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 é un' istanza di OggettoIntegro se e solo se per ogni part1,part2 vale: se obj is uguale a "l' unione delle parti di part1 e part2", allora part1 é connesso a part2.

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

se obj1 é una superficie di obj2,
allora per ogni obj3 vale: se obj3 é una parte superficiale di obj2, allora obj3 é una parte di obj1

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

se obj1 é una parte interiore di obj2,
allora per ogni part vale: se part é una parte superficiale di obj2, allora obj1 non si sovrappone a part

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

Se obj3 is uguale a "l' unione delle parti di obj1 e obj2", allora per ogni part vale: part é una parte di obj3 se e solo se part é una parte di obj1 o part é una parte di obj2.

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

Se obj3 is uguale a "l' intersezione delle parti di obj1 e obj2", allora per ogni part vale: part é una parte di obj3 se e solo se part é una parte di obj1 e part é una parte di obj2.

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

Se obj3 is uguale a "la differenza tra le parti di obj1 e obj2", allora per ogni part vale: part é una parte di obj3 se e solo se part é una parte di obj1 e part é not una parte di obj2.

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

se hole1 é un' apertura in obj e hole2 é un' apertura in obj,
allora per ogni hole3 vale: se hole3 é una parte di "l' unione delle parti di hole1 e hole2", allora hole3 é un' apertura in obj

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

Se obj1 is uguale a " ció che entra nell'apertura hole", allora per ogni obj2 vale: obj2 si sovrappones a obj1 se e solo se esiste obj3 tale che hole é un' apertura in obj3 e obj2 si sovrappones a obj3.

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

se obj1 riempie completamentes hole,
allora per ogni obj2 vale: se obj2 é connesso a hole, allora obj2 é connesso a obj1

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

Se obj1 is uguale a "la superficie dell'apertura hole", allora per ogni obj2 vale: obj2 si sovrappones a obj1 se e solo se esiste obj3 tale che obj3 é una parte superficiale di " ció che entra nell'apertura hole" e hole incontras obj3 e obj2 si sovrappones a obj3.

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

se subproc é un sottoprocesso di proc,
allora per ogni region vale: se proc é localizzato in region, allora subproc é localizzato in region

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

se
- path1 é cammino mentre process si verifica
- process si originas in source
- process fines in dest
- la lunghezza di path1 é measure1
- non esiste path2,measure2 tale che path2 é cammino mentre process si verifica e process si originas in origin e process fines in dest e la lunghezza di path2 é measure2 e measure2 é meno dimeasure1
,
allora per ogni obj vale: se obj é una parte di path1, allora obj is between source and 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))))

se keep é un' istanza di Trattenere e obj é un paziente di keep,
allora esiste place tale che per ogni time vale: se time é una parte di"il tempo di esistenza di keep", allora "obj é localizzato in place" vales durante time

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

se cooperate é un' istanza di Cooperazione,
allora esiste purp tale che per ogni agent vale: se cooperate é un agente di agent, allora cooperate ha &n scopo purp per agent

(=>
      (instance ?COOPERATE Cooperation)
      (exists
            (?PURP)
            (forall
                  (?AGENT)
                  (=>
                        (agent ?COOPERATE ?AGENT)
                        (hasPurposeForAgent ?COOPERATE ?PURP ?AGENT)))))

se war é un' istanza di Guerra e war é un agente di agent,
allora
- agent é un' istanza di Nazione
- - agent é un' istanza di Organizzazione
  - per ogni member vale: se member é un membro di agent, allora member é un' istanza di Nazione

(=>
      (and
            (instance ?WAR War)
            (agent ?WAR ?AGENT))
      (or
            (instance ?AGENT Nation)
            (and
                  (instance ?AGENT Organization)
                  (forall
                        (?MEMBER)
                        (=>
                              (member ?MEMBER ?AGENT)
                              (instance ?MEMBER Nation))))))

se bacterium é un' istanza di Bacterio,
allora esiste Cellula cell1 tale che cell1 é un componente dibacterium e per ogni cell2 vale: se cell2 é un componente dibacterium e cell2 é un' istanza di Cellula, allora cell1 is uguale a 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))))))

se virus é un' istanza di Virus,
allora esiste Molecola mol1 tale che mol1 é un componente divirus e per ogni mol2 vale: se mol2 é un componente divirus e mol2 é un' istanza di Molecola, allora mol1 is uguale a 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))))))

se food é un' istanza di Cibo,
allora per ogni part1 vale: se part1 é una parte di food, allora esiste part2,Animale animal tale che part1 é una parte di part2 e part2 é una parte di animal

(=>
      (instance ?FOOD Food)
      (forall
            (?PART1)
            (=>
                  (part ?PART1 ?FOOD)
                  (exists
                        (?PART2 ?ANIMAL)
                        (and
                              (part ?PART1 ?PART2)
                              (part ?PART2 ?ANIMAL)
                              (instance ?ANIMAL Animal))))))

se meat é un' istanza di Carne,
allora per ogni part vale: se part é una parte di meat, allora esiste subpart,time,animal tale che subpart é una parte di part e "animal é un' istanza di Animale e subpart é una parte di animal" vales durante 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))))))))

se veg é un' istanza di FruttaOVerdura,
allora per ogni part vale: se part é una parte di veg, allora esiste subpart,time,plant tale che subpart é una parte di part e "plant é un' istanza di Pianta e subpart é una parte di plant" vales durante 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))))))))

se artifact é un' istanza di ManufattoStatico,
allora esiste place tale che per ogni time vale: se time succede?{s} prima di o con "la fine di "il tempo di esistenza di artifact"" e "l' inizio di "il tempo di esistenza di artifact"" succede?{s} prima di o con time, allora "il luogo dove artifact era in time" is uguale a place

(=>
      (instance ?ARTIFACT StationaryArtifact)
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (and
                              (beforeOrEqual
                                    ?TIME
                                    (EndFn
                                          (WhenFn ?ARTIFACT)))
                              (beforeOrEqual
                                    (BeginFn
                                          (WhenFn ?ARTIFACT))
                                    ?TIME))
                        (equal
                              (WhereFn ?ARTIFACT ?TIME)
                              ?PLACE)))))

se machine é un' istanza di Macchinario,
allora per ogni proc vale: se machine é uno strumento per proc, allora esiste resource,result tale che resource é una risorsa per proc e result é un risultato di proc

(=>
      (instance ?MACHINE Machine)
      (forall
            (?PROC)
            (=>
                  (instrument ?PROC ?MACHINE)
                  (exists
                        (?RESOURCE ?RESULT)
                        (and
                              (resource ?PROC ?RESOURCE)
                              (result ?PROC ?RESULT))))))

se group é un' istanza di GruppoDiEtá,
allora per ogni memb1,memb2,age1,age2 vale: se memb1 é un membro di group e memb2 é un membro di group e il etá di memb1 é age1 e il etá di memb2 é age2, allora age1 is uguale a 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))))

se group é un' istanza di GruppoFamiliare,
allora per ogni memb1,memb2 vale: se memb1 é un membro di group e memb2 é un membro di group, allora memb1 e memb2 sono parenti

(=>
      (instance ?GROUP FamilyGroup)
      (forall
            (?MEMB1 ?MEMB2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP))
                  (familyRelation ?MEMB1 ?MEMB2))))

se "entitá nel processo proc si stanno muovendo verso attr1" vales durante time,
allora per ogni attr2 vale: se "entitá nel processo proc si stanno muovendo verso attr2" vales durante time, allora attr2 is uguale a attr1

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

se "proc é davanti a attr1" vales durante time,
allora per ogni attr2 vale: se "proc é davanti a attr2" vales durante time, allora attr2 is uguale a attr1

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

Per ogni org vale: org non impiega person e person é un' istanza di Umano se e solo se unemployed is an attribute of person.

(<=>
      (forall
            (?ORG)
            (and
                  (not
                        (employs ?ORG ?PERSON))
                  (instance ?PERSON Human)))
      (attribute ?PERSON Unemployed))

se monochromatic is an attribute of obj e part é una parte superficiale di obj e color is an attribute of part e color é un' istanza di ColorePirmario,
allora per ogni element vale: se element é una parte superficiale di obj, allora color is an attribute of element

(=>
      (and
            (attribute ?OBJ Monochromatic)
            (superficialPart ?PART ?OBJ)
            (attribute ?PART ?COLOR)
            (instance ?COLOR PrimaryColor))
      (forall
            (?ELEMENT)
            (=>
                  (superficialPart ?ELEMENT ?OBJ)
                  (attribute ?ELEMENT ?COLOR))))

se wet is an attribute of obj,
allora per ogni part vale: se part é una parte di obj, allora esiste subpart tale che subpart é una parte di part e liquid is an attribute of subpart

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

entity é un' istanza di "l' intersezione di tutti gli elementi di superclass" se e solo se per ogni class vale: se class é un' istanza di superclass, allora entity é un' istanza di class.

(<=>
      (instance
            ?ENTITY
            (GeneralizedIntersectionFn ?SUPERCLASS))
      (forall
            (?CLASS)
            (=>
                  (instance ?CLASS ?SUPERCLASS)
                  (instance ?ENTITY ?CLASS))))