| appearance as argument number 2 |
|
| (termFormat EnglishLanguage forall "forall") | domainEnglishFormat.kif 65868-65868 |
| antecedent |
|
|
| (<=> (holdsDuring ?T (and (instance ?PERSON Human) (forall (?ORG) (not (employs ?ORG ?PERSON))))) (holdsDuring ?T (attribute ?PERSON Unemployed))) |
Merge.kif 17350-17358 | 实体 是 人类 的 instance 和 对所有 另一个 实体 那个 另外 实体 doesn't employs 那个 实体 在 时间位置 holdsDuring 若且唯若 失业的 是 那个 实体 的 attribute 在 那个 时间位置 holdsDuring |
| (=> (and (climateTypeInArea ?AREA ColdClimateZone) (forall (?MO) (and (instance ?MO Month) (averageTemperatureForPeriod ?AREA ?MO (MeasureFn ?TEMP CelsiusDegree))))) (greaterThan 10.0 ?TEMP)) |
Geography.kif 1516-1524 | |
| (=> (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 5984-5997 | |
| (=> (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 5970-5982 | |
| (=> (and (instance ?AUCTIONS Collection) (forall (?AUC) (=> (member ?AUC ?AUCTIONS) (instance ?AUC Auctioning)))) (exists (?AMOUNT ?TOTAL_PURCHASE_AMOUNT) (and (total (KappaFn ?AMOUNT (transactionAmount ?AUC ?AMOUNT)) ?TOTAL_PURCHASE_AMOUNT) (equal (AuctionGMBFn ?AUCTIONS) ?TOTAL_PURCHASE_AMOUNT)))) |
UXExperimentalTerms.kif 3202-3215 | |
| (=> (and (instance ?COLL Collection) (forall (?MEMBER) (=> (member ?MEMBER ?COLL) (instance ?MEMBER FinancialTransaction)))) (exists (?ITEM ?BUYING) (equal (CardinalityFn (KappaFn ?ITEM (and (instance ?ITEM Physical) (instance ?BUYING Buying) (member ?BUYING ?COLL) (patient ?BUYING ?ITEM)))) (BoughtItemsFn ?COLL)))) |
UXExperimentalTerms.kif 2887-2903 | |
| (=> (and (instance ?COLL Collection) (forall (?MEMBER) (=> (member ?MEMBER ?COLL) (instance ?MEMBER WebListing)))) (equal (DivisionFn (CardinalityFn (exists (?LISTING ?SITE ?ITEM) (KappaFn ?LISTING (and (instance ?LISTING WebListing) (instance ?SITE WebSite) (instance ?ITEM Physical) (member ?LISTING ?COLL) (patient ?LISTING ?ITEM) (hostedOn ?LISTING ?SITE) (exists (?BUYING) (and (instance ?BUYING Buying) (patient ?BUYING ?ITEM) (eCommerceSite ?BUYING ?SITE))))))) (CardinalityFn ?COLL)) (BidCountFn ?COLL))) |
UXExperimentalTerms.kif 2845-2870 | |
| (=> (and (instance ?COLL Collection) (forall (?MEMBER) (=> (member ?MEMBER ?COLL) (instance ?MEMBER WebListing)))) (exists (?BIDDING ?ITEM ?LISTING ?BIDDING) (equal (CardinalityFn (KappaFn ?BIDDING (and (instance ?ITEM Physical) (instance ?LISTING WebListing) (instance ?BIDDING Bidding) (member ?LISTING ?COLL) (objectOfBid ?BIDDING ?ITEM) (patient ?LISTING ?ITEM)))) (BidCountFn ?COLL)))) |
UXExperimentalTerms.kif 2922-2940 | |
| (=> (and (instance ?COLL Collection) (instance ?SITE WebSite) (instance ?AGENT AutonomousAgent) (instance ?LISTING WebListing) (instance ?TIME TimePoint) (listingSeller ?LISTING ?AGENT) (not (member ?LISTING ?COLL)) (forall (?ITEM ?MEMBER) (and (=> (and (instance ?ITEM WebListing) (member ?ITEM (SellersItemsFn ?AGENT ?SITE)) (temporalPart ?TIME (WhenFn ?ITEM)) (not (equal ?ITEM ?LISTING))) (member ?ITEM ?COLL)) (=> (member ?MEMBER ?COLL) (and (temporalPart ?TIME (WhenFn ?ITEM)) (instance ?MEMBER WebListing)))))) (equal (SellersOtherItemsFn ?AGENT ?SITE ?LISTING ?TIME) ?COLL)) |
UXExperimentalTerms.kif 1033-1060 |
|
| (=> (and (instance ?PURCHASES Collection) (forall (?MEMBER) (=> (member ?MEMBER ?PURCHASES) (instance ?MEMBER Buying))) (exists (?REGION) (and (instance ?REGION GeopoliticalArea) (forall (?BUYER ?BUYING) (=> (and (instance ?BUYER AutonomousAgent) (instance ?BUYING Buying) (member ?BUYING ?PURCHASES) (agent ?BUYING ?BUYER)) (located ?BUYER ?REGION)))))) (exists (?AMOUNT ?PURCHASE ?TOTAL_PURCHASE_AMOUNT) (and (total (KappaFn ?AMOUNT (and (instance ?PURCHASE Buying) (member ?PURCHASE ?PURCHASES) (transactionAmount ?PURCHASE ?AMOUNT))) ?TOTAL_PURCHASE_AMOUNT) (equal (GMBFn ?PURCHASES) ?TOTAL_PURCHASE_AMOUNT)))) |
UXExperimentalTerms.kif 2956-2983 | |
| (=> (and (instance ?SALES Collection) (forall (?MEMBER) (=> (member ?MEMBER ?SALES) (instance ?MEMBER Selling))) (exists (?REGION) (and (instance ?REGION GeopoliticalArea) (forall (?SELLER ?SELLING) (=> (and (instance ?SELLER AutonomousAgent) (instance ?SELLING Buying) (member ?SELLING ?SALES) (agent ?SELLING ?SELLER)) (located ?SELLER ?REGION)))))) (exists (?AMOUNT ?SALE ?TOTAL_SALE_AMOUNT) (and (total (KappaFn ?AMOUNT (and (instance ?SALE Selling) (member ?SALE ?SALES) (transactionAmount ?SALE ?AMOUNT))) ?TOTAL_SALE_AMOUNT) (equal (GMVFn ?SALES) ?TOTAL_SALE_AMOUNT)))) |
UXExperimentalTerms.kif 2999-3026 | |
| (=> (and (instance ?SEAT AuditoriumSeat) (part ?SEAT ?AUDITORIUM) (part ?STAGE ?AUDITORIUM) (instance ?AUDITORIUM Auditorium) (instance ?STAGE PerformanceStage) (located ?PERSON ?SEAT) (instance ?PERSON Human) (subclass ?SEE Seeing) (forall (?INST) (=> (instance ?INST ?SEE) (patient ?INST ?STAGE)))) (capability ?SEE agent ?PERSON)) |
Mid-level-ontology.kif 8124-8138 | |
| (=> (and (instance ?VISITOR Human) (instance ?COLL Collection) (forall (?EXPERIMENT ?EVENT) (=> (exists (?CLASS) (and (instance ?EXPERIMENT Experimenting) (instance ?EVENT Process) (member ?EVENT (QualifyingEventsFn ?EXPERIMENT)) (instance ?EVENT ?CLASS) (capability ?CLASS experiencer ?VISITOR))) (member ?EVENT ?COLL))) (=> (member ?PROC ?COLL) (and (instance ?PROC Process) (exists (?EXP ?PROCESS) (and (instance ?EXP Experimenting) (member ?PROC (QualifyingEventsFn ?EXP)) (instance ?PROC ?PROCESS) (capability ?PROCESS experiencer ?VISITOR)))))) (equal (QualifiedTreatmentsFn ?VISITOR) ?COLL)) |
UXExperimentalTerms.kif 4241-4267 | |
| (=> (and (instance ?VISITOR Human) (instance ?QPVIEWS Collection) (forall (?PAGE ?ACCESSING ?EXPERIMENT) (=> (and (instance ?PAGE WebPage) (instance ?ACCESSING AccessingWebPage) (instance ?EXPERIMENT Experimenting) (agent ?ACCESSING ?VISITOR) (patient ?ACCESSING ?PAGE) (treatedPage ?PAGE ?EXPERIMENT)) (member ?ACCESSING ?QPVIEWS)))) (equal ?QPVIEWS (QPViewsFn ?VISITOR))) |
UXExperimentalTerms.kif 4175-4190 |
|
| (=> (and (instance ?VISITS Collection) (instance ?HYPERLINK HypertextLink) (forall (?ACCESSING) (and (member ?ACCESSING ?PAGE) (and (instance ?ACCESSING AccessingWebPage) (component ?PAGE ?HYPERLINK))))) (exists (?CLICKS) (and (instance ?CLICKS Collection) (forall (?CLICK) (=> (and (instance ?CLICK RequestingHyperlink) (patient ?CLICK ?HYPERLINK)) (member ?CLICK ?CLICKS))) (equal (ClickThroughRateFn ?VISITS ?HYPERLINK) (DivisionFn (CardinalityFn ?CLICKS) (CardinalityFn ?VISITS)))))) |
UXExperimentalTerms.kif 3333-3356 | |
| (=> (and (instance ?VISITS Collection) (instance ?PURCHASES Collection) (subCollection ?PURCHASES ?VISITS) (forall (?MEMBER) (=> (member ?MEMBER ?VISITS) (instance ?MEMBER AccessingWebPage))) (forall (?BUYING ?VISITOR ?ACCESSING ?BUYING ?PAGE) (=> (and (instance ?VISITOR Human) (instance ?BUYING Buying) (instance ?ACCESSING AccessingWebPage) (instance ?PAGE WebPage) (member ?ACCESSING ?VISITS) (destination ?ACCESSING ?PAGE) (agent ?BUYING ?VISITOR) (agent ?ACCESSING ?VISITOR) (during (WhenFn ?BUYING) (WhenFn ?ACCESSING)) (instrument ?BUYING ?PAGE)) (member ?BUYING ?PURCHASES)))) (exists (?INTERVAL ?PURCHASE_IN_INTERVAL ?VISIT_IN_INTERVAL) (equal (SCRFn ?VISITS ?INTERVAL) (DivisionFn (CardinalityFn (KappaFn ?PURCHASE_IN_INTERVAL (and (member ?PURCHASE_IN_INTERVAL ?PURCHASES) (during (WhenFn ?PURCHASE_IN_INTERVAL) ?INTERVAL)))) (CardinalityFn (KappaFn ?VISIT_IN_INTERVAL (and (member ?VISIT_IN_INTERVAL ?VISITS) (during (WhenFn ?PURCHASE_IN_INTERVAL) ?INTERVAL)))))))) |
UXExperimentalTerms.kif 3668-3704 |
|
| consequent |
|
|
| (<=> (and (instance ?Y (YearFn ?YEAR)) (equal (MaleLifeExpectancyAtBirthFn ?AREA ?Y) ?REALNUMBER)) (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH) (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) ?Y) (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 357-390 | 年 是 那个 年EAR year 的 instance 和 地缘政治区域 和 那个 年 的 male 出生估计寿命 equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| (<=> (and (instance ?YEAR (YearFn ?Y)) (equal (FemaleLifeExpectancyAtBirthFn ?AREA ?YEAR) ?REALNUMBER)) (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH) (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) ?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 403-436 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 female 出生预期寿命 equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| (<=> (and (instance ?YEAR (YearFn ?Y)) (equal (LifeExpectancyAtBirthFn ?AREA ?YEAR) ?REALNUMBER)) (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH) (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) ?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 310-342 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的出生预期 life equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| (<=> (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 若且唯若 有存在 另一个 串列 和 正整数 这样 那个 另外 串列 的长度 equal 那个 串列 的长度 和 那个 另外 串列 的第 1 几个元素 equal 那个 串列 的第 1 几个元素 和 对所有 另一个 正整数
|
| (<=> (larger ?OBJ1 ?OBJ2) (forall (?QUANT1 ?QUANT2 ?UNIT) (=> (and (measure ?OBJ1 (MeasureFn ?QUANT1 ?UNIT)) (measure ?OBJ2 (MeasureFn ?QUANT2 ?UNIT)) (instance ?UNIT UnitOfLength)) (greaterThan ?QUANT1 ?QUANT2)))) |
Merge.kif 7800-7808 | 客体 larger 另一个 客体 若且唯若 对所有 实数， 另一个 实数， and 和 测量单位 |
| (<=> (subCollection ?COLL1 ?COLL2) (forall (?MEMBER) (=> (member ?MEMBER ?COLL1) (member ?MEMBER ?COLL2)))) |
Merge.kif 1290-1295 | 群体 是 另一个 群体 的 真正的子集 若且唯若 对所有 物理 |
| (=> (allRoomsPhysicalAmenity ?INV ?OBJ) (forall (?X) (=> (memberType ?INV ?X) (roomAmenity ?X ?OBJ)))) |
Hotel.kif 171-176 |
|
| (=> (allRoomsPolicy ?INV ?POLICY) (forall (?X) (=> (memberType ?INV ?X) (roomPolicy ?X ?POLICY)))) |
Hotel.kif 233-238 |
|
| (=> (allRoomsServiceAmenity ?INV ?OBJ) (forall (?X) (=> (memberType ?INV ?X) (roomAmenity ?X ?OBJ)))) |
Hotel.kif 218-223 |
|
| (=> (and (attribute ?OBJ ?SPHERE) (instance ?SPHERE Sphere)) (exists (?CENTER ?DIST) (forall (?PT) (=> (pointOfFigure ?PT ?OBJ) (geometricDistance ?PT ?CENTER ?DIST))))) |
Mid-level-ontology.kif 5539-5547 | |
| (=> (and (attribute ?OBJ Monochromatic) (superficialPart ?PART ?OBJ) (attribute ?PART ?COLOR) (instance ?COLOR PrimaryColor)) (forall (?ELEMENT) (=> (superficialPart ?ELEMENT ?OBJ) (attribute ?ELEMENT ?COLOR)))) |
Merge.kif 17792-17801 | |
| (=> (and (citizen ?AGENT ?POLITY) (subProposition UniversalSuffrageLaw (RegionalLawFn ?POLITY))) (confersRight (forall (?VOTINGAGE ?AGE ?ELECTION) (=> (and (citizen ?AGENT ?POLITY) (suffrageAgeMinimum ?POLITY (MeasureFn ?VOTINGAGE YearDuration)) (age ?AGENT (MeasureFn ?AGE YearDuration)) (greaterThanOrEqualTo ?AGE ?VOTINGAGE) (instance ?ELECTION (ElectionFn ?POLITY))) (exists (?VOTING) (and (instance ?VOTING (VotingFn ?ELECTION)) (agent ?VOTING ?AGENT))))) (RegionalLawFn ?POLITY) ?AGENT)) |
Government.kif 1094-1114 | |
| (=> (and (element ?X (PropertyFn ?HOTEL)) (instance ?X RoomInventory)) (forall (?Y) (=> (member ?Y ?X) (element ?Y (PropertyFn ?HOTEL))))) |
Hotel.kif 147-154 | |
| (=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0)))) |
Merge.kif 4855-4866 | |
| (=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?GREATER) (and (greaterThan ?GREATER ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?GREATER) 0))))))) |
Merge.kif 4868-4882 | |
| (=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 4940-4950 | |
| (=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?LESS) (and (lessThan ?LESS ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?LESS ?ELEMENT) 0))))))) |
Merge.kif 4952-4966 | |
| (=> (and (equal ?D (AlbumCopiesFn ?A ?DS)) (instance ?X ?D)) (forall (?S) (=> (inList ?S ?A) (exists (?C) (and (copy ?C ?S) (stored ?C ?X)))))) |
Music.kif 936-946 |
|
| (=> (and (hole ?HOLE1 ?OBJ) (hole ?HOLE2 ?OBJ)) (forall (?HOLE3) (=> (part ?HOLE3 (MereologicalSumFn ?HOLE1 ?HOLE2)) (hole ?HOLE3 ?OBJ)))) |
Merge.kif 9959-9966 | |
| (=> (and (instance ?AGENT AutonomousAgent) (instance ?SITE WebSite)) (exists (?COLL) (and (instance ?COLL Collection) (forall (?LISTING) (=> (and (instance ?LISTING WebListing) (hostedOn ?LISTING ?SITE) (listingSeller ?LISTING ?AGENT)) (member ?LISTING ?COLL))) (equal (SellersItemsFn ?AGENT ?SITE) ?COLL)))) |
UXExperimentalTerms.kif 992-1008 |
|
| (=> (and (instance ?CHIN Chin) (instance ?FACE Face) (part ?CHIN ?FACE)) (forall (?PART) (=> (and (part ?PART ?FACE) (not (part ?PART ?CHIN))) (orientation ?PART ?CHIN Below)))) |
Mid-level-ontology.kif 13826-13837 | |
| (=> (and (instance ?G Grinding) (patient ?G ?O) (instance ?O CorpuscularObject)) (holdsDuring (EndFn (WhenFn ?G)) (exists (?C) (and (result ?G ?C) (instance ?C Collection) (forall (?M) (=> (member ?M ?C) (part ?M ?O))))))) |
Food.kif 1012-1026 | |
| (=> (and (instance ?INTERVAL TimeInterval) (instance ?SITE WebSite)) (exists (?NEWBUYERS) (and (instance ?NEWBUYERS Collection) (forall (?AGENT) (=> (member ?AGENT ?NEWBUYERS) (and (exists (?BUYING) (and (instance ?AGENT AutonomousAgent) (instance ?BUYING Buying) (agent ?BUYING ?AGENT) (instrument ?BUYING ?SITE) (during ?BUYING ?INTERVAL))) (not (exists (?INTERVAL_BEFORE) (and (instance ?INTERVAL_BEFORE TimeInterval) (earlier ?INTERVAL_BEFORE ?INTERVAL) (holdsDuring ?INTERVAL_BEFORE (exists (?BUYING_BEFORE) (and (instance ?BUYING_BEFORE Buying) (agent ?BUYING_BEFORE ?AGENT) (instrument ?BUYING_BEFORE ?SITE) (during ?BUYING_BEFORE ?INTERVAL)))))))))) (equal (SiteWideNewBuyersFn ?INTERVAL ?SITE) ?NEWBUYERS)))) |
UXExperimentalTerms.kif 3376-3408 |
|
| (=> (and (instance ?INTERVAL TimeInterval) (instance ?SITE WebSite)) (exists (?NEWREGISTRATIONS) (and (instance ?NEWREGISTRATIONS Collection) (forall (?USER) (=> (and (instance ?USER Human) (not (exists (?INTERVAL_BEFORE) (and (instance ?INTERVAL_BEFORE TimeInterval) (earlier ?INTERVAL_BEFORE ?INTERVAL) (holdsDuring ?INTERVAL_BEFORE (registeredUser ?USER ?SITE))))) (exists (?INTERVAL_DURING) (and (instance ?INTERVAL_DURING TimeInterval) (during ?INTERVAL_DURING ?INTERVAL) (holdsDuring ?INTERVAL (registeredUser ?USER ?SITE))))) (member ?USER ?NEWREGISTRATIONS))) (equal ?NEWREGISTRATIONS (SiteWideNewRegistrationsFn ?INTERVAL ?SITE))))) |
UXExperimentalTerms.kif 3428-3455 |
|
| (=> (and (instance ?INTERVAL TimeInterval) (instance ?SITE WebSite)) (exists (?NEWSELLERS) (and (instance ?NEWSELLERS Collection) (forall (?AGENT) (=> (member ?AGENT ?NEWSELLERS) (and (exists (?SELLING) (and (instance ?AGENT AutonomousAgent) (instance ?SELLING Selling) (agent ?SELLING ?AGENT) (instrument ?SELLING ?SITE) (during ?SELLING ?INTERVAL))) (not (exists (?INTERVAL_BEFORE) (and (instance ?INTERVAL_BEFORE TimeInterval) (earlier ?INTERVAL_BEFORE ?INTERVAL) (holdsDuring ?INTERVAL_BEFORE (exists (?SELLING_BEFORE) (and (instance ?SELLING_BEFORE Selling) (agent ?SELLING_BEFORE ?AGENT) (instrument ?SELLING_BEFORE ?SITE) (during ?SELLING_BEFORE ?INTERVAL)))))))))) (equal (SiteWideNewSellersFn ?INTERVAL ?SITE) ?NEWSELLERS)))) |
UXExperimentalTerms.kif 3475-3507 |
|
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| (containsInformation (forall (?AGENT ?VOTER ?ELECTION ?VOTING) (=> (and (instance ?ELECTION (ElectionFn ?AGENT)) (instance ?VOTING (VotingFn ?ELECTION)) (agent ?VOTING ?VOTER)) (attribute ?VOTER Male))) ExclusiveMaleSuffrage) |
Government.kif 1203-1210 | 对所有 ?AGENT， ?VOTER,， ， ?ELECTION， and 和 ?VOTING
|
| (containsInformation (forall (?COUNTRY ?ELECTION ?VOTING ?VOTER) (=> (and (instance ?COUNTRY Nation) (instance ?ELECTION (ElectionFn ?COUNTRY)) (instance ?VOTING (VotingFn ?ELECTION)) (agent ?VOTING ?VOTER)) (citizen ?VOTER ?COUNTRY))) VoterCitizenshipRequirement) |
Government.kif 885-893 | 对所有 ?COUNTRY， ?ELECTION,， ， ?VOTING， and 和 ?VOTER
|
| (containsInformation (forall (?POLITY ?AGENT ?ELECTION ?VOTINGAGE ?AGE) (=> (and (citizen ?AGENT ?POLITY) (suffrageAgeMinimum ?POLITY (MeasureFn ?VOTINGAGE YearDuration)) (age ?AGENT (MeasureFn ?AGE YearDuration)) (greaterThanOrEqualTo ?AGE ?VOTINGAGE) (instance ?ELECTION (ElectionFn ?POLITY))) (capability (VotingFn ?ELECTION) agent ?AGENT))) UniversalSuffrageLaw) |
Government.kif 1054-1065 | 对所有 ?POLITY， ?AGENT,， ， ?ELECTION,， ， ?VOTINGAGE， and 和 ?AGE
|
| (containsInformation (forall (?POLITY ?VOTER ?ELECTION ?VOTINGAGE ?AGE) (=> (and (citizen ?VOTER ?POLITY) (suffrageAgeMinimum ?POLITY (MeasureFn ?VOTINGAGE YearDuration)) (age ?VOTER (MeasureFn ?AGE YearDuration)) (greaterThanOrEqualTo ?AGE ?VOTINGAGE) (instance ?ELECTION (ElectionFn ?POLITY))) (exists (?VOTING) (and (instance ?VOTING (VotingFn ?ELECTION)) (agent ?VOTING ?VOTER))))) CompulsorySuffrageLaw) |
Government.kif 1122-1136 | 对所有 ?POLITY， ?VOTER,， ， ?ELECTION,， ， ?VOTINGAGE， and 和 ?AGE
|
| (exists (?TIME) (and (instance ?TIME TimeInterval) (finishes ?TIME (WhenFn JesusOfNazareth)) (starts ?TIME (WhenFn TwelveApostles)) (forall (?MEM) (=> (holdsDuring ?TIME (member ?MEM TwelveApostles)) (holdsDuring ?TIME (friend ?MEM JesusOfNazareth)))))) |
Media.kif 1970-1978 | 有存在 时距 这样 那个 时距 是 时距 的 instance 和 那个 时距 finishes了才到 JesusOfNazareth 出现 的 time 和 那个 时距 starts了才到 TwelveApostles 出现 的 time 和 对所有 实体
|
| appearance as argument number 0 |
|
|
| (forall (?NUMBER) (equal (MeasureFn ?NUMBER OunceMass) (MeasureFn (DivisionFn ?NUMBER 16.0) PoundMass))) |
Mid-level-ontology.kif 14229-14232 | 对所有 实数 那个 实数 OunceMass equal 那个 实数 和 16.0 磅质量 |
| (forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1))) |
Merge.kif 4730-4731 | 对所有 整数 (那个 整数+2) equal (那个 整数 和 1) |
| (forall (?NUMBER) (equal (SuccessorFn ?NUMBER) (AdditionFn ?NUMBER 1))) |
Merge.kif 4714-4715 | 对所有 整数 (那个 整数+1) equal (那个 整数 和 1) |
| (forall (@ROW ?ITEM) (equal (ListLengthFn (ListFn @ROW ?ITEM)) (SuccessorFn (ListLengthFn (ListFn @ROW))))) |
Merge.kif 3032-3035 | 对所有 @ROW 和 另一个 实体 (@ROW 和 那个 另外 实体) 的长度 equal ((@ROW) 的长度+1) |
| (forall (@ROW ?ITEM) (equal (ListOrderFn (ListFn @ROW ?ITEM) (ListLengthFn (ListFn @ROW ?ITEM))) ?ITEM)) |
Merge.kif 3037-3041 | 对所有 @ROW 和 另一个 实体 (@ROW 和 那个 另外 实体) 的第 (@ROW 和 那个 另外 实体) 的长度 几个元素 equal 那个 另外 实体 |
| (forall (@ROW ?ITEM) (initialList (ListFn @ROW) (ListFn @ROW ?ITEM))) |
Merge.kif 3310-3311 | 对所有 @ROW 和 另一个 实体 (@ROW) %starts (@ROW 和 那个 另外 实体) |
|
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