Browsing Interface
: Welcome guest :
log in
[
Home
| 
Graph
|  ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
HerbaceousPlant
Hindi
ItalianLanguage
JapaneseLanguage
PortugueseLanguage
SpanishLanguage
SwedishLanguage
WoodyPlant
cb
cz
de
hi
ro
sv
tg
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
AdditionFn
Sigma KEE - AdditionFn
AdditionFn
appearance as argument number 1
(
documentation
AdditionFn
ChineseLanguage
"如果 ?NUMBER1 和 ?NUMBER2 是
Number
,那么 (
AdditionFn
?NUMBER1 ?NUMBER2)就是这些数字的算术和。")
chinese_format.kif 2214-2215
(
documentation
AdditionFn
EnglishLanguage
"If ?NUMBER1 and ?NUMBER2 are
Number
s, then (
AdditionFn
?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers.")
Merge.kif 4716-4718
(
documentation
AdditionFn
JapaneseLanguage
"?NUMBER1 と ?NUMBER2 が
Number
の場合、 (
AdditionFn
?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。")
japanese_format.kif 878-879
(
domain
AdditionFn
1
RealNumber
)
Merge.kif 4712-4712
Die Zahl 1 Argument von
AdditionFn
ist ein
fall
von
RealNumber
%n{nicht}
(
domain
AdditionFn
2
RealNumber
)
Merge.kif 4713-4713
Die Zahl 2 Argument von
AdditionFn
ist ein
fall
von
RealNumber
%n{nicht}
(
identityElement
AdditionFn
0)
Merge.kif 5295-5295
0 ist ein identitaetsElement von
AdditionFn
(
instance
AdditionFn
AssociativeFunction
)
Merge.kif 4708-4708
AdditionFn
ist ein
fall
von
AssociativeFunction
%n{nicht}
(
instance
AdditionFn
BinaryFunction
)
Merge.kif 4707-4707
AdditionFn
ist ein
fall
von
BinaryFunction
%n{nicht}
(
instance
AdditionFn
CommutativeFunction
)
Merge.kif 4709-4709
AdditionFn
ist ein
fall
von
CommutativeFunction
%n{nicht}
(
instance
AdditionFn
TotalValuedRelation
)
Merge.kif 4711-4711
AdditionFn
ist ein
fall
von
TotalValuedRelation
%n{nicht}
(
range
AdditionFn
RealNumber
)
Merge.kif 4714-4714
bildbereich
von
AdditionFn
ist ein fall von
RealNumber
{nicht}
appearance as argument number 2
(
format
ChineseLanguage
AdditionFn
"(%*[+])")
chinese_format.kif 682-682
(
format
EnglishLanguage
AdditionFn
"(%*[+])")
english_format.kif 684-684
(
format
FrenchLanguage
AdditionFn
"(%*[+])")
french_format.kif 414-414
(
format
ItalianLanguage
AdditionFn
"(%*[+]")
relations-it.txt 20-20
(
format
JapaneseLanguage
AdditionFn
"(%*[+])")
japanese_format.kif 2131-2131
(
format
PortugueseLanguage
AdditionFn
"(%*[+])")
portuguese_format.kif 366-366
(
format
cz
AdditionFn
"(%*[+])")
relations-cz.txt 423-423
(
format
de
AdditionFn
"(%*[+])")
relations-de.txt 889-889
(
format
hi
AdditionFn
"(%*[+]")
relations-hindi.txt 65-65
(
format
ro
AdditionFn
"(%*[+])")
relations-ro.kif 436-436
(
format
sv
AdditionFn
"(%*[+])")
relations-sv.txt 458-458
(
format
tg
AdditionFn
"(%*[+]")
relations-cb.txt 54-54
(
termFormat
ChineseLanguage
AdditionFn
"加成")
domainEnglishFormat.kif 5418-5418
(
termFormat
ChineseLanguage
AdditionFn
"加法函数")
chinese_format.kif 683-683
(
termFormat
ChineseTraditionalLanguage
AdditionFn
"加成")
domainEnglishFormat.kif 5417-5417
(
termFormat
EnglishLanguage
AdditionFn
"addition")
domainEnglishFormat.kif 5416-5416
(
termFormat
tg
AdditionFn
"tungkulin ng pagsasama")
relations-tg.txt 57-57
antecedent
(=>
(
and
(
equal
?OUT
(
ReverseFn
?IN))
(
equal
?LEN
(
StringLengthFn
?IN))
(
greaterThan
?LEN 1)
(
greaterThan
?N 0)
(
lessThan
?N ?LEN)
(
equal
?PIVOT
(
CeilingFn
(
DivisionFn
(
SubtractionFn
?LEN 1) 2)))
(
equal
?NEW
(
AdditionFn
(
SubtractionFn
?PIVOT ?N) ?PIVOT))
(
equal
?S
(
SubstringFn
?IN ?N
(
AdditionFn
1 ?N))))
(
equal
?S
(
SubstringFn
?OUT ?NEW
(
AdditionFn
1 ?NEW))))
Media.kif 3068-3089
Wenn
SymbolicString
ist gleich
ReverseFn
** SymbolicString
%n{nicht} und
NonnegativeInteger
ist gleich
StringLengthFn
** ** SymbolicString
%n{nicht} und
** NonnegativeInteger
ist
groesserAls
1 %n{nicht} und
** NonnegativeInteger
ist
groesserAls
0 %n{nicht} und
** ** NonnegativeInteger
ist
kleinerAls
** NonnegativeInteger
%n{nicht} und
Integer
ist gleich die
oberstegrenze
von (
** NonnegativeInteger
und 1) und 2 %n{nicht} und
** ** NonnegativeInteger
EW ist gleich ((
** Integer
und
** ** NonnegativeInteger
) und
** Integer
) %n{nicht} und
** SymbolicString
ist gleich
SubstringFn
** ** SymbolicString
,
** ** NonnegativeInteger
and (1 und
** ** NonnegativeInteger
) %n{nicht},
dann
** ** SymbolicString
ist gleich
SubstringFn
** SymbolicString
,
** ** NonnegativeInteger
EW and (1 und
** ** NonnegativeInteger
EW) %n{nicht}
(=>
(
and
(
holdsDuring
?T
(
attribute
?F
Menopausal
))
(
birthdate
?F ?B)
(
instance
?B
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y))))
(
equal
?A1
(
AdditionFn
49 ?Y))
(
equal
?A2
(
AdditionFn
52 ?Y))
(
equal
?START
(
BeginFn
?T)))
(
modalAttribute
(
and
(
greaterThan
?START ?A1)
(
greaterThan
?A2 ?START))
Likely
))
Mid-level-ontology.kif 23916-23932
Wenn
Menopausal
ist ein
attribut
von
Human
%n{nicht} haelt
waehrend
TimeInterval
%n{nicht} und
birthdate
** Human
and
Day
und
** Day
ist ein
fall
von der
tag
PositiveInteger
%n{nicht} und
RealNumber
ist gleich (49 und
Integer
) %n{nicht} und
** RealNumber
ist gleich (52 und
** Integer
) %n{nicht} und
TimePoint
ist gleich der
anfang
von
** TimeInterval
%n{nicht},
dann die Aussage
** TimePoint
ist
groesserAls
** RealNumber
%n{nicht} und
** ** RealNumber
ist
groesserAls
** TimePoint
%n{nicht} hat die modale Kraft von
Likely
(=>
(
and
(
instance
?Account
CreditAccount
)
(
accountHolder
?Account ?Agent)
(
principalAmount
?Account ?Principal)
(
agreementPeriod
?Account ?Period)
(
interestEarned
?Account ?Interest ?Period)
(
equal
?Total
(
AdditionFn
?Principal ?Interest)))
(
holdsObligation
(
KappaFn
?Payment
(
transactionAmount
?Payment ?Total)) ?Agent))
FinancialOntology.kif 1224-1233
Wenn
FinancialAccount
ist ein
fall
von
CreditAccount
%n{nicht} und
accountHolder
** FinancialAccount
and
CognitiveAgent
und
principalAmount
** FinancialAccount
and
RealNumber
und
agreementPeriod
** FinancialAccount
and
TimeInterval
und
interestEarned
** FinancialAccount
,
Interest
and
** TimeInterval
und
** RealNumber
ist gleich (
** RealNumber
und
** Interest
) %n{nicht},
dann
** CognitiveAgent
wird
gezwungen
, die Aufgabe der Art von die
kategorie
die
SymbolicString
beschreibt durchzuf�hren %n{nicht}
(=>
(
and
(
instance
?Account
Loan
)
(
borrower
?Account ?Agent)
(
principalAmount
?Account ?Principal)
(
agreementPeriod
?Account ?Period)
(
interestEarned
?Account ?Interest ?Period)
(
equal
?Total
(
AdditionFn
?Principal ?Interest)))
(
holdsObligation
(
KappaFn
?Payment
(
transactionAmount
?Payment ?Total)) ?Agent))
FinancialOntology.kif 1273-1282
Wenn
Loan
ist ein
fall
von
Loan
%n{nicht} und
borrower
** Loan
and
CognitiveAgent
und
principalAmount
** Loan
and
RealNumber
und
agreementPeriod
** Loan
and
TimeInterval
und
interestEarned
** Loan
,
Interest
and
** TimeInterval
und
** RealNumber
ist gleich (
** RealNumber
und
** Interest
) %n{nicht},
dann
** CognitiveAgent
wird
gezwungen
, die Aufgabe der Art von die
kategorie
die
SymbolicString
beschreibt durchzuf�hren %n{nicht}
(=>
(
and
(
instance
?Bond
ZeroCouponBond
)
(
maturityDate
(
AccountFn
?Bond) ?Date)
(
possesses
?BondHolder ?Bond)
(
principalAmount
(
AccountFn
?Bond)
(
MeasureFn
?Principal ?CUNIT))
(
agreementPeriod
(
AccountFn
?Bond) ?Period)
(
interestEarned
(
AccountFn
?Bond)
(
MeasureFn
?Interest ?CUNIT) ?Period)
(
equal
?Total
(
AdditionFn
?Principal ?Interest)))
(
exists
(?Payment)
(
and
(
instance
?Payment
Payment
)
(
destination
?Payment ?BondHolder)
(
origin
?Payment
(
AccountFn
?Bond))
(
transactionAmount
?Payment
(
MeasureFn
?Total ?CUNIT)))))
FinancialOntology.kif 2333-2355
Wenn
FinancialAsset
ist ein
fall
von
ZeroCouponBond
%n{nicht} und
maturityDate
AccountFn
** FinancialAsset
and
Day
und
** FinancialAsset
Holder besitzt
** FinancialAsset
%n{nicht} und
principalAmount
AccountFn
** FinancialAsset
and
RealNumber
UnitOfMeasure
(s) und
agreementPeriod
AccountFn
** FinancialAsset
and
TimeInterval
und
interestEarned
AccountFn
** FinancialAsset
,
** RealNumber
** UnitOfMeasure
(s) and
** TimeInterval
und
** RealNumber
ist gleich (
** RealNumber
und
** ** RealNumber
) %n{nicht},
dann es gibt
FinancialTransaction
um
** FinancialTransaction
ist ein
fall
von
Payment
%n{nicht} und
** FinancialTransaction
endet an
** FinancialAsset
Holder %n{nicht} und
** FinancialTransaction
beginnet an
AccountFn
** FinancialAsset
%n{nicht} und
transactionAmount
** FinancialTransaction
and
** ** RealNumber
** UnitOfMeasure
(s)
(=>
(
and
(
instance
?Deposit
Deposit
)
(
instance
?Account
FinancialAccount
)
(
destination
?Deposit
(
CurrencyFn
?Account))
(
transactionAmount
?Deposit
(
MeasureFn
?Amount ?CUNIT))
(
currentAccountBalance
?Account
(
ImmediatePastFn
(
WhenFn
?Deposit))
(
MeasureFn
?Balance1 ?CUNIT))
(
equal
?Balance2
(
AdditionFn
?Balance1 ?Amount)))
(
currentAccountBalance
?Account
(
ImmediateFutureFn
(
FutureFn
?Deposit))
(
MeasureFn
?Balance2 ?CUNIT)))
FinancialOntology.kif 436-453
Wenn
FinancialTransaction
ist ein
fall
von
Deposit
%n{nicht} und
FinancialAccount
ist ein
fall
von
FinancialAccount
%n{nicht} und
** FinancialTransaction
endet an
CurrencyFn
** FinancialAccount
%n{nicht} und
transactionAmount
** FinancialTransaction
and
RealNumber
UnitOfMeasure
(s) und
currentAccountBalance
** FinancialAccount
, direkt
vor
die
zeit
des Bestehens von
** FinancialTransaction
and
** RealNumber
** UnitOfMeasure
(s) und
** RealNumber
ist gleich (
** ** RealNumber
und
** RealNumber
) %n{nicht},
dann
currentAccountBalance
** FinancialAccount
, sofort
nach
nach
** FinancialTransaction
and
** ** RealNumber
** UnitOfMeasure
(s)
(=>
(
and
(
instance
?LIST
ConsecutiveTimeIntervalList
)
(
equal
?T1
(
ListOrderFn
?LIST ?N))
(
equal
?T2
(
ListOrderFn
?LIST
(
AdditionFn
?N 1))))
(
equal
(
BeginFn
?T2)
(
EndFn
?T1)))
Weather.kif 1935-1944
Wenn
List
ist ein
fall
von
ConsecutiveTimeIntervalList
%n{nicht} und
TimeInterval
ist gleich
entity
mitglied
von
** List
%n{nicht} und
** TimeInterval
ist gleich (
PositiveInteger
und 1)te
mitglied
von
** List
%n{nicht},
dann der
anfang
von
** ** TimeInterval
ist gleich das
ende
von
** TimeInterval
%n{nicht}
(=>
(
and
(
not
(
equal
?NUMBER2 0))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER))
Merge.kif 5117-5128
Wenn
Integer
ist gleich 0 nicht und (die
groesste
Ganzzahl kleiner als oder Gleichgestelltes zu
** Integer
und
** Integer
und
** Integer
und
** Integer
) ist gleich
** ** Integer
%n{nicht},
dann
** ** Integer
betrag
** Integer
ist gleich
** ** Integer
%n{nicht}
consequent
(<=>
(
average
?LIST1 ?AVERAGE)
(
exists
(?LIST2 ?LASTPLACE)
(
and
(
equal
(
ListLengthFn
?LIST2)
(
ListLengthFn
?LIST1))
(
equal
(
ListOrderFn
?LIST2 1)
(
ListOrderFn
?LIST1 1))
(
forall
(?ITEMFROM2)
(=>
(
inList
?ITEMFROM2 ?LIST2)
(
exists
(?POSITION ?POSITIONMINUSONE ?ITEMFROM1 ?PRIORFROM2)
(
and
(
greaterThan
?POSITION 1)
(
lessThanOrEqualTo
?POSITION
(
ListLengthFn
?LIST2))
(
equal
(
ListOrderFn
?LIST2 ?ITEMFROM2) ?POSITION)
(
inList
?ITEMFROM1 ?LIST1)
(
equal
?POSITION
(
ListOrderFn
?LIST1 ?ITEMFROM1))
(
inList
?PRIORFROM2 ?LIST2)
(
equal
?POSITIONMINUSONE
(
SubtractionFn
?POSITION 1))
(
equal
?POSITIONMINUSONE
(
ListOrderFn
?LIST2 ?PRIORFROM2))
(
equal
?ITEMFROM2
(
AdditionFn
?ITEMFROM1 ?PRIORFROM2))))))
(
equal
?LASTPLACE
(
ListLengthFn
?LIST2))
(
equal
?AVERAGE
(
DivisionFn
(
ListOrderFn
?LIST2 ?LASTPLACE) ?LASTPLACE)))))
People.kif 272-293
average
List
and
RealNumber
genau dann wenn es gibt
** List
und
PositiveInteger
um
Laenge
von
** ** List
ist gleich
Laenge
von
** List
%n{nicht} und 1te
mitglied
von
** ** List
ist gleich 1te
mitglied
von
** List
%n{nicht} und fuer alle
** PositiveInteger
wenn
** ** PositiveInteger
ist ein
Mitglied
von
** ** List
,
dann es gibt
** RealNumber
,
** ** RealNumber
MINUSONE,, ,
** PositiveInteger
, and und
** PositiveInteger
um
** ** RealNumber
ist
groesserAls
1 %n{nicht} und
** ** RealNumber
ist
kleinerAlsOderGleich
Laenge
von
** ** List
%n{nicht} und
** ** PositiveInteger
te
mitglied
von
** ** List
ist gleich
** ** RealNumber
%n{nicht} und
** ** PositiveInteger
ist ein
Mitglied
von
** List
und
** ** RealNumber
ist gleich
** ** PositiveInteger
te
mitglied
von
** List
%n{nicht} und
** ** PositiveInteger
ist ein
Mitglied
von
** ** List
und
** ** RealNumber
MINUSONE ist gleich (
** ** RealNumber
und 1) %n{nicht} und
** ** RealNumber
MINUSONE ist gleich
** ** PositiveInteger
te
mitglied
von
** ** List
%n{nicht} und
** ** PositiveInteger
ist gleich (
** ** PositiveInteger
und
** ** PositiveInteger
) %n{nicht}
und
** PositiveInteger
ist gleich
Laenge
von
** ** List
%n{nicht} und
** RealNumber
ist gleich
** PositiveInteger
te
mitglied
von
** ** List
und
** PositiveInteger
%n{nicht}
(=>
(
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)))
Merge.kif 5993-6006
Wenn der
wert
von
GraphPath
ist gleich
RealNumber
%n{nicht} und
GraphArc
ist ein
teil
von
** GraphPath
%n{nicht} und
** GraphArc
ist ein
teil
von
** GraphPath
%n{nicht} und der
wert
von
** GraphArc
ist
** RealNumber
und der
wert
von
** ** GraphArc
ist
** RealNumber
und fuer alle
GraphElement
wenn
** GraphElement
ist ein
teil
von
** GraphPath
%n{nicht},
dann
** GraphElement
ist gleich
** GraphArc
%n{nicht} oder
** GraphElement
ist gleich
** ** GraphArc
%n{nicht}
,
dann der
wert
von
** GraphPath
ist gleich (
** ** RealNumber
und
** ** RealNumber
) %n{nicht}
(=>
(
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)))
Merge.kif 5979-5991
Wenn der
wert
von
GraphPath
ist gleich
RealNumber
%n{nicht} und
** GraphPath
ist ein
teilgraph
von
** GraphPath
%n{nicht} und
GraphArc
ist ein
teil
von
** GraphPath
%n{nicht} und der
wert
von
** GraphArc
ist
** RealNumber
und fuer alle
GraphElement
wenn
** GraphElement
ist ein
teil
von
** GraphPath
%n{nicht},
dann
** GraphElement
ist ein
teil
von
** ** GraphPath
%n{nicht} oder
** GraphElement
ist gleich
** GraphArc
%n{nicht}
,
dann
** RealNumber
ist gleich (der
wert
von
** ** GraphPath
und
** ** RealNumber
) %n{nicht}
(=>
(
and
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER)
(
not
(
equal
?NUMBER2 0)))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 5104-5115
Wenn
Integer
betrag
** Integer
ist gleich
** Integer
%n{nicht} und
** ** Integer
ist gleich 0 nicht,
dann (die
groesste
Ganzzahl kleiner als oder Gleichgestelltes zu
** Integer
und
** ** Integer
und
** ** Integer
und
** ** Integer
) ist gleich
** Integer
%n{nicht}
(=>
(
and
(
equal
?A
(
ListSumFn
?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?A
(
AdditionFn
(
FirstFn
?L)
(
ListSumFn
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Merge.kif 3258-3268
Wenn
RealNumber
ist gleich
ListSumFn
List
%n{nicht} und
Laenge
von
** List
ist
groesserAls
1 %n{nicht},
dann
** RealNumber
ist gleich (
FirstFn
** List
und
ListSumFn
SubListFn
2,
Laenge
von
** List
and
** List
) %n{nicht}
(=>
(
and
(
equal
?LIST3
(
ListConcatenateFn
?LIST1 ?LIST2))
(
not
(
equal
?LIST1
NullList
))
(
not
(
equal
?LIST2
NullList
))
(
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))))
Merge.kif 3083-3102
Wenn
List
ist gleich die Liste bestanden aus
** List
und
** List
%n{nicht} und
** ** List
ist gleich
NullList
nicht und
** ** List
ist gleich
NullList
nicht und
PositiveInteger
ist
kleinerAlsOderGleich
Laenge
von
** ** List
%n{nicht} und
** PositiveInteger
ist
kleinerAlsOderGleich
Laenge
von
** ** List
%n{nicht} und
** PositiveInteger
ist ein
fall
von
PositiveInteger
%n{nicht} und
** ** PositiveInteger
ist ein
fall
von
PositiveInteger
%n{nicht},
dann
** PositiveInteger
te
mitglied
von
** List
ist gleich
** PositiveInteger
te
mitglied
von
** ** List
%n{nicht} und (
Laenge
von
** ** List
und
** ** PositiveInteger
)te
mitglied
von
** List
ist gleich
** ** PositiveInteger
te
mitglied
von
** ** List
%n{nicht}
(=>
(
and
(
equal
?OUT
(
ReverseFn
?IN))
(
equal
?LEN
(
StringLengthFn
?IN))
(
greaterThan
?LEN 1)
(
greaterThan
?N 0)
(
lessThan
?N ?LEN)
(
equal
?PIVOT
(
CeilingFn
(
DivisionFn
(
SubtractionFn
?LEN 1) 2)))
(
equal
?NEW
(
AdditionFn
(
SubtractionFn
?PIVOT ?N) ?PIVOT))
(
equal
?S
(
SubstringFn
?IN ?N
(
AdditionFn
1 ?N))))
(
equal
?S
(
SubstringFn
?OUT ?NEW
(
AdditionFn
1 ?NEW))))
Media.kif 3068-3089
Wenn
SymbolicString
ist gleich
ReverseFn
** SymbolicString
%n{nicht} und
NonnegativeInteger
ist gleich
StringLengthFn
** ** SymbolicString
%n{nicht} und
** NonnegativeInteger
ist
groesserAls
1 %n{nicht} und
** NonnegativeInteger
ist
groesserAls
0 %n{nicht} und
** ** NonnegativeInteger
ist
kleinerAls
** NonnegativeInteger
%n{nicht} und
Integer
ist gleich die
oberstegrenze
von (
** NonnegativeInteger
und 1) und 2 %n{nicht} und
** ** NonnegativeInteger
EW ist gleich ((
** Integer
und
** ** NonnegativeInteger
) und
** Integer
) %n{nicht} und
** SymbolicString
ist gleich
SubstringFn
** ** SymbolicString
,
** ** NonnegativeInteger
and (1 und
** ** NonnegativeInteger
) %n{nicht},
dann
** ** SymbolicString
ist gleich
SubstringFn
** SymbolicString
,
** ** NonnegativeInteger
EW and (1 und
** ** NonnegativeInteger
EW) %n{nicht}
(=>
(
and
(
equal
?R
(
SubListFn
?S ?E ?L))
(
greaterThan
(
SubtractionFn
?E ?S) 1))
(
equal
?R
(
ListConcatenateFn
(
ListFn
(
ListOrderFn
?L ?S))
(
SubListFn
(
AdditionFn
1 ?S) ?E ?L))))
Merge.kif 3190-3202
Wenn
List
ist gleich
SubListFn
PositiveInteger
,
Integer
and
** List
%n{nicht} und (
** Integer
und
** PositiveInteger
) ist
groesserAls
1 %n{nicht},
dann
** List
ist gleich die Liste bestanden aus (
** PositiveInteger
te
mitglied
von
** ** List
) und
SubListFn
(1 und
** PositiveInteger
),
** Integer
and
** ** List
%n{nicht}
(=>
(
and
(
equal
?VA
(
VarianceAverageFn
?M ?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?VA
(
AdditionFn
(
VarianceAverageFn
?M
(
ListOrderFn
?L 1))
(
VarianceAverageFn
?M
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Weather.kif 1453-1465
Wenn
RealNumber
ist gleich
VarianceAverageFn
Number
and
List
%n{nicht} und
Laenge
von
** List
ist
groesserAls
1 %n{nicht},
dann
** RealNumber
ist gleich (
VarianceAverageFn
** Number
and 1te
mitglied
von
** List
und
VarianceAverageFn
** Number
and
SubListFn
2,
Laenge
von
** List
and
** List
) %n{nicht}
(=>
(
and
(
instance
?M
Mixture
)
(
instance
?Z
UnitOfMeasure
)
(
mixtureRatio
?A ?B ?X ?Y ?Z)
(
measure
?M
(
MeasureFn
?T ?Z))
(
part
?A ?M)
(
part
?B ?M)
(
measure
?A
(
MeasureFn
?X ?Z))
(
measure
?B
(
MeasureFn
?Y ?Z)))
(
equal
?T
(
AdditionFn
?X ?Y)))
Food.kif 1248-1262
Wenn
Object
ist ein
fall
von
Mixture
%n{nicht} und
UnitOfMeasure
ist ein
fall
von
UnitOfMeasure
%n{nicht} und
mixtureRatio
Substance
,
** Substance
,
RealNumber
,
** RealNumber
and
** UnitOfMeasure
und das
mass
von
** Object
ist
** RealNumber
** UnitOfMeasure
(s) %n{nicht} und
** Substance
ist ein
teil
von
** Object
%n{nicht} und
** ** Substance
ist ein
teil
von
** Object
%n{nicht} und das
mass
von
** Substance
ist
** RealNumber
** UnitOfMeasure
(s) %n{nicht} und das
mass
von
** ** Substance
ist
** ** RealNumber
** UnitOfMeasure
(s) %n{nicht},
dann
** ** RealNumber
ist gleich (
** RealNumber
und
** ** RealNumber
) %n{nicht}
(=>
(
and
(
instance
?MIT
BarMitzvah
)
(
patient
?MIT ?X)
(
instance
?X
Boy
)
(
member
?X ?GROUP)
(
instance
?GROUP
Judaism
)
(
birthdate
?X ?DAY)
(
instance
?DAY
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
exists
(?Y13 ?BD13)
(
and
(
instance
?Y13
Integer
)
(
equal
?Y13
(
AdditionFn
?Y 13))
(
instance
?BD13
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y13))))
(
equal
(
WhenFn
?MIT)
(
ImmediateFutureFn
?BD13)))))
Biography.kif 69-85
Wenn
Process
ist ein
fall
von
BarMitzvah
%n{nicht} und
Human
ist ein
patient
von
** Process
%n{nicht} und
** Human
ist ein
fall
von
Boy
%n{nicht} und
** Human
ist ein
Mitglied
von
Collection
%n{nicht} und
** Collection
ist ein
fall
von
Judaism
%n{nicht} und
birthdate
** Human
and
Day
und
** Day
ist ein
fall
von der
tag
PositiveInteger
%n{nicht},
dann es gibt
Integer
und
TimePosition
um
** Integer
ist ein
fall
von
Integer
%n{nicht} und
** Integer
ist gleich (
** Integer
und 13) %n{nicht} und
** TimePosition
ist ein
fall
von der
tag
** PositiveInteger
%n{nicht} und die
zeit
des Bestehens von
** Process
ist gleich sofort
nach
** TimePosition
%n{nicht}
(=>
(
and
(
instance
?MIT
BatMitzvah
)
(
patient
?MIT ?X)
(
instance
?X
Girl
)
(
member
?X ?GROUP)
(
instance
?GROUP
Judaism
)
(
birthdate
?X ?DAY)
(
instance
?DAY
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
exists
(?Y13 ?BD13)
(
and
(
instance
?Y13
Integer
)
(
equal
?Y13
(
AdditionFn
?Y 13))
(
instance
?BD13
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y13))))
(
equal
(
WhenFn
?MIT)
(
ImmediateFutureFn
?BD13)))))
Biography.kif 99-115
Wenn
Process
ist ein
fall
von
BatMitzvah
%n{nicht} und
Human
ist ein
patient
von
** Process
%n{nicht} und
** Human
ist ein
fall
von
Girl
%n{nicht} und
** Human
ist ein
Mitglied
von
Collection
%n{nicht} und
** Collection
ist ein
fall
von
Judaism
%n{nicht} und
birthdate
** Human
and
Day
und
** Day
ist ein
fall
von der
tag
PositiveInteger
%n{nicht},
dann es gibt
Integer
und
TimePosition
um
** Integer
ist ein
fall
von
Integer
%n{nicht} und
** Integer
ist gleich (
** Integer
und 13) %n{nicht} und
** TimePosition
ist ein
fall
von der
tag
** PositiveInteger
%n{nicht} und die
zeit
des Bestehens von
** Process
ist gleich sofort
nach
** TimePosition
%n{nicht}
(=>
(
and
(
instance
?UNIT
UnitOfArea
)
(
landAreaOnly
?AREA
(
MeasureFn
?LAND ?UNIT))
(
waterAreaOnly
?AREA
(
MeasureFn
?WATER ?UNIT)))
(
totalArea
?AREA
(
MeasureFn
(
AdditionFn
?LAND ?WATER) ?UNIT)))
Geography.kif 555-560
Wenn
UnitOfMeasure
ist ein
fall
von
UnitOfArea
%n{nicht} und
landAreaOnly
GeographicArea
and
RealNumber
** UnitOfMeasure
(s) und
waterAreaOnly
** GeographicArea
and
** RealNumber
** UnitOfMeasure
(s),
dann
totalArea
** GeographicArea
and (
** RealNumber
und
** ** RealNumber
)
** UnitOfMeasure
(s)
(=>
(
and
(
instance
?UTC
(
HourFn
?H1
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
instance
?CST
(
HourFn
?H2
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
equal
(
RelativeTimeFn
?UTC
CentralTimeZone
) ?CST))
(
equal
?H2
(
AdditionFn
?H1 6)))
Merge.kif 17206-17212
Wenn
TimePosition
ist ein
fall
von die
stunde
NonnegativeInteger
%n{nicht} und
** TimePosition
ist ein
fall
von die
stunde
** NonnegativeInteger
%n{nicht} und ist gleich
** ** TimePosition
%n{nicht},
dann
** ** NonnegativeInteger
ist gleich (
** NonnegativeInteger
und 6) %n{nicht}
(=>
(
and
(
instance
?UTC
(
HourFn
?H1
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
instance
?EST
(
HourFn
?H2
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
equal
(
RelativeTimeFn
?UTC
EasternTimeZone
) ?EST))
(
equal
?H2
(
AdditionFn
?H1 5)))
Merge.kif 17218-17224
Wenn
TimePosition
ist ein
fall
von die
stunde
NonnegativeInteger
%n{nicht} und
** TimePosition
ist ein
fall
von die
stunde
** NonnegativeInteger
%n{nicht} und ist gleich
** ** TimePosition
%n{nicht},
dann
** ** NonnegativeInteger
ist gleich (
** NonnegativeInteger
und 5) %n{nicht}
(=>
(
and
(
instance
?UTC
(
HourFn
?H1
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
instance
?MST
(
HourFn
?H2
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
equal
(
RelativeTimeFn
?UTC
MountainTimeZone
) ?MST))
(
equal
?H2
(
AdditionFn
?H1 7)))
Merge.kif 17194-17200
Wenn
TimePosition
ist ein
fall
von die
stunde
NonnegativeInteger
%n{nicht} und
** TimePosition
ist ein
fall
von die
stunde
** NonnegativeInteger
%n{nicht} und ist gleich
** ** TimePosition
%n{nicht},
dann
** ** NonnegativeInteger
ist gleich (
** NonnegativeInteger
und 7) %n{nicht}
(=>
(
and
(
instance
?UTC
(
HourFn
?H1
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
instance
?PST
(
HourFn
?H2
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
equal
(
RelativeTimeFn
?UTC
PacificTimeZone
) ?PST))
(
equal
?H2
(
AdditionFn
?H1 8)))
Merge.kif 17182-17188
Wenn
TimePosition
ist ein
fall
von die
stunde
NonnegativeInteger
%n{nicht} und
** TimePosition
ist ein
fall
von die
stunde
** NonnegativeInteger
%n{nicht} und ist gleich
** ** TimePosition
%n{nicht},
dann
** ** NonnegativeInteger
ist gleich (
** NonnegativeInteger
und 8) %n{nicht}
(=>
(
and
(
totalLengthOfHighwaySystem
?AREA
(
MeasureFn
?LENGTH ?UNIT))
(
lengthOfPavedHighway
?AREA
(
MeasureFn
?LENGTH1 ?UNIT))
(
lengthOfUnpavedHighway
?AREA
(
MeasureFn
?LENGTH2 ?UNIT))
(
instance
?UNIT
UnitOfLength
))
(
totalLengthOfHighwaySystem
?AREA
(
MeasureFn
(
AdditionFn
?LENGTH1 ?LENGTH2) ?UNIT)))
Transportation.kif 510-517
Wenn
totalLengthOfHighwaySystem
GeographicArea
and
RealNumber
UnitOfMeasure
(s) und
lengthOfPavedHighway
** GeographicArea
and
** RealNumber
1
** UnitOfMeasure
(s) und
lengthOfUnpavedHighway
** GeographicArea
and
** RealNumber
2
** UnitOfMeasure
(s) und
** UnitOfMeasure
ist ein
fall
von
UnitOfLength
%n{nicht},
dann
totalLengthOfHighwaySystem
** GeographicArea
and (
** RealNumber
1 und
** RealNumber
2)
** UnitOfMeasure
(s)
(=>
(
and
(
totalLengthOfHighwaySystem
?AREA
(
MeasureFn
?LENGTH ?UNIT))
(
lengthOfPavedHighway
?AREA
(
MeasureFn
?LENGTH1 ?UNIT))
(
lengthOfUnpavedHighway
?AREA
(
MeasureFn
?LENGTH2 ?UNIT)))
(
equal
?LENGTH
(
AdditionFn
?LENGTH1 ?LENGTH2)))
Transportation.kif 503-508
Wenn
totalLengthOfHighwaySystem
GeographicArea
and
RealNumber
UnitOfMeasure
(s) und
lengthOfPavedHighway
** GeographicArea
and
** RealNumber
1
** UnitOfMeasure
(s) und
lengthOfUnpavedHighway
** GeographicArea
and
** RealNumber
2
** UnitOfMeasure
(s),
dann
** RealNumber
ist gleich (
** RealNumber
1 und
** RealNumber
2) %n{nicht}
(=>
(
conjugate
?COMPOUND1 ?COMPOUND2)
(
exists
(?NUMBER1 ?NUMBER2)
(
and
(
protonNumber
?COMPOUND1 ?NUMBER1)
(
protonNumber
?COMPOUND2 ?NUMBER2)
(
or
(
equal
?NUMBER1
(
AdditionFn
?NUMBER2 1))
(
equal
?NUMBER2
(
AdditionFn
?NUMBER1 1))))))
Mid-level-ontology.kif 6501-6509
Wenn
conjugate
CompoundSubstance
and
** CompoundSubstance
,
dann es gibt
PositiveInteger
und
** PositiveInteger
um
protonNumber
** CompoundSubstance
and
** PositiveInteger
und
protonNumber
** ** CompoundSubstance
and
** ** PositiveInteger
und
** PositiveInteger
ist gleich (
** ** PositiveInteger
und 1) %n{nicht} oder
** ** PositiveInteger
ist gleich (
** PositiveInteger
und 1) %n{nicht}
statement
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4720-4721
Fuer alle
Integer
(
** Integer
+1) ist gleich (
** Integer
und 1) %n{nicht}
Show simplified definition (without tree view)
Show simplified definition (with tree view)
Show without tree
Sigma web home
Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is
open source software
produced by
Articulate Software
and its partners