| appearance as argument number 1 |
|
| (documentation KappaFn ChineseLanguage "这是一个组成类别的运算符，它拿两个参数：一个变数和一个 包含属于这个变数，起码一个不受限制例子的公式。应用 KappaFn 到一个变数和一个公式的结果是一个包含 满足这个公式东西的 SetOrClass。例如：我们用以下的方式表达小于100素数的 SetOrClass： (KappaFn ?NUMBER (and (instance ?NUMBER PrimeNumber) (lessThan ?NUMBER 100)))。注：请尽量避免 用这个函数，因为目前还没有编写公理来支持它。") | chinese_format.kif 2318-2322 | |
| (documentation KappaFn EnglishLanguage "A class-forming operator that takes two arguments: a variable and a formula containing at least one unbound occurrence of the variable. The result of applying KappaFn to a variable and a formula is the SetOrClass of things that satisfy the formula. For example, we can denote the SetOrClass of prime numbers that are less than 100 with the following expression: (KappaFn ?NUMBER (and (instance ?NUMBER PrimeNumber) (lessThan ?NUMBER 100))). Note that the use of this function is discouraged, since there is currently no axiomatic support for it.") | Merge.kif 5310-5318 | |
| (domain KappaFn 1 SymbolicString) | Merge.kif 5306-5306 | |
| (domain KappaFn 2 Formula) | Merge.kif 5307-5307 | |
| (instance KappaFn BinaryFunction) | Merge.kif 5304-5304 | |
| (instance KappaFn PartialValuedRelation) | Merge.kif 5305-5305 | |
| (range KappaFn Class) | Merge.kif 5308-5308 |
| appearance as argument number 2 |
|
|
| (format ChineseLanguage KappaFn " %1 所描述的类别") | chinese_format.kif 508-508 | |
| (format EnglishLanguage KappaFn "the class described by %1") | english_format.kif 516-516 | |
| (termFormat ChineseLanguage KappaFn "卡帕") | domainEnglishFormat.kif 32119-32119 | |
| (termFormat ChineseLanguage KappaFn "组成类别函数") | chinese_format.kif 509-509 | |
| (termFormat ChineseTraditionalLanguage KappaFn "卡帕") | domainEnglishFormat.kif 32118-32118 | |
| (termFormat EnglishLanguage KappaFn "kappa") | domainEnglishFormat.kif 32117-32117 |
| antecedent |
|
|
| (<=> (and (instance ?Account PersonalAccount) (greaterThan (CardinalityFn (KappaFn ?Agent (accountHolder ?Account ?Agent))) 1)) (instance ?Account JointAccount)) |
FinancialOntology.kif 951-955 | |
| (=> (and (instance ?BUYINGS Collection) (instance ?GMB CurrencyMeasure) (instance ?TOTAL RealNumber) (equal ?GMB (GMBFn ?BUYINGS)) (equal ?TOTAL (CardinalityFn (KappaFn ?ITEM (and (instance ?ITEM Object) (exists (?BUYING) (and (member ?BUYING ?BUYINGS) (patient ?ITEM ?BUYING)))))))) (equal (ABPFn ?BUYINGS) (DivisionFn ?GMB ?TOTAL))) |
UXExperimentalTerms.kif 3444-3464 | |
| (=> (and (instance ?SELLINGS Collection) (instance ?GMV CurrencyMeasure) (instance ?TOTAL RealNumber) (equal ?GMV (GMVFn ?SELLINGS)) (equal ?TOTAL (CardinalityFn (KappaFn ?ITEM (and (instance ?ITEM Object) (exists (?SELLING) (and (member ?SELLING ?SELLINGS) (patient ?SELLING ?ITEM)))))))) (equal (ASPFn ?SELLINGS) (DivisionFn ?GMV ?TOTAL))) |
UXExperimentalTerms.kif 3487-3507 |
| consequent |
|
|
| (<=> (equal (BirthsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (DivisionFn (PopulationFn ?AREA) 1000) ?THOUSANDS) (equal ?BIRTHCOUNT (CardinalityFn (KappaFn ?BIRTH (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INFANT) (instance ?INFANT Human) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA))))) (equal (DivisionFn ?BIRTHCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 104-117 | |
| (<=> (equal (DeathsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (DivisionFn (PopulationFn ?AREA) 1000) ?THOUSANDS) (equal ?DEATHCOUNT (CardinalityFn (KappaFn ?DEATH (and (instance ?DEATH Death) (experiencer ?DEATH ?PERSON) (instance ?PERSON Human) (during (WhenFn ?DEATH) (YearFn ?YEAR)) (equal (WhereFn ?DEATH (WhenFn ?DEATH)) ?AREA))))) (equal (DivisionFn ?DEATHCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 138-151 | |
| (<=> (equal (DeathsPerThousandLiveBirthsFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal ?BIRTHCOUNT (CardinalityFn (KappaFn ?BIRTH (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INFANT) (instance ?INFANT Human) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA))))) (equal (DivisionFn ?BIRTHCOUNT 1000) ?THOUSANDSOFBIRTHS) (equal ?INFANTDEATHCOUNT (CardinalityFn (KappaFn ?DEATH (and (instance ?DEATH Death) (experiencer ?DEATH ?INFANT) (instance ?INFANT Human) (age ?INFANT (MeasureFn ?AGE YearDuration)) (lessThan ?AGE 1) (during (WhenFn ?DEATH) (YearFn ?YEAR)) (equal (WhereFn ?DEATH (WhenFn ?DEATH)) ?AREA))))) (equal (DivisionFn ?INFANTDEATHCOUNT ?THOUSANDSOFBIRTHS) ?REALNUMBER))) |
People.kif 253-277 | |
| (<=> (equal (FemaleLifeExpectancyAtBirthFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (exists (?LIST) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (attribute ?INDIVIDUAL Female) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER)))) |
People.kif 411-442 | |
| (<=> (equal (LifeExpectancyAtBirthFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (exists (?LIST) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER)))) |
People.kif 323-353 | |
| (<=> (equal (MaleLifeExpectancyAtBirthFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (exists (?LIST) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (attribute ?INDIVIDUAL Male) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER)))) |
People.kif 367-398 | |
| (<=> (equal (MaleToFemaleRatioFn ?AREA) ?REALNUMBER) (and (equal ?MALECOUNT (CardinalityFn (KappaFn ?MALE (and (instance ?MALE Human) (attribute ?MALE Male) (inhabits ?MALE ?AREA))))) (equal ?FEMALECOUNT (CardinalityFn (KappaFn ?FEMALE (and (instance ?FEMALE Human) (attribute ?FEMALE Female) (inhabits ?FEMALE ?AREA))))) (equal (DivisionFn ?MALECOUNT ?FEMALECOUNT) ?REALNUMBER))) |
People.kif 221-238 | |
| (<=> (equal (MigrantsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (SubtractionFn ?YEAR ?PREVIOUSYEAR) 1) (holdsDuring (YearFn ?YEAR) (equal (PopulationFn ?AREA) ?POPULATION)) (equal (DivisionFn ?POPULATION 1000) ?THOUSANDS) (equal ?IMMIGRATION (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (holdsDuring (YearFn ?PREVIOUSYEAR) (not (inhabits ?PERSON ?AREA))) (holdsDuring (YearFn ?YEAR) (inhabits ?PERSON ?AREA)))))) (equal ?EMMIGRATION (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (holdsDuring (YearFn ?PREVIOUSYEAR) (inhabits ?PERSON ?AREA)) (holdsDuring (YearFn ?YEAR) (not (inhabits ?PERSON ?AREA))))))) (equal (SubtractionFn ?IMMIGRATION ?EMMIGRATION) ?MIGRATIONCOUNT) (equal (DivisionFn ?MIGRATIONCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 174-202 | |
| (<=> (lengthOfBroadGaugeRailway ?AREA ?LENGTH) (length (KappaFn ?RAILWAYS (and (instance ?RAILWAYS BroadGaugeRailway) (located ?RAILWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 179-186 | |
| (<=> (lengthOfCrudeOilPipeline ?AREA ?LENGTH) (length (KappaFn ?PIPELINE (and (instance ?PIPELINE CrudeOilPipeline) (located ?PIPELINE ?AREA))) ?LENGTH)) |
Transportation.kif 701-708 | |
| (<=> (lengthOfDualGaugeRailway ?AREA ?LENGTH) (length (KappaFn ?RAILWAYS (and (instance ?RAILWAYS DualGaugeRailway) (located ?RAILWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 207-214 | |
| (<=> (lengthOfElectrifiedRailway ?AREA ?LENGTH) (length (KappaFn ?RAILWAYS (and (instance ?RAILWAYS ElectrifiedRailway) (located ?RAILWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 125-132 | |
| (<=> (lengthOfExpresswaySystem ?AREA ?LENGTH) (length (KappaFn ?HIGHWAYS (and (instance ?HIGHWAYS Expressway) (located ?HIGHWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 558-565 | |
| (<=> (lengthOfMultipleTrackRailway ?AREA ?LENGTH) (length (KappaFn ?RAILWAYS (and (instance ?RAILWAYS MultipleTrackRailway) (located ?RAILWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 152-159 | |
| (<=> (lengthOfNarrowGaugeRailway ?AREA ?LENGTH) (length (KappaFn ?RAILWAYS (and (instance ?RAILWAYS NarrowGaugeRailway) (located ?RAILWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 234-241 | |
| (<=> (lengthOfNaturalGasPipeline ?AREA ?LENGTH) (length (KappaFn ?PIPELINE (and (instance ?PIPELINE NaturalGasPipeline) (located ?PIPELINE ?AREA))) ?LENGTH)) |
Transportation.kif 724-731 | |
| (<=> (lengthOfPavedHighway ?AREA ?LENGTH) (length (KappaFn ?HIGHWAYS (and (instance ?HIGHWAYS SurfacedRoadway) (located ?HIGHWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 532-539 | |
| (<=> (lengthOfPetroleumProductPipeline ?AREA ?LENGTH) (length (KappaFn ?PIPELINE (and (instance ?PIPELINE PetroleumProductPipeline) (located ?PIPELINE ?AREA))) ?LENGTH)) |
Transportation.kif 747-754 | |
| (<=> (lengthOfStandardGaugeRailway ?AREA ?LENGTH) (length (KappaFn ?RAILWAYS (and (instance ?RAILWAYS StandardGaugeRailway) (located ?RAILWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 262-269 | |
| (<=> (lengthOfUnclassifiedGaugeRailway ?AREA ?LENGTH) (length (KappaFn ?RAILWAYS (and (located ?RAILWAYS ?AREA) (not (instance ?RAILWAYS (UnionFn StandardGaugeRailway (UnionFn BroadGaugeRailway (UnionFn DualGaugeRailway NarrowGaugeRailway))))))) ?LENGTH)) |
Transportation.kif 291-303 | |
| (<=> (lengthOfUnpavedHighway ?AREA ?LENGTH) (length (KappaFn ?HIGHWAYS (and (instance ?HIGHWAYS UnsurfacedRoadway) (located ?HIGHWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 590-597 | |
| (<=> (totalFacilityTypeInArea ?AREA (ExtensionFn AirportWithPavedRunway) ?COUNT) (cardinality (KappaFn ?AIRPORT (exists (?RUNWAY) (and (instance ?AIRPORT Airport) (instance ?RUNWAY PavedRunway) (part ?RUNWAY ?AIRPORT) (located ?AIRPORT ?AREA)))) ?COUNT)) |
Transportation.kif 1266-1276 | |
| (<=> (totalFacilityTypeInArea ?AREA ?TYPE ?COUNT) (cardinality (KappaFn ?ITEM (and (instance ?ITEM ?TYPE) (located ?ITEM ?AREA))) ?COUNT)) |
Transportation.kif 1210-1217 | |
| (<=> (totalLengthOfHighwaySystem ?AREA ?LENGTH) (length (KappaFn ?HIGHWAYS (and (instance ?HIGHWAYS Roadway) (located ?HIGHWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 478-485 | |
| (<=> (totalLengthOfRailwaySystem ?AREA ?LENGTH) (length (KappaFn ?RAILWAYS (and (instance ?RAILWAYS Railway) (located ?RAILWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 98-105 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| (equal (AvailableForMilitaryServiceMaleFn ?AREA) (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (attribute ?PERSON Male) (militaryAge ?AREA ?MILITARYAGE) (age ?PERSON ?AGE) (greaterThanOrEqualTo ?AGE ?MILITARYAGE) (inhabits ?PERSON ?AREA))))) |
Military.kif 867-876 | |
| (equal (ChildrenBornPerWomanFn ?AREA (YearFn ?YEAR)) (CardinalityFn (KappaFn ?INFANT (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INFANT) (agent ?BIRTH ?WOMAN) (instance ?WOMAN Human) (attribute ?WOMAN Female) (holdsDuring (YearFn ?YEAR) (inhabits ?WOMAN ?AREA)))))) |
People.kif 462-472 | |
| (equal (FitForMilitaryServiceMaleFn ?AREA) (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (attribute ?PERSON Male) (instance ?PROCESS MilitaryProcess) (fitForMilitaryService ?PERSON ?PROCESS) (militaryAge ?AREA ?MILITARYAGE) (age ?PERSON ?AGE) (greaterThanOrEqualTo ?AGE ?MILITARYAGE) (inhabits ?PERSON ?AREA))))) |
Military.kif 890-901 | |
| (equal (PopulationFn ?AREA) (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (inhabits ?PERSON ?AREA))))) |
People.kif 49-54 | |
| (equal (ReachingMilitaryAgeAnnuallyMaleFn ?AREA ?YEAR) (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (attribute ?PERSON Male) (militaryAge ?AREA ?MILITARYAGE) (equal ?AGEMINUSONE (SubtractionFn ?AGE 1)) (holdsDuring ?YEAR (or (age ?PERSON ?AGEMINUSONE) (age ?PERSON ?AGE))) (equal ?AGE ?MILITARYAGE) (inhabits ?PERSON ?AREA))))) |
Military.kif 928-941 |
|
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