| 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 Numbers, then (AdditionFn ?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers.") | Merge.kif 4744-4746 | |
| (documentation AdditionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (AdditionFn ?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。") | japanese_format.kif 878-879 | |
| (domain AdditionFn 1 RealNumber) | Merge.kif 4740-4740 | |
| (domain AdditionFn 2 RealNumber) | Merge.kif 4741-4741 | |
| (identityElement AdditionFn 0) | Merge.kif 5323-5323 | |
| (instance AdditionFn AssociativeFunction) | Merge.kif 4736-4736 | |
| (instance AdditionFn BinaryFunction) | Merge.kif 4735-4735 | |
| (instance AdditionFn CommutativeFunction) | Merge.kif 4737-4737 | |
| (instance AdditionFn TotalValuedRelation) | Merge.kif 4739-4739 | |
| (range AdditionFn RealNumber) | Merge.kif 4742-4742 |
| 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 5427-5427 | |
| (termFormat ChineseLanguage AdditionFn "加法函数") | chinese_format.kif 683-683 | |
| (termFormat ChineseTraditionalLanguage AdditionFn "加成") | domainEnglishFormat.kif 5426-5426 | |
| (termFormat EnglishLanguage AdditionFn "addition") | domainEnglishFormat.kif 5425-5425 | |
| (termFormat de AdditionFn "AdditionFn") | terms-de.txt 263-263 | |
| (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 3052-3073 | |
| (=> (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 25562-25578 | |
| (=> (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 1240-1249 | |
| (=> (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 1289-1298 | |
| (=> (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 2350-2372 | |
| (=> (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 438-455 | |
| (=> (and (instance ?LIST ConsecutiveTimeIntervalList) (equal ?T1 (ListOrderFn ?LIST ?N)) (equal ?T2 (ListOrderFn ?LIST (AdditionFn ?N 1)))) (equal (BeginFn ?T2) (EndFn ?T1))) |
Weather.kif 2659-2668 | |
| (=> (and (not (equal ?NUMBER2 0)) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)) |
Merge.kif 5145-5156 |
| 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 | |
| (=> (and (arcLength ?SEMI (MeasureFn ?L ?U)) (equal ?SEMI SemicircularArc)) (exists (?CIR ?C) (and (equal ?CIR Circle) (geometricPart ?SEMI ?CIR) (circumference ?CIR (MeasureFn ?C ?U)) (equal ?C (AdditionFn ?L ?L))))) |
Mid-level-ontology.kif 5700-5710 | |
| (=> (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 6018-6031 | |
| (=> (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 6004-6016 | |
| (=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5132-5143 | |
| (=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L))))) |
Merge.kif 3271-3281 | |
| (=> (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 3096-3115 | |
| (=> (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 3052-3073 | |
| (=> (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 3203-3215 | |
| (=> (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 2178-2190 | |
| (=> (and (instance ?AREA GeographicArea) (objectGeographicCoordinates ?AREA ?LAT ?LONG) (equal (MeasureFn ?DEG AngularDegree) (MagneticDeclinationFn ?LAT ?LONG))) (exists (?MN) (and (headingWRTMagneticNorth ?AREA (MeasureFn ?MN AngularDegree)) (headingWRTTrueNorth ?AREA (MeasureFn (AdditionFn ?MN ?DEG) AngularDegree))))) |
Geography.kif 3950-3962 | |
| (=> (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 1249-1263 | |
| (=> (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 71-87 | |
| (=> (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 102-118 | |
| (=> (and (instance ?UNIT UnitOfArea) (landAreaOnly ?AREA (MeasureFn ?LAND ?UNIT)) (waterAreaOnly ?AREA (MeasureFn ?WATER ?UNIT))) (totalArea ?AREA (MeasureFn (AdditionFn ?LAND ?WATER) ?UNIT))) |
Geography.kif 725-730 | |
| (=> (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 17381-17387 | |
| (=> (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 17393-17399 | |
| (=> (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 17369-17375 | |
| (=> (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 17357-17363 | |
| (=> (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 | |
| (=> (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 | |
| (=> (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 7438-7446 |
| statement |
|
|
| (forall (?NUMBER) (equal (SuccessorFn ?NUMBER) (AdditionFn ?NUMBER 1))) |
Merge.kif 4748-4749 |
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
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