equal (equal)
(equal entity1 entity2) is true just in case
entity1 is identical with entity2.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
addition fn
division fn
exponentiation fn
max fn
min fn
multiplication fn
reciprocal fn
remainder fn
round fn
subtraction fn
arc weight
authors
before or equal
causes
causes subclass
citizen
closed on
connected
contains information
cooccur
copy
date
decreases likelihood
developmental form
disjoint
distributes
documentation
duration
earlier
editor
element
employs
equivalence relation on
equivalent content class
equivalent content instance
exploits
expressed in language
faces
family relation
finishes
frequency
graph part
greater than
greater than or equal to
has purpose
has skill
holds during
holds obligation
holds right
hole
identity element
in list
in scope of interest
increases likelihood
independent probability
inhabits
inhibits
initial list
instance
inverse
irreflexive on
larger
less than
less than or equal to
material
measure
meets temporally
modal attribute
overlaps temporally
parent
partial ordering on
partly located
path length
possesses
precondition
prevents
property
publishes
range
range subclass
refers
reflexive on
related internal concept
sibling
smaller
starts
sub attribute
sub collection
sub graph
sub list
sub process
sub proposition
subclass
subrelation
subsumes content class
subsumes content instance
successor attribute
successor attribute closure
temporal part
time
total ordering on
trichotomizing on
uses
valence
version
Type restrictions
equal(Entitá, Entitá)
Related WordNet synsets
- sameness
- the quality of being alike: "sameness of purpose kept them together"
- identity, identicalness, indistinguishability
- exact sameness; "they shared an identity of interests"
- equality
- the quality or state of being the same in quantity or measure or value or status
- equivalence
- essential equality and interchangeability
- equatability
- capability of being equated
- changelessness
- the property of remaining unchanged
- equivalent
- a person or thing equal to another in value or measure or force or effect or significance etc: "send two dollars or the equivalent in stamps"
- equate, correspond
- be equivalent or parallel, in mathematics
- equal, be
- be identical or equivalent to: "One dollar equals 1,000 rubles these days!"
- equal
- well matched; having the same quantity, value, or measure as another; "on equal terms"; "all men are equal before the law"
- like, equal, equivalent, same
- equal in amount or value; "like amounts"; "equivalent amounts"; "the same amount"; "gave one six blows and the other a like number"; "an equal number"; "the same number"
- same
- same in identity; "the same man I saw yesterday"; "never wore the same dress twice"; "this road is the same one we were on yesterday"; "on the same side of the street"
See more related synsets on a separate page.
Axioms (245)
Se class1 é una sottoclasse immediata di class2, allora non esiste class2 class3 tale che class1 é una sottoclasse di class3 e class2 is not uguale a class3 e class1 is not uguale a class3.
(=>
(immediateSubclass ?CLASS1 ?CLASS2)
(not
(exists
(?CLASS3)
(and
(subclass ?CLASS3 ?CLASS2)
(subclass ?CLASS1 ?CLASS3)
(not
(equal ?CLASS2 ?CLASS3))
(not
(equal ?CLASS1 ?CLASS3))))))
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))))
(=>
(equal ?OBJ1 ?OBJ2)
(=>
(and
(equal
?OBJ1
(ListOrderFn
(ListFn @ROW1)
?NUMBER))
(equal
?OBJ2
(ListOrderFn
(ListFn @ROW2)
?NUMBER))
(equal
(ListFn @ROW1)
(ListFn @ROW2)))
(<=>
(holds @ROW1)
(holds @ROW2))))
(=>
(equal ?LIST1 ?LIST2)
(=>
(and
(equal
?LIST1
(ListFn @ROW1))
(equal
?LIST2
(ListFn @ROW2)))
(forall
(?NUMBER)
(equal
(ListOrderFn
(ListFn @ROW1)
?NUMBER)
(ListOrderFn
(ListFn @ROW2)
?NUMBER)))))
Se rango di function é un'istanza di class e "function(" is uguale a value, allora value é un' istanza di class.
(=>
(and
(range ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(instance ?VALUE ?CLASS))
Se i valori resi da function sono sottoclassi diclass e "function(" is uguale a value, allora value é una sottoclasse di class.
(=>
(and
(rangeSubclass ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(subclass ?VALUE ?CLASS))
Se e ? sono disgiunti e rel1 é un é membro di "(" e rel2 é un é membro di "(" e rel1 is not uguale a rel2 e rel1( vales, allora rel2( non vale.
(=>
(and
(disjointRelation @ROW1)
(inList
?REL1
(ListFn @ROW1))
(inList
?REL2
(ListFn @ROW1))
(not
(equal ?REL1 ?REL2))
(holds ?REL1 @ROW2))
(not
(holds ?REL2 @ROW2)))
- se é opposto a ?,
- allora per ogni attr1,attr2 vale:
.
(=>
(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 rel(,inst vales e rel é un' istanza di Funzione, allora "rel(" is uguale a inst.
(=>
(and
(holds ?REL @ROW ?INST)
(instance ?REL Function))
(equal
(AssignmentFn ?REL @ROW)
?INST))
(=>
(instance ?ATOM Atom)
(forall
(?NUCLEUS1 ?NUCLEUS2)
(=>
(and
(component ?NUCLEUS1 ?ATOM)
(component ?NUCLEUS2 ?ATOM)
(instance ?NUCLEUS1 AtomicNucleus)
(instance ?NUCLEUS2 AtomicNucleus))
(equal ?NUCLEUS1 ?NUCLEUS2))))
Se mixture é un' istanza di Mistura, allora esiste SostanzaPura pure1,SostanzaPura pure2 tale che pure1 is not uguale a pure2 e pure1 é un membro di mixture e pure2 é un membro di mixture.
(=>
(instance ?MIXTURE Mixture)
(exists
(?PURE1 ?PURE2)
(and
(subclass ?PURE1 PureSubstance)
(subclass ?PURE2 PureSubstance)
(not
(equal ?PURE1 ?PURE2))
(piece ?PURE1 ?MIXTURE)
(piece ?PURE2 ?MIXTURE))))
Se obj é un' istanza di OggettoCorpuscolare, allora esiste Sostanza substance1,Sostanza substance2 tale che substance1 é fatto di obj e substance2 é fatto di obj e substance1 is not uguale a substance2.
(=>
(instance ?OBJ CorpuscularObject)
(exists
(?SUBSTANCE1 ?SUBSTANCE2)
(and
(subclass ?SUBSTANCE1 Substance)
(subclass ?SUBSTANCE2 Substance)
(material ?SUBSTANCE1 ?OBJ)
(material ?SUBSTANCE2 ?OBJ)
(not
(equal ?SUBSTANCE1 ?SUBSTANCE2)))))
Se process é un' istanza di ProcessoRelazionale, allora esiste obj1,obj2 tale che obj1 é un paziente di process e obj2 é un paziente di process e obj1 is not uguale a obj2.
(=>
(instance ?PROCESS DualObjectProcess)
(exists
(?OBJ1 ?OBJ2)
(and
(patient ?PROCESS ?OBJ1)
(patient ?PROCESS ?OBJ2)
(not
(equal ?OBJ1 ?OBJ2)))))
"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))))
"la classe corrispondente a attribute" is uguale a class se e solo se "la descrizione di class" is uguale a attribute.
(<=>
(equal
(ExtensionFn ?ATTRIBUTE)
?CLASS)
(equal
(AbstractionFn ?CLASS)
?ATTRIBUTE))
number1 é minore o uguale a number2 se e solo se number1 is uguale a number2 o number1 é meno dinumber2.
(<=>
(lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2)))
number1 é più grande di o uguale a number2 se e solo se number1 is uguale a number2 o number1 é più grande di number2.
(<=>
(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(greaterThan ?NUMBER1 ?NUMBER2)))
Se number é un' istanza di NumeroImmaginario, allora esiste NumeroReale real tale che number is uguale a "real*"la radice quadrata di "".
(=>
(instance ?NUMBER ImaginaryNumber)
(exists
(?REAL)
(and
(instance ?REAL RealNumber)
(equal
?NUMBER
(MultiplicationFn
?REAL
(SquareRootFn -1))))))
Se number é un' istanza di NumeroComplesso, allora esiste NumeroReale real1,NumeroReale real2 tale che number is uguale a "(real1+"real2*"la radice quadrata di """.
(=>
(instance ?NUMBER ComplexNumber)
(exists
(?REAL1 ?REAL2)
(and
(instance ?REAL1 RealNumber)
(instance ?REAL2 RealNumber)
(equal
?NUMBER
(AdditionFn
?REAL1
(MultiplicationFn
?REAL2
(SquareRootFn -1)))))))
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))))))
(=>
(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 formula1 aumentas la verosimiglianza di formula2 e "la probabilitá diformula2" is uguale a number1 e probabilitá di formula1 ammesso che formula2 valga é formula2, allora number2 é più grande di number1.
(=>
(and
(increasesLikelihood ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(greaterThan ?NUMBER2 ?NUMBER1))
Se formula1 decreases likelihood of formula2 e "la probabilitá diformula2" is uguale a number1 e probabilitá di formula1 ammesso che formula2 valga é formula2, allora number2 é meno dinumber1.
(=>
(and
(decreasesLikelihood ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(lessThan ?NUMBER2 ?NUMBER1))
Se probabilitá di formula1 e formula2 é indipendente e "la probabilitá diformula2" is uguale a number1 e probabilitá di formula1 ammesso che formula2 valga é formula2, allora number2 is uguale a number1.
(=>
(and
(independentProbability ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(equal ?NUMBER2 ?NUMBER1))
(=>
(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))))
list is uguale a null list se e solo se non esiste item tale che item é un é membro di list.
(<=>
(equal ?LIST NullList)
(not
(exists
(?ITEM)
(inList ?ITEM ?LIST))))
- 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))))
"lunghezza di "(,item"" is uguale a "("lunghezza di "(""+1".
(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))
""lunghezza di "(,item""th elemento di "(,item"" is uguale a item.
(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)
(=>
(valence ?REL ?NUMBER)
(forall
(@ROW)
(=>
(holds ?REL @ROW)
(equal
(ListLengthFn
(ListFn @ROW))
?NUMBER))))
Se "lunghezza di list1" is uguale a number, allora esiste list2 tale che list1 inizias list2 e "(number+1" is uguale a "lunghezza di list2" e ""(number+1"th elemento di list2" is uguale a item.
(=>
(equal
(ListLengthFn ?LIST1)
?NUMBER)
(exists
(?LIST2)
(and
(initialList ?LIST1 ?LIST2)
(equal
(SuccessorFn ?NUMBER)
(ListLengthFn ?LIST2))
(equal
(ListOrderFn
?LIST2
(SuccessorFn ?NUMBER))
?ITEM))))
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))))))
item é un é membro di list se e solo se esiste number tale che "numberth elemento di list" is uguale a item.
(<=>
(inList ?ITEM ?LIST)
(exists
(?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER)
?ITEM)))
- 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))))))))
(=>
(initialList ?LIST1 ?LIST2)
(forall
(?NUMBER1 ?NUMBER2)
(=>
(and
(equal
(ListLengthFn ?LIST1)
?NUMBER1)
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
(equal
(ListOrderFn ?LIST1 ?NUMBER2)
(ListOrderFn ?LIST2 ?NUMBER2)))))
(=>
(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 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 obj é esattamente localizzato in region, allora non esiste otherobj tale che otherobj é esattamente localizzato in region e otherobj is not uguale a obj.
(=>
(exactlyLocated ?OBJ ?REGION)
(not
(exists
(?OTHEROBJ)
(and
(exactlyLocated ?OTHEROBJ ?REGION)
(not
(equal ?OTHEROBJ ?OBJ))))))
"il luogo dove thing era in time" is uguale a region se e solo se "thing é esattamente localizzato in region" vales durante time.
(<=>
(equal
(WhereFn ?THING ?TIME)
?REGION)
(holdsDuring
?TIME
(exactlyLocated ?THING ?REGION)))
Se time é un' istanza di PosizioneTemporale e "agent1 possiedees obj" vales durante time e "agent2 possiedees obj" vales durante time, allora agent1 is uguale a agent2.
(=>
(and
(instance ?TIME TimePosition)
(holdsDuring
?TIME
(possesses ?AGENT1 ?OBJ))
(holdsDuring
?TIME
(possesses ?AGENT2 ?OBJ)))
(equal ?AGENT1 ?AGENT2))
"(number+1" is uguale a "(number+".
(equal
(SuccessorFn ?NUMBER)
(AdditionFn ?NUMBER 1))
"(number+2" is uguale a "(number-".
(equal
(PredecessorFn ?NUMBER)
(SubtractionFn ?NUMBER 1))
Se number é un' istanza di NumeroRazionale, allora esiste NumeroIntero int1,NumeroIntero int2 tale che number is uguale a "int1/int2".
(=>
(instance ?NUMBER RationalNumber)
(exists
(?INT1 ?INT2)
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer)
(equal
?NUMBER
(DivisionFn ?INT1 ?INT2)))))
"ilvalore assoluto dinumber1" is uguale a number2 e number1 é un' istanza di NumeroReale e number2 é un' istanza di NumeroReale se e solo se
(<=>
(and
(equal
(AbsoluteValueFn ?NUMBER1)
?NUMBER2)
(instance ?NUMBER1 RealNumber)
(instance ?NUMBER2 RealNumber))
(or
(and
(instance ?NUMBER1 NonnegativeRealNumber)
(equal ?NUMBER1 ?NUMBER2))
(and
(instance ?NUMBER1 NegativeRealNumber)
(equal
?NUMBER2
(SubtractionFn 0 ?NUMBER1)))))
Se "il tetto di number" is uguale a int, allora non esiste NumeroIntero otherint tale che otherint é più grande di o uguale a number e otherint é meno diint.
(=>
(equal
(CeilingFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(greaterThanOrEqualTo ?OTHERINT ?NUMBER)
(lessThan ?OTHERINT ?INT)))))
Se "the il maggior numero intero minore o uguale a number" is uguale a int, allora non esiste NumeroIntero otherint tale che otherint é minore o uguale a number e otherint é più grande di int.
(=>
(equal
(FloorFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(lessThanOrEqualTo ?OTHERINT ?NUMBER)
(greaterThan ?OTHERINT ?INT)))))
- 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 number é un' istanza di NumeroComplesso, allora esiste part1,part2 tale che part1 is uguale a "la parte reale di number" e part2 is uguale a "la parte immaginaria di number".
(=>
(instance ?NUMBER ComplexNumber)
(exists
(?PART1 ?PART2)
(and
(equal
?PART1
(RealNumberFn ?NUMBER))
(equal
?PART2
(ImaginaryPartFn ?NUMBER)))))
- 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 "il maggiore di number1 e number2" is uguale a number, allora - number is uguale a number1 e number1 é più grande di number2
o - number is uguale a number2 e number2 é più grande di number1
o - number is uguale a number1 e number is uguale a number2
.
(=>
(equal
(MaxFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(or
(and
(equal ?NUMBER ?NUMBER1)
(greaterThan ?NUMBER1 ?NUMBER2))
(and
(equal ?NUMBER ?NUMBER2)
(greaterThan ?NUMBER2 ?NUMBER1))
(and
(equal ?NUMBER ?NUMBER1)
(equal ?NUMBER ?NUMBER2))))
Se "il minore di number1 e number2" is uguale a number, allora - number is uguale a number1 e number1 é meno dinumber2
o - number is uguale a number2 e number2 é meno dinumber1
o - number is uguale a number1 e number is uguale a number2
.
(=>
(equal
(MinFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(or
(and
(equal ?NUMBER ?NUMBER1)
(lessThan ?NUMBER1 ?NUMBER2))
(and
(equal ?NUMBER ?NUMBER2)
(lessThan ?NUMBER2 ?NUMBER1))
(and
(equal ?NUMBER ?NUMBER1)
(equal ?NUMBER ?NUMBER2))))
Se number é un' istanza di Quantitá, allora "il reciproco di number" is uguale a "number elevato a potenza ".
(=>
(instance ?NUMBER Quantity)
(equal
(ReciprocalFn ?NUMBER)
(ExponentiationFn ?NUMBER -1)))
Se number é un' istanza di Quantitá, allora is uguale a "number*"il reciproco di number"".
(=>
(instance ?NUMBER Quantity)
(equal
1
(MultiplicationFn
?NUMBER
(ReciprocalFn ?NUMBER))))
"number1 mod number2" is uguale a number se e solo se "(""the il maggior numero intero minore o uguale a "number1/number2""*number2"+number" is uguale a number1.
(<=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2))
?NUMBER2)
?NUMBER)
?NUMBER1))
Se "number1 mod number2" is uguale a number, allora "il segno di number2" is uguale a "il segno di number".
(=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(SignumFn ?NUMBER2)
(SignumFn ?NUMBER)))
Se number é un' istanza di NumeroInteroPari, allora "number mod " is uguale a .
(=>
(instance ?NUMBER EvenInteger)
(equal
(RemainderFn ?NUMBER 2)
0))
Se number é un' istanza di NumeroInteroDispari, allora "number mod " is uguale a .
(=>
(instance ?NUMBER OddInteger)
(equal
(RemainderFn ?NUMBER 2)
1))
(=>
(instance ?PRIME PrimeNumber)
(forall
(?NUMBER)
(=>
(equal
(RemainderFn ?PRIME ?NUMBER)
0)
(or
(equal ?NUMBER 1)
(equal ?NUMBER ?PRIME)))))
- se "number1 arrotondato" is uguale a number2,
- allora
- se "(number1-"the il maggior numero intero minore o uguale a number1"" é meno di, allora number2 is uguale a "the il maggior numero intero minore o uguale a number1"
o - se "(number1-"the il maggior numero intero minore o uguale a number1"" é più grande di o uguale a , allora number2 is uguale a "il tetto di number1"
.
(=>
(equal
(RoundFn ?NUMBER1)
?NUMBER2)
(or
(=>
(lessThan
(SubtractionFn
?NUMBER1
(FloorFn ?NUMBER1))
0.5)
(equal
?NUMBER2
(FloorFn ?NUMBER1)))
(=>
(greaterThanOrEqualTo
(SubtractionFn
?NUMBER1
(FloorFn ?NUMBER1))
0.5)
(equal
?NUMBER2
(CeilingFn ?NUMBER1)))))
Se number é un' istanza di NumeroRealeNonNegativo, allora "il segno di number" is uguale a o "il segno di number" is uguale a .
(=>
(instance ?NUMBER NonnegativeRealNumber)
(or
(equal
(SignumFn ?NUMBER)
1)
(equal
(SignumFn ?NUMBER)
0)))
Se number é un' istanza di NumeroRealePositivo, allora "il segno di number" is uguale a .
(=>
(instance ?NUMBER PositiveRealNumber)
(equal
(SignumFn ?NUMBER)
1))
Se number é un' istanza di NumeroRealeNegativo, allora "il segno di number" is uguale a .
(=>
(instance ?NUMBER NegativeRealNumber)
(equal
(SignumFn ?NUMBER)
-1))
Se "la radice quadrata di number1" is uguale a number2, allora "number2*number2" is uguale a number1.
(=>
(equal
(SquareRootFn ?NUMBER1)
?NUMBER2)
(equal
(MultiplicationFn ?NUMBER2 ?NUMBER2)
?NUMBER1))
Se degree é un' istanza di MisuraDiAngoloPiano, allora "la tangente di degree" is uguale a ""il seno di degree"/"il coseno di degree"".
(=>
(instance ?DEGREE PlaneAngleMeasure)
(equal
(TangentFn ?DEGREE)
(DivisionFn
(SineFn ?DEGREE)
(CosineFn ?DEGREE))))
- 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 "(int1+1" is uguale a "(int2+1", allora int1 is uguale a int2.
(=>
(equal
(SuccessorFn ?INT1)
(SuccessorFn ?INT2))
(equal ?INT1 ?INT2))
Se int é un' istanza di NumeroIntero, allora int is uguale a "("(int+2"+1".
(=>
(instance ?INT Integer)
(equal
?INT
(SuccessorFn
(PredecessorFn ?INT))))
Se int é un' istanza di NumeroIntero, allora int is uguale a "("(int+1"+2".
(=>
(instance ?INT Integer)
(equal
?INT
(PredecessorFn
(SuccessorFn ?INT))))
Se "(int1+2" is uguale a "(int2+2", allora int1 is uguale a int2.
(=>
(equal
(PredecessorFn ?INT1)
(PredecessorFn ?INT2))
(equal ?INT1 ?INT2))
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 set é un' istanza di InsiemeFinito, allora esiste NumeroInteroNonNegativo number tale che number is uguale a "il numero di istanzia in set".
(=>
(instance ?SET FiniteSet)
(exists
(?NUMBER)
(and
(instance ?NUMBER NonnegativeInteger)
(equal
?NUMBER
(CardinalityFn ?SET)))))
(=>
(instance ?SUPERCLASS PairwiseDisjointClass)
(forall
(?CLASS1 ?CLASS2)
(=>
(and
(instance ?CLASS1 ?SUPERCLASS)
(instance ?CLASS2 ?SUPERCLASS))
(or
(equal ?CLASS1 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2)))))
Se graph é un' istanza di Grafo e node1 é un' istanza di NodoDelGrafo e node2 é un' istanza di NodoDelGrafo e node1 é una parte di graph e node2 é una parte di graph e node1 is not uguale a node2, allora esiste arc,path tale che - arc legas node1 e node2
o .
(=>
(and
(instance ?GRAPH Graph)
(instance ?NODE1 GraphNode)
(instance ?NODE2 GraphNode)
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(not
(equal ?NODE1 ?NODE2)))
(exists
(?ARC ?PATH)
(or
(links ?NODE1 ?NODE2 ?ARC)
(and
(subGraph ?PATH ?GRAPH)
(instance ?PATH GraphPath)
(or
(and
(equal
(BeginNodeFn ?PATH)
?NODE1)
(equal
(EndNodeFn ?PATH)
?NODE2))
(and
(equal
(BeginNodeFn ?PATH)
?NODE2)
(equal
(EndNodeFn ?PATH)
?NODE1)))))))
Se graph é un' istanza di Grafo, allora esiste node1,node2,node3,arc1,arc2 tale che node1 é una parte di graph e node2 é una parte di graph e node3 é una parte di graph e arc1 é una parte di graph e arc2 é una parte di graph e node2 legas arc1 e node1 e node3 legas arc2 e node2 e node1 is not uguale a node2 e node2 is not uguale a node3 e node1 is not uguale a node3 e arc1 is not uguale a arc2.
(=>
(instance ?GRAPH Graph)
(exists
(?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
(and
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(graphPart ?NODE3 ?GRAPH)
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(links ?ARC1 ?NODE1 ?NODE2)
(links ?ARC2 ?NODE2 ?NODE3)
(not
(equal ?NODE1 ?NODE2))
(not
(equal ?NODE2 ?NODE3))
(not
(equal ?NODE1 ?NODE3))
(not
(equal ?ARC1 ?ARC2)))))
Se graph é un' istanza di GrafoDiretto e arc é un' istanza di ArcoDelGrafo e arc é una parte di graph, allora esiste node1,node2 tale che "il nodo iniziale di arc" is uguale a node1 e "il nodo terminale di arc" is uguale a node2.
(=>
(and
(instance ?GRAPH DirectedGraph)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(exists
(?NODE1 ?NODE2)
(and
(equal
(InitialNodeFn ?ARC)
?NODE1)
(equal
(TerminalNodeFn ?ARC)
?NODE2))))
(=>
(and
(instance ?GRAPH GraphPath)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(=>
(equal
(InitialNodeFn ?ARC)
?NODE)
(not
(exists
(?OTHER)
(and
(equal
(InitialNodeFn ?OTHER)
?NODE)
(not
(equal ?OTHER ?ARC)))))))
(=>
(and
(instance ?GRAPH GraphPath)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(=>
(equal
(TerminalNodeFn ?ARC)
?NODE)
(not
(exists
(?OTHER)
(and
(equal
(TerminalNodeFn ?OTHER)
?NODE)
(not
(equal ?OTHER ?ARC)))))))
graph é un' istanza di CircuitoDelGrafo se e solo se esiste node tale che "l' inizio di graph" is uguale a node e "la fine di graph" is uguale a node.
(<=>
(instance ?GRAPH GraphCircuit)
(exists
(?NODE)
(and
(equal
(BeginNodeFn ?GRAPH)
?NODE)
(equal
(EndNodeFn ?GRAPH)
?NODE))))
graph é un' istanza di MultiGrafo se e solo se esiste arc1,arc2,node1,node2 tale che arc1 é una parte di graph e arc2 é una parte di graph e node1 é una parte di graph e node2 é una parte di graph e arc1 legas node1 e node2 e arc2 legas node1 e node2 e arc1 is not uguale a arc2.
(<=>
(instance ?GRAPH MultiGraph)
(exists
(?ARC1 ?ARC2 ?NODE1 ?NODE2)
(and
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(links ?NODE1 ?NODE2 ?ARC1)
(links ?NODE1 ?NODE2 ?ARC2)
(not
(equal ?ARC1 ?ARC2)))))
Se "il nodo iniziale di arc" is uguale a node e "il nodo terminale di arc" is uguale a node, allora arc é un' istanza di GrafoCiclico.
(=>
(and
(equal
(InitialNodeFn ?ARC)
?NODE)
(equal
(TerminalNodeFn ?ARC)
?NODE))
(instance ?ARC GraphLoop))
- se ,
- 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 ,
- 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, allora path é un' istanza di "l' insieme di cammini tra node1 e node2".
(=>
(equal
(MinimalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(instance
?PATH
(GraphPathFn ?NODE1 ?NODE2)))
- 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, allora path é un' istanza di "l' insieme di cammini tra node1 e node2".
(=>
(equal
(MaximalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(instance
?PATH
(GraphPathFn ?NODE1 ?NODE2)))
- 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 path é una parte di graph e graph é not un' istanza di GrafoDiretto, allora "l' insieme di cammini tra node1 e node2" is uguale a path se e solo se "l' insieme di cammini tra node2 e node1" is uguale a path.
(=>
(and
(graphPart ?PATH ?GRAPH)
(not
(instance ?GRAPH DirectedGraph)))
(<=>
(equal
(GraphPathFn ?NODE1 ?NODE2)
?PATH)
(equal
(GraphPathFn ?NODE2 ?NODE1)
?PATH)))
- 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 "number unit(s" is uguale a quant e unit é una sottoclasse di quanttype, allora quant é un' istanza di quanttype.
(=>
(and
(equal
(MeasureFn ?NUMBER ?UNIT)
?QUANT)
(subclass ?UNIT ?QUANTTYPE))
(instance ?QUANT ?QUANTTYPE))
Se unit é un' istanza di UnitáDiMisura, allora "1 mille units" is uguale a " unit(s".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(KiloFn ?UNIT)
(MeasureFn 1000 ?UNIT)))
Se unit é un' istanza di UnitáDiMisura, allora "1 milione units" is uguale a " unit(s".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MegaFn ?UNIT)
(MeasureFn 1000000 ?UNIT)))
Se unit é un' istanza di UnitáDiMisura, allora "1 miliardo units " is uguale a " unit(s".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(GigaFn ?UNIT)
(MeasureFn 1000000000 ?UNIT)))
Se unit é un' istanza di UnitáDiMisura, allora "1 trilione units" is uguale a " unit(s".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(TeraFn ?UNIT)
(MeasureFn 1000000000000 ?UNIT)))
Se unit é un' istanza di UnitáDiMisura, allora "unmillesimo di un unit" is uguale a " unit(s".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MilliFn ?UNIT)
(MeasureFn 0.001 ?UNIT)))
Se unit é un' istanza di UnitáDiMisura, allora "un milionesimo di unit" is uguale a " unit(s".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MicroFn ?UNIT)
(MeasureFn 0.000001 ?UNIT)))
Se unit é un' istanza di UnitáDiMisura, allora "un miliardesimo di un unit" is uguale a " unit(s".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(NanoFn ?UNIT)
(MeasureFn 0.000000001 ?UNIT)))
Se unit é un' istanza di UnitáDiMisura, allora "un trilionesimo di un unit" is uguale a " unit(s".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(PicoFn ?UNIT)
(MeasureFn 0.000000000001 ?UNIT)))
Se number é un' istanza di NumeroReale e unit é un' istanza di UnitáDiMisura, allora "la magnitudine di "number unit(s"" is uguale a number.
(=>
(and
(instance ?NUMBER RealNumber)
(instance ?UNIT UnitOfMeasure))
(equal
(MagnitudeFn
(MeasureFn ?NUMBER ?UNIT))
?NUMBER))
Se number é un' istanza di NumeroReale, allora "number centimeter(s" is uguale a ""number*" meter(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Centimeter)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
Meter)))
Se number é un' istanza di NumeroReale, allora "number celsius degree(s" is uguale a ""(number-" kelvin degree(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(SubtractionFn ?NUMBER 273.15)
KelvinDegree)))
Se number é un' istanza di NumeroReale, allora "number celsius degree(s" is uguale a """(number-"/" fahrenheit degree(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(DivisionFn
(SubtractionFn ?NUMBER 32)
1.8)
FahrenheitDegree)))
Se number é un' istanza di NumeroReale, allora "number day duration(s" is uguale a ""number*" hour duration(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER DayDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 24)
HourDuration)))
Se number é un' istanza di NumeroReale, allora "number hour duration(s" is uguale a ""number*" minute duration(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER HourDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
MinuteDuration)))
Se number é un' istanza di NumeroReale, allora "number minute duration(s" is uguale a ""number*" second duration(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MinuteDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
SecondDuration)))
Se number é un' istanza di NumeroReale, allora "number week duration(s" is uguale a ""number*" day duration(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER WeekDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 7)
DayDuration)))
Se number é un' istanza di NumeroReale, allora "number year duration(s" is uguale a ""number*" day duration(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER YearDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 365)
DayDuration)))
Se number é un' istanza di NumeroReale, allora "number amu(s" is uguale a ""number**" gram(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Amu)
(MeasureFn
(MultiplicationFn ?NUMBER 1.6605402 E-24)
Gram)))
Se number é un' istanza di NumeroReale, allora "number electron volt(s" is uguale a ""number**" joule(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER ElectronVolt)
(MeasureFn
(MultiplicationFn ?NUMBER 1.60217733 E-19)
Joule)))
Se number é un' istanza di NumeroReale, allora "number angstrom(s" is uguale a ""number**" meter(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Angstrom)
(MeasureFn
(MultiplicationFn ?NUMBER 1.0 E-10)
Meter)))
Se number é un' istanza di NumeroReale, allora "number foot(s" is uguale a ""number*" meter(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Foot)
(MeasureFn
(MultiplicationFn ?NUMBER 0.3048)
Meter)))
Se number é un' istanza di NumeroReale, allora "number inch(s" is uguale a ""number*" meter(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Inch)
(MeasureFn
(MultiplicationFn ?NUMBER 0.0254)
Meter)))
Se number é un' istanza di NumeroReale, allora "number mile(s" is uguale a ""number*" meter(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Mile)
(MeasureFn
(MultiplicationFn ?NUMBER 1609.344)
Meter)))
Se number é un' istanza di NumeroReale, allora "number united states gallon(s" is uguale a ""number*" liter(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 3.785411784)
Liter)))
Se number é un' istanza di NumeroReale, allora "number quart(s" is uguale a ""number/" united states gallon(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Quart)
(MeasureFn
(DivisionFn ?NUMBER 4)
UnitedStatesGallon)))
Se number é un' istanza di NumeroReale, allora "number pint(s" is uguale a ""number/" quart(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Pint)
(MeasureFn
(DivisionFn ?NUMBER 2)
Quart)))
Se number é un' istanza di NumeroReale, allora "number cup(s" is uguale a ""number/" pint(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Cup)
(MeasureFn
(DivisionFn ?NUMBER 2)
Pint)))
Se number é un' istanza di NumeroReale, allora "number ounce(s" is uguale a ""number/" cup(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Ounce)
(MeasureFn
(DivisionFn ?NUMBER 8)
Cup)))
Se number é un' istanza di NumeroReale, allora "number united kingdom gallon(s" is uguale a ""number*" liter(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedKingdomGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 4.54609)
Liter)))
Se number é un' istanza di NumeroReale, allora "number pound mass(s" is uguale a ""number*" gram(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundMass)
(MeasureFn
(MultiplicationFn ?NUMBER 453.59237)
Gram)))
Se number é un' istanza di NumeroReale, allora "number slug(s" is uguale a ""number*" gram(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Slug)
(MeasureFn
(MultiplicationFn ?NUMBER 14593.90)
Gram)))
Se number é un' istanza di NumeroReale, allora "number rankine degree(s" is uguale a ""number*" kelvin degree(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER RankineDegree)
(MeasureFn
(MultiplicationFn ?NUMBER 1.8)
KelvinDegree)))
Se number é un' istanza di NumeroReale, allora "number pound force(s" is uguale a ""number*" newton(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundForce)
(MeasureFn
(MultiplicationFn ?NUMBER 4.448222)
Newton)))
Se number é un' istanza di NumeroReale, allora "number calorie(s" is uguale a ""number*" joule(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Calorie)
(MeasureFn
(MultiplicationFn ?NUMBER 4.1868)
Joule)))
Se number é un' istanza di NumeroReale, allora "number british thermal unit(s" is uguale a ""number*" joule(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER BritishThermalUnit)
(MeasureFn
(MultiplicationFn ?NUMBER 1055.05585262)
Joule)))
Se number é un' istanza di NumeroReale, allora "number angular degree(s" is uguale a ""number*"PiGreco/"" radian(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER AngularDegree)
(MeasureFn
(MultiplicationFn
?NUMBER
(DivisionFn Pi 180))
Radian)))
Se number é un' istanza di NumeroReale, allora "number united states cent(s" is uguale a ""number*" united states dollar(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
UnitedStatesDollar)))
Se number é un' istanza di NumeroReale, allora "number euro cent(s" is uguale a ""number*" euro dollar(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER EuroCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
EuroDollar)))
Se number é un' istanza di NumeroReale, allora "number byte(s" is uguale a ""number*" bit(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Byte)
(MeasureFn
(MultiplicationFn ?NUMBER 8)
Bit)))
Se number é un' istanza di NumeroReale, allora "number kilo byte(s" is uguale a ""number*" byte(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER KiloByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
Byte)))
Se number é un' istanza di NumeroReale, allora "number mega byte(s" is uguale a ""number*" kilo byte(s".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MegaByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
KiloByte)))
"valore delle appartenenze di person" is uguale a amount se e solo se valore di "appartenenze di person" é amount.
(<=>
(equal
(WealthFn ?PERSON)
?AMOUNT)
(monetaryValue
(PropertyFn ?PERSON)
?AMOUNT))
Se point é un' istanza di PuntoTemporale e point is not uguale a positive infinity, allora point succede?{s} prima di positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(before ?POINT PositiveInfinity))
Se point é un' istanza di PuntoTemporale e point is not uguale a positive infinity, allora esiste otherpoint tale che otherpoint is tra point e positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))
Se point é un' istanza di PuntoTemporale e point is not uguale a negative infinity, allora negative infinity succede?{s} prima di point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(before NegativeInfinity ?POINT))
Se point é un' istanza di PuntoTemporale e point is not uguale a negative infinity, allora esiste otherpoint tale che otherpoint is tra negative infinity e point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))
- 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))))
interval1 inizias interval2 se e solo se "l' inizio di interval1" is uguale a "l' inizio di interval2" e "la fine di interval1" succede?{s} prima di "la fine di interval2".
(<=>
(starts ?INTERVAL1 ?INTERVAL2)
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(before
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2))))
interval1 finiscees interval2 se e solo se "l' inizio di interval2" succede?{s} prima di "l' inizio di interval1" e "la fine di interval2" is uguale a "la fine di interval1".
(<=>
(finishes ?INTERVAL1 ?INTERVAL2)
(and
(before
(BeginFn ?INTERVAL2)
(BeginFn ?INTERVAL1))
(equal
(EndFn ?INTERVAL2)
(EndFn ?INTERVAL1))))
Se point1 succede?{s} prima di o con point2, allora point1 succede?{s} prima di point2 o point1 is uguale a point2.
(=>
(beforeOrEqual ?POINT1 ?POINT2)
(or
(before ?POINT1 ?POINT2)
(equal ?POINT1 ?POINT2)))
interval1 incontras interval2 se e solo se "la fine di interval1" is uguale a "l' inizio di interval2".
(<=>
(meetsTemporally ?INTERVAL1 ?INTERVAL2)
(equal
(EndFn ?INTERVAL1)
(BeginFn ?INTERVAL2)))
Se "l' inizio di interval1" is uguale a "l' inizio di interval2" e "la fine di interval1" is uguale a "la fine di interval2", allora interval1 is uguale a interval2.
(=>
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(equal
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2)))
(equal ?INTERVAL1 ?INTERVAL2))
phys1 occores nello stesso tempo di phys2 se e solo se "il tempo di esistenza di phys1" is uguale a "il tempo di esistenza di phys2".
(<=>
(cooccur ?PHYS1 ?PHYS2)
(equal
(WhenFn ?PHYS1)
(WhenFn ?PHYS2)))
Se "intervallo tra point1 e point2" is uguale a interval, allora "l' inizio di interval" is uguale a point1 e "la fine di interval" is uguale a point2.
(=>
(equal
(TimeIntervalFn ?POINT1 ?POINT2)
?INTERVAL)
(and
(equal
(BeginFn ?INTERVAL)
?POINT1)
(equal
(EndFn ?INTERVAL)
?POINT2)))
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 process é un' istanza di EntitáConcreta, allora "prima "il tempo di esistenza di process"" is uguale a "intervallo tra negative infinity e "l' inizio di "il tempo di esistenza di process""".
(=>
(instance ?PROCESS Physical)
(equal
(PastFn
(WhenFn ?PROCESS))
(TimeIntervalFn
NegativeInfinity
(BeginFn
(WhenFn ?PROCESS)))))
Se process é un' istanza di EntitáConcreta, allora "dopo "il tempo di esistenza di process"" is uguale a "intervallo tra "la fine di "il tempo di esistenza di process"" e positive infinity".
(=>
(instance ?PROCESS Physical)
(equal
(FutureFn
(WhenFn ?PROCESS))
(TimeIntervalFn
(EndFn
(WhenFn ?PROCESS))
PositiveInfinity)))
Se day1 é un' istanza di "il giorno number1" e day2 é un' istanza di "il giorno number2" e "(number2-number1" is uguale a , allora day1 incontras day2.
(=>
(and
(instance
?DAY1
(DayFn ?NUMBER1 ?MONTH))
(instance
?DAY2
(DayFn ?NUMBER2 ?MONTH))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?DAY1 ?DAY2))
Se hour1 é un' istanza di "l' ora number1" e hour2 é un' istanza di "l' ora number2" e "(number2-number1" is uguale a , allora hour1 incontras hour2.
(=>
(and
(instance
?HOUR1
(HourFn ?NUMBER1 ?DAY))
(instance
?HOUR2
(HourFn ?NUMBER2 ?DAY))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?HOUR1 ?HOUR2))
Se minute1 é un' istanza di "il minutonumber1" e minute2 é un' istanza di "il minutonumber2" e "(number2-number1" is uguale a , allora minute1 incontras minute2.
(=>
(and
(instance
?MINUTE1
(MinuteFn ?NUMBER1 ?HOUR))
(instance
?MINUTE2
(MinuteFn ?NUMBER2 ?HOUR))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?MINUTE1 ?MINUTE2))
Se second1 é un' istanza di "il secondo number1" e second2 é un' istanza di "il secondo number2" e "(number2-number1" is uguale a , allora second1 incontras second2.
(=>
(and
(instance
?SECOND1
(SecondFn ?NUMBER1 ?MINUTE))
(instance
?SECOND2
(SecondFn ?NUMBER2 ?MINUTE))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?SECOND1 ?SECOND2))
Se year1 é un' istanza di Anno e year2 é un' istanza di Anno e "(year2-year1" is uguale a , allora year1 incontras year2.
(=>
(and
(instance ?YEAR1 Year)
(instance ?YEAR2 Year)
(equal
(SubtractionFn ?YEAR2 ?YEAR1)
1))
(meetsTemporally ?YEAR1 ?YEAR2))
Se leap é un' istanza di AnnoBisestile e leap is uguale a "number Anno(s", allora
(=>
(and
(instance ?LEAP LeapYear)
(equal
?LEAP
(MeasureFn ?NUMBER Year)))
(or
(and
(equal
(RemainderFn ?NUMBER 4)
0)
(not
(equal
(RemainderFn ?NUMBER 100)
0)))
(equal
(RemainderFn ?NUMBER 400)
0)))
Se month1 is uguale a "il mese Gennaio" e month2 is uguale a "il mese Febbraio", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn January ?YEAR))
(equal
?MONTH2
(MonthFn February ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se "il mese Febbraio" is uguale a month e year é not un' istanza di AnnoBisestile, allora durata di month é " day duration(s".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(not
(instance ?YEAR LeapYear)))
(duration
?MONTH
(MeasureFn 28 DayDuration)))
Se "il mese Febbraio" is uguale a month e year é un' istanza di AnnoBisestile, allora durata di month é " day duration(s".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(instance ?YEAR LeapYear))
(duration
?MONTH
(MeasureFn 29 DayDuration)))
Se month1 is uguale a "il mese Febbraio" e month2 is uguale a "il mese Marzo", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn February ?YEAR))
(equal
?MONTH2
(MonthFn March ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Marzo" e month2 is uguale a "il mese Aprile", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn March ?YEAR))
(equal
?MONTH2
(MonthFn April ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Aprile" e month2 is uguale a "il mese Maggio", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn April ?YEAR))
(equal
?MONTH2
(MonthFn May ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Maggio" e month2 is uguale a "il mese Giugno", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn May ?YEAR))
(equal
?MONTH2
(MonthFn June ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Giugno" e month2 is uguale a "il mese Luglio", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn June ?YEAR))
(equal
?MONTH2
(MonthFn July ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Luglio" e month2 is uguale a "il mese Agosto", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn July ?YEAR))
(equal
?MONTH2
(MonthFn August ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Agosto" e month2 is uguale a "il mese Settembre", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn August ?YEAR))
(equal
?MONTH2
(MonthFn September ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Settembre" e month2 is uguale a "il mese Ottobre", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn September ?YEAR))
(equal
?MONTH2
(MonthFn October ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Ottobre" e month2 is uguale a "il mese Novembre", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn October ?YEAR))
(equal
?MONTH2
(MonthFn November ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Novembre" e month2 is uguale a "il mese Dicembre", allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn November ?YEAR))
(equal
?MONTH2
(MonthFn December ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Se month1 is uguale a "il mese Dicembre" e month2 is uguale a "il mese Gennaio" e year1 incontras year2, allora month1 incontras month2.
(=>
(and
(equal
?MONTH1
(MonthFn December ?YEAR1))
(equal
?MONTH2
(MonthFn January ?YEAR2))
(meetsTemporally ?YEAR1 ?YEAR2))
(meetsTemporally ?MONTH1 ?MONTH2))
- 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))))))
(=>
(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 esiste class time tale che time inizias interval.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(exists
(?TIME)
(and
(instance ?TIME ?CLASS)
(starts ?TIME ?INTERVAL))))
Se "decomposizione di interval in ? interval-types" is uguale a class, allora esiste class time tale che time finiscees interval.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(exists
(?TIME)
(and
(instance ?TIME ?CLASS)
(finishes ?TIME ?INTERVAL))))
- 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))))))
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME)
(=>
(and
(instance ?TIME TimePoint)
(temporalPart ?TIME ?INTERVAL))
(exists
(?INSTANCE)
(and
(instance ?INSTANCE ?CLASS)
(temporalPart ?TIME ?INSTANCE))))))
Se year é un' istanza di Anno, allora "il numero di istanzia in "decomposizione di year in ? Meses"" is uguale a .
(=>
(instance ?YEAR Year)
(equal
(CardinalityFn
(TemporalCompositionFn ?YEAR Month))
12))
Se month é un' istanza di Mese e durata di month é "number day duration(s", allora "il numero di istanzia in "decomposizione di month in ? Giornos"" is uguale a number.
(=>
(and
(instance ?MONTH Month)
(duration
?MONTH
(MeasureFn ?NUMBER DayDuration)))
(equal
(CardinalityFn
(TemporalCompositionFn ?MONTH Day))
?NUMBER))
Se week é un' istanza di Settimana, allora "il numero di istanzia in "decomposizione di week in ? Giornos"" is uguale a .
(=>
(instance ?WEEK Week)
(equal
(CardinalityFn
(TemporalCompositionFn ?WEEK Day))
7))
Se day é un' istanza di Giorno, allora "il numero di istanzia in "decomposizione di day in ? Oras"" is uguale a .
(=>
(instance ?DAY Day)
(equal
(CardinalityFn
(TemporalCompositionFn ?DAY Hour))
24))
Se hour é un' istanza di Ora, allora "il numero di istanzia in "decomposizione di hour in ? Minutos"" is uguale a .
(=>
(instance ?HOUR Hour)
(equal
(CardinalityFn
(TemporalCompositionFn ?HOUR Minute))
60))
Se minute é un' istanza di Minuto, allora "il numero di istanzia in "decomposizione di minute in ? Secondos"" is uguale a .
(=>
(instance ?MINUTE Minute)
(equal
(CardinalityFn
(TemporalCompositionFn ?MINUTE Second))
60))
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 é un membro di coll e obj2 é un membro di coll e obj1 is not uguale a obj2, allora obj1 non si sovrappone a obj2.
(=>
(and
(member ?OBJ1 ?COLL)
(member ?OBJ2 ?COLL)
(not
(equal ?OBJ1 ?OBJ2)))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
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 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 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 "il tempo di esistenza di subproc" is uguale a "il tempo di esistenza di proc" o "il tempo di esistenza di subproc" has luogodurante "il tempo di esistenza di proc".
(=>
(subProcess ?SUBPROC ?PROC)
(or
(equal
(WhenFn ?SUBPROC)
(WhenFn ?PROC))
(during
(WhenFn ?SUBPROC)
(WhenFn ?PROC))))
Se rep é un' istanza di RiproduzioneAsessuata e organism é un risultato di rep, allora non esiste parent1,parent2 tale che parent1 é un parente di organism e parent2 é un parente di organism e parent1 is not uguale a parent2.
(=>
(and
(instance ?REP AsexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?PARENT1 ?PARENT2)
(and
(parent ?ORGANISM ?PARENT1)
(parent ?ORGANISM ?PARENT2)
(not
(equal ?PARENT1 ?PARENT2))))))
Se increase é un' istanza di Aumento e obj é un paziente di increase, allora esiste unit,quant1,quant2 tale che ""obj unit(s" is uguale a quant1" vales durante "immediatamente prima di "il tempo di esistenza di increase"" e ""obj unit(s" is uguale a quant2" vales durante "immediatamente dopo "il tempo di esistenza di increase"" e quant2 é più grande di quant1.
(=>
(and
(instance ?INCREASE Increasing)
(patient ?INCREASE ?OBJ))
(exists
(?UNIT ?QUANT1 ?QUANT2)
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?INCREASE))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?INCREASE))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT2))
(greaterThan ?QUANT2 ?QUANT1))))
Se heat é un' istanza di Riscaldamento e obj é un paziente di heat, allora esiste MisuraDiTemperatura unit,quant1,quant2 tale che ""obj unit(s" is uguale a quant1" vales durante "immediatamente prima di "il tempo di esistenza di heat"" e ""obj unit(s" is uguale a quant2" vales durante "immediatamente dopo "il tempo di esistenza di heat"" e quant2 é più grande di quant1.
(=>
(and
(instance ?HEAT Heating)
(patient ?HEAT ?OBJ))
(exists
(?UNIT ?QUANT1 ?QUANT2)
(and
(instance ?UNIT TemperatureMeasure)
(holdsDuring
(ImmediatePastFn
(WhenFn ?HEAT))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?HEAT))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT2))
(greaterThan ?QUANT2 ?QUANT1))))
Se decrease é un' istanza di Diminuzione e obj é un paziente di decrease, allora esiste unit,quant1,quant2 tale che ""obj unit(s" is uguale a quant1" vales durante "immediatamente prima di "il tempo di esistenza di decrease"" e ""obj unit(s" is uguale a quant2" vales durante "immediatamente dopo "il tempo di esistenza di decrease"" e quant2 é meno diquant1.
(=>
(and
(instance ?DECREASE Decreasing)
(patient ?DECREASE ?OBJ))
(exists
(?UNIT ?QUANT1 ?QUANT2)
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?DECREASE))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?DECREASE))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT2))
(lessThan ?QUANT2 ?QUANT1))))
Se cool é un' istanza di Raffreddamento e obj é un paziente di cool, allora esiste MisuraDiTemperatura unit,quant1,quant2 tale che ""obj unit(s" is uguale a quant1" vales durante "immediatamente prima di "il tempo di esistenza di cool"" e ""obj unit(s" is uguale a quant2" vales durante "immediatamente dopo "il tempo di esistenza di cool"" e quant2 é meno diquant1.
(=>
(and
(instance ?COOL Cooling)
(patient ?COOL ?OBJ))
(exists
(?UNIT ?QUANT1 ?QUANT2)
(and
(instance ?UNIT TemperatureMeasure)
(holdsDuring
(ImmediatePastFn
(WhenFn ?COOL))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COOL))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT2))
(lessThan ?QUANT2 ?QUANT1))))
Se transfer é un' istanza di Trasferimento e transfer é un agente di agent e patient é un paziente di transfer, allora agent is not uguale a patient.
(=>
(and
(instance ?TRANSFER Transfer)
(agent ?TRANSFER ?AGENT)
(patient ?TRANSFER ?PATIENT))
(not
(equal ?AGENT ?PATIENT)))
Se sub é un' istanza di Sostituzione, allora esiste Porre put,Spostamento remove,obj1,obj2,place tale che put é un sottoprocesso di sub e remove é un sottoprocesso di sub e obj1 é un paziente di remove e remove si originas in place e obj2 é un paziente di put e put fines in place e obj1 is not uguale a obj2.
(=>
(instance ?SUB Substituting)
(exists
(?PUT ?REMOVE ?OBJ1 ?OBJ2 ?PLACE)
(and
(instance ?PUT Putting)
(instance ?REMOVE Removing)
(subProcess ?PUT ?SUB)
(subProcess ?REMOVE ?SUB)
(patient ?REMOVE ?OBJ1)
(origin ?REMOVE ?PLACE)
(patient ?PUT ?OBJ2)
(destination ?PUT ?PLACE)
(not
(equal ?OBJ1 ?OBJ2)))))
Se change é un' istanza di CambiamentodiPossesso e obj é un paziente di change e "agent1 possiedees obj" vales durante "immediatamente prima di "il tempo di esistenza di change"" e "agent2 possiedees obj" vales durante "immediatamente dopo "il tempo di esistenza di change"", allora agent1 is not uguale a agent2.
(=>
(and
(instance ?CHANGE ChangeOfPossession)
(patient ?CHANGE ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(possesses ?AGENT1 ?OBJ))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(possesses ?AGENT2 ?OBJ)))
(not
(equal ?AGENT1 ?AGENT2)))
Se trans é un' istanza di Scambio, allora esiste agent1,agent2,Dare give1,Dare give2,obj1,obj2 tale che give1 é un sottoprocesso di trans e give2 é un sottoprocesso di trans e give1 é un agente di agent1 e give2 é un agente di agent2 e obj1 é un paziente di give1 e obj2 é un paziente di give2 e give1 fines in agent2 e give2 fines in agent1 e agent1 is not uguale a agent2 e obj1 is not uguale a obj2.
(=>
(instance ?TRANS Transaction)
(exists
(?AGENT1 ?AGENT2 ?GIVE1 ?GIVE2 ?OBJ1 ?OBJ2)
(and
(instance ?GIVE1 Giving)
(instance ?GIVE2 Giving)
(subProcess ?GIVE1 ?TRANS)
(subProcess ?GIVE2 ?TRANS)
(agent ?GIVE1 ?AGENT1)
(agent ?GIVE2 ?AGENT2)
(patient ?GIVE1 ?OBJ1)
(patient ?GIVE2 ?OBJ2)
(destination ?GIVE1 ?AGENT2)
(destination ?GIVE2 ?AGENT1)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?OBJ1 ?OBJ2)))))
Se count é un' istanza di Contare e count é un agente di agent e entity é un paziente di count, allora esiste number tale che agent conosces ""il numero di istanzia in entity" is uguale a number".
(=>
(and
(instance ?COUNT Counting)
(agent ?COUNT ?AGENT)
(patient ?COUNT ?ENTITY))
(exists
(?NUMBER)
(knows
?AGENT
(equal
(CardinalityFn ?ENTITY)
?NUMBER))))
compound é un' istanza di Composto se e solo se esiste SostanzaElementare element1,SostanzaElementare element2,SintesiChimica process tale che element1 is not uguale a element2 e element1 é una risorsa per process e element2 é una risorsa per process e compound é un risultato di process.
(<=>
(instance ?COMPOUND CompoundSubstance)
(exists
(?ELEMENT1 ?ELEMENT2 ?PROCESS)
(and
(instance ?ELEMENT1 ElementalSubstance)
(instance ?ELEMENT2 ElementalSubstance)
(not
(equal ?ELEMENT1 ?ELEMENT2))
(instance ?PROCESS ChemicalSynthesis)
(resource ?PROCESS ?ELEMENT1)
(resource ?PROCESS ?ELEMENT2)
(result ?PROCESS ?COMPOUND))))
Se interaction é un' istanza di InterazioneSociale, allora esiste agent1,agent2 tale che interaction é un agente di agent1 e interaction é un agente di agent2 e agent1 is not uguale a agent2.
(=>
(instance ?INTERACTION SocialInteraction)
(exists
(?AGENT1 ?AGENT2)
(and
(agent ?INTERACTION ?AGENT1)
(agent ?INTERACTION ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2)))))
Se disseminate é un' istanza di Diffusione, allora esiste AgenteCognitivo agent1,AgenteCognitivo agent2 tale che disseminate fines in agent1 e disseminate fines in agent2 e agent1 is not uguale a agent2.
(=>
(instance ?DISSEMINATE Disseminating)
(exists
(?AGENT1 ?AGENT2)
(and
(destination ?DISSEMINATE ?AGENT1)
(instance ?AGENT1 CognitiveAgent)
(destination ?DISSEMINATE ?AGENT2)
(instance ?AGENT2 CognitiveAgent)
(not
(equal ?AGENT1 ?AGENT2)))))
Se contest é un' istanza di Competizione, allora esiste agent1,agent2,purp1,purp2 tale che contest é un agente di agent1 e contest é un agente di agent2 e contest ha &n scopo purp1 per agent1 e contest ha &n scopo purp2 per agent2 e agent1 is not uguale a agent2 e purp1 is not uguale a purp2.
(=>
(instance ?CONTEST Contest)
(exists
(?AGENT1 ?AGENT2 ?PURP1 ?PURP2)
(and
(agent ?CONTEST ?AGENT1)
(agent ?CONTEST ?AGENT2)
(hasPurposeForAgent ?CONTEST ?PURP1 ?AGENT1)
(hasPurposeForAgent ?CONTEST ?PURP2 ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?PURP1 ?PURP2)))))
Se process é un' istanza di CambiamentoDiStato e obj é un paziente di process, allora esiste part,StatoFisico state1,StatoFisico state2 tale che part é una parte di obj e state1 is not uguale a state2 e "state1 is an attribute of part" vales durante "immediatamente prima di "il tempo di esistenza di process"" e "state2 is an attribute of part" vales durante "immediatamente dopo "il tempo di esistenza di freeze"".
(=>
(and
(instance ?PROCESS StateChange)
(patient ?PROCESS ?OBJ))
(exists
(?PART ?STATE1 ?STATE2)
(and
(part ?PART ?OBJ)
(instance ?STATE1 PhysicalState)
(instance ?STATE2 PhysicalState)
(not
(equal ?STATE1 ?STATE2))
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROCESS))
(attribute ?PART ?STATE1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FREEZE))
(attribute ?PART ?STATE2)))))
Se area é un' istanza di SuperficieAcquatica, allora esiste bed,hole,Acqua water tale che " ció che entra nell'apertura hole" is uguale a bed e water riempie propriamentes hole e "l' unione delle parti di bed e water" is uguale a area.
(=>
(instance ?AREA WaterArea)
(exists
(?BED ?HOLE ?WATER)
(and
(equal
(PrincipalHostFn ?HOLE)
?BED)
(instance ?WATER Water)
(properlyFills ?WATER ?HOLE)
(equal
(MereologicalSumFn ?BED ?WATER)
?AREA))))
"il numero di istanzia in Continente" is uguale a .
(equal
(CardinalityFn Continent)
7)
(=>
(instance ?BACTERIUM Bacterium)
(exists
(?CELL1)
(and
(component ?CELL1 ?BACTERIUM)
(instance ?CELL1 Cell)
(forall
(?CELL2)
(=>
(and
(component ?CELL2 ?BACTERIUM)
(instance ?CELL2 Cell))
(equal ?CELL1 ?CELL2))))))
(=>
(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 junct é un' istanza di Giuntura, allora esiste ParteDelCorpo struct1,ParteDelCorpo struct2 tale che junct é connesso a struct1 e junct é connesso a struct2 e struct1 is not uguale a struct2.
(=>
(instance ?JUNCT BodyJunction)
(exists
(?STRUCT1 ?STRUCT2)
(and
(connected ?JUNCT ?STRUCT1)
(connected ?JUNCT ?STRUCT2)
(instance ?STRUCT1 BodyPart)
(instance ?STRUCT2 BodyPart)
(not
(equal ?STRUCT1 ?STRUCT2)))))
Se morph é un' istanza di Morfema, allora non esiste Morfema othermorph tale che othermorph é una parte di morph e othermorph is not uguale a morph.
(=>
(instance ?MORPH Morpheme)
(not
(exists
(?OTHERMORPH)
(and
(instance ?OTHERMORPH Morpheme)
(part ?OTHERMORPH ?MORPH)
(not
(equal ?OTHERMORPH ?MORPH))))))
Se phrase é un' istanza di Sintagma, allora esiste Parola part1,Parola part2 tale che part1 é una parte di phrase e part2 é una parte di phrase e part1 is not uguale a part2.
(=>
(instance ?PHRASE Phrase)
(exists
(?PART1 ?PART2)
(and
(part ?PART1 ?PHRASE)
(part ?PART2 ?PHRASE)
(instance ?PART1 Word)
(instance ?PART2 Word)
(not
(equal ?PART1 ?PART2)))))
Se "edizione int1 di text" is uguale a edition1 e "edizione int2 di text" is uguale a edition2 e int2 é più grande di int1 e pub1 é un' istanza di Editoria e pub2 é un' istanza di Editoria e edition1 é un paziente di pub1 e edition2 é un paziente di pub2 e data di pub1 é date1 e data di pub2 é date2, allora "la fine di date1" succede?{s} prima di "la fine di date2".
(=>
(and
(equal
(EditionFn ?TEXT ?INT1)
?EDITION1)
(equal
(EditionFn ?TEXT ?INT2)
?EDITION2)
(greaterThan ?INT2 ?INT1)
(instance ?PUB1 Publication)
(instance ?PUB2 Publication)
(patient ?PUB1 ?EDITION1)
(patient ?PUB2 ?EDITION2)
(date ?PUB1 ?DATE1)
(date ?PUB2 ?DATE2))
(before
(EndFn ?DATE1)
(EndFn ?DATE2)))
Se "edizione number di text1" is uguale a text2, allora text1 sussume il contenuto di text2.
(=>
(equal
(EditionFn ?TEXT1 ?NUMBER)
?TEXT2)
(subsumesContentClass ?TEXT1 ?TEXT2))
Se text é una sottoclasse di Periodico e "volume int1 nella serie text" is uguale a volume1 e "volume int2 nella serie text" is uguale a volume2 e int2 é più grande di int1 e pub1 é un' istanza di Editoria e pub2 é un' istanza di Editoria e volume1 é un paziente di pub1 e volume2 é un paziente di pub2 e data di pub1 é date1 e data di pub2 é date2, allora "la fine di date1" succede?{s} prima di "la fine di date2".
(=>
(and
(subclass ?TEXT Periodical)
(equal
(SeriesVolumeFn ?TEXT ?INT1)
?VOLUME1)
(equal
(SeriesVolumeFn ?TEXT ?INT2)
?VOLUME2)
(greaterThan ?INT2 ?INT1)
(instance ?PUB1 Publication)
(instance ?PUB2 Publication)
(patient ?PUB1 ?VOLUME1)
(patient ?PUB2 ?VOLUME2)
(date ?PUB1 ?DATE1)
(date ?PUB2 ?DATE2))
(before
(EndFn ?DATE1)
(EndFn ?DATE2)))
Se "volume number nella serie series" is uguale a volume, allora series sussume il contenuto di volume.
(=>
(equal
(SeriesVolumeFn ?SERIES ?NUMBER)
?VOLUME)
(subsumesContentClass ?SERIES ?VOLUME))
Se "il numero periodico number di periodical" is uguale a issue, allora periodical sussume il contenuto di issue.
(=>
(equal
(PeriodicalIssueFn ?PERIODICAL ?NUMBER)
?ISSUE)
(subsumesContentClass ?PERIODICAL ?ISSUE))
Se series é un' istanza di Serie, allora esiste Libro book1,Libro book2 tale che series sussume il contenuto di book1 e series sussume il contenuto di book2 e book1 is not uguale a book2.
(=>
(instance ?SERIES Series)
(exists
(?BOOK1 ?BOOK2)
(and
(instance ?BOOK1 Book)
(instance ?BOOK2 Book)
(subsumesContentInstance ?SERIES ?BOOK1)
(subsumesContentInstance ?SERIES ?BOOK2)
(not
(equal ?BOOK1 ?BOOK2)))))
Se mole é un' istanza di Molecola, allora esiste Atomo atom1,Atomo atom2 tale che atom1 é una parte di mole e atom2 é una parte di mole e atom1 is not uguale a atom2.
(=>
(instance ?MOLE Molecule)
(exists
(?ATOM1 ?ATOM2)
(and
(instance ?ATOM1 Atom)
(instance ?ATOM2 Atom)
(part ?ATOM1 ?MOLE)
(part ?ATOM2 ?MOLE)
(not
(equal ?ATOM1 ?ATOM2)))))
(=>
(instance ?ARTIFACT StationaryArtifact)
(exists
(?PLACE)
(forall
(?TIME)
(=>
(and
(beforeOrEqual
?TIME
(EndFn
(WhenFn ?ARTIFACT)))
(beforeOrEqual
(BeginFn
(WhenFn ?ARTIFACT))
?TIME))
(equal
(WhereFn ?ARTIFACT ?TIME)
?PLACE)))))
- 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 "la legittima entitá organizzativa di unit" is uguale a org e attr é un' istanza di AttributoNormativo, allora attr is an attribute of unit se e solo se attr is an attribute of org.
(=>
(and
(equal
(OrganizationFn ?UNIT)
?ORG)
(instance ?ATTR NormativeAttribute))
(<=>
(attribute ?UNIT ?ATTR)
(attribute ?ORG ?ATTR)))
Se obj1 é attr1 a obj2 e é opposto a ? e attr1 é un é membro di "(" e attr2 é un é membro di "(" e attr1 is not uguale a attr2, allora obj1 é not attr2 a obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(contraryAttribute @ROW)
(inList
?ATTR1
(ListFn @ROW))
(inList
?ATTR2
(ListFn @ROW))
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
- 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))))
Se obj1 é attr1 a obj2 e attr1 é un' istanza di AttributoDirezionale e attr2 é un' istanza di AttributoDirezionale e attr1 is not uguale a attr2, allora obj1 é not attr2 a obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(instance ?ATTR1 DirectionalAttribute)
(instance ?ATTR2 DirectionalAttribute)
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
Se "relative time fn(time1,pacific time zone)" is uguale a time2, allora time2 is uguale a "(time1+".
(=>
(equal
(RelativeTimeFn ?TIME1 PacificTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 8)))
Se "relative time fn(time1,mountain time zone)" is uguale a time2, allora time2 is uguale a "(time1+".
(=>
(equal
(RelativeTimeFn ?TIME1 MountainTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 7)))
Se "relative time fn(time1,central time zone)" is uguale a time2, allora time2 is uguale a "(time1+".
(=>
(equal
(RelativeTimeFn ?TIME1 CentralTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 6)))
Se "relative time fn(time1,eastern time zone)" is uguale a time2, allora time2 is uguale a "(time1+".
(=>
(equal
(RelativeTimeFn ?TIME1 EasternTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 5)))
Se polychromatic is an attribute of obj, allora esiste part1,part2,AttributoDiColore color1,AttributoDiColore color2 tale che part1 é una parte superficiale di obj e part2 é una parte superficiale di obj e color1 is an attribute of part1 e color2 is an attribute of part2 e color1 is not uguale a color2.
(=>
(attribute ?OBJ Polychromatic)
(exists
(?PART1 ?PART2 ?COLOR1 ?COLOR2)
(and
(superficialPart ?PART1 ?OBJ)
(superficialPart ?PART2 ?OBJ)
(attribute ?PART1 ?COLOR1)
(attribute ?PART2 ?COLOR2)
(instance ?COLOR1 ColorAttribute)
(instance ?COLOR2 ColorAttribute)
(not
(equal ?COLOR1 ?COLOR2)))))
Se class1 é un' istanza di InsiemeOClasse e class2 é un' istanza di InsiemeOClasse, allora "la differenza tra class1 e class2" is uguale a "l' unione di class1 e "il complemento di class2"".
(=>
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass))
(equal
(RelativeComplementFn ?CLASS1 ?CLASS2)
(IntersectionFn
?CLASS1
(ComplementFn ?CLASS2))))
