forall - Sigma Knowledge base Browser

antecedent

(<=> (holdsDuring ?T (and (instance ?PERSON Human) (forall (?ORG) (not (employs ?ORG ?PERSON))))) (holdsDuring ?T (attribute ?PERSON Unemployed)))	Merge.kif 17451-17459	An entity is an instance of human and for all another entity the other entity doesn't employ the entity holds during a time position if and only if unemployed person is an attribute of the entity holds during the time position
(=> (and (climateTypeInArea ?AREA ColdClimateZone) (forall (?MO) (and (instance ?MO Month) (averageTemperatureForPeriod ?AREA ?MO (MeasureFn ?TEMP CelsiusDegree))))) (greaterThan 10.0 ?TEMP))	Geography.kif 2983-2991	If cold climate zone is a climate type in area of a geographic area and for all a time interval the time interval is an instance of month and the geographic area average temperature for period the time interval for a real number celsius degree(s), then 10.0 is greater than the real number
(=> (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 6043-6056	If equal the value of a graph path and a real number and a graph arc is a part of the graph path and another graph arc is a part of the graph path and the value of the graph arc is another real number and the value of the other graph arc is a third real number and for all a graph element if the graph element is a part of the graph path, then equal the graph element and the graph arc or equal the graph element and the other graph arc , then equal the value of the graph path and (the other real number and the third real number)
(=> (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 6029-6041	If equal the value of a graph path and a real number and another graph path is a subgraph of the graph path and a graph arc is a part of the graph path and the value of the graph arc is another real number and for all a graph element if the graph element is a part of the graph path, then the graph element is a part of the other graph path or equal the graph element and the graph arc , then equal the real number and (the value of the other graph path and the other real number)
(=> (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 3201-3214	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of auctioning , then there exist a symbolic string and an entity_PURCHASE_AMOUNT such that the total of values in the class described by the symbolic string is the entity_PURCHASE_AMOUNT and equal the total purchase price of the collection and the entity_PURCHASE_AMOUNT
(=> (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 2886-2902	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of financial transaction , then there exist a symbolic string and an entity such that equal the number of instances in the class described by the symbolic string and number of items purchased in the collection
(=> (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 2921-2939	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of web listing , then there exist a symbolic string, an entity,, , another entity and the symbolic string such that equal the number of instances in the class described by the symbolic string and number of bids in the collection
(=> (and (instance ?COLL Collection) (forall (?MEMBER) (=> (member ?MEMBER ?COLL) (instance ?MEMBER WebListing)))) (exists (?LISTING ?SITE ?ITEM) (equal (DivisionFn (CardinalityFn (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	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of web listing , then there exist a symbolic string, an entity and another entity such that equal the number of instances in the class described by the symbolic string and the number of instances in the collection and number of bids in the collection
(=> (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	If a collection is an instance of collection and a web site is an instance of web site and an agent is an instance of agent and a web listing is an instance of web listing and a time point is an instance of time point and the agent sells the web listing and the web listing is not a member of the collection and for all a physical and another physical if the physical is an instance of web listing and the physical is a member of items for sale by the agent at the web site and the time point is a part of the time of existence of the physical and equal the physical and the web listing, then the physical is a member of the collection and if the other physical is a member of the collection, then the time point is a part of the time of existence of the physical and the other physical is an instance of web listing , then equal things for sale by the agent not listed in the web listing at the web site during the time point and the collection
(=> (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 2955-2982	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of buying and there exists an object such that the object is an instance of geopolitical area and for all an agent and a process if the agent is an instance of agent and the process is an instance of buying and the process is a member of the collection and the agent is an agent of the process, then the agent is located at the object , then there exist a symbolic string, an entity and another entity_PURCHASE_AMOUNT such that the total of values in the class described by the symbolic string is the other entity_PURCHASE_AMOUNT and equal the value of the collection and the other entity_PURCHASE_AMOUNT
(=> (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 2998-3025	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of selling and there exists an object such that the object is an instance of geopolitical area and for all an agent and a process if the agent is an instance of agent and the process is an instance of buying and the process is a member of the collection and the agent is an agent of the process, then the agent is located at the object , then there exist a symbolic string, an entity and another entity_SALE_AMOUNT such that the total of values in the class described by the symbolic string is the other entity_SALE_AMOUNT and equal the value of the collection and the other entity_SALE_AMOUNT
(=> (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 8507-8521	If an object is an instance of auditorium seat and the object is a part of another object and a third object is a part of the other object and the other object is an instance of auditorium and the third object is an instance of performance stage and a fourth object is located at the object and the fourth object is an instance of human and a kind of process is a subclass of seeing and for all another process if the other process is an instance of a kind of process, then the third object is a patient of the other process , then the fourth object is capable of doing the kind of process as a agent
(=> (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 4240-4266	If a human is an instance of human and a collection is an instance of collection and for all an experimenting and a physical if there exists a kind of process such that the experimenting is an instance of experimenting and the physical is an instance of process and the physical is a member of events in the experimenting and the physical is an instance of a kind of process and the human is capable of doing the kind of process as a experiencer, then the physical is a member of the collection and if another physical is a member of the collection, then the other physical is an instance of process and there exist another experimenting and the other physicalESS such that the other experimenting is an instance of experimenting and the other physical is a member of events in the other experimenting and the other physical is an instance of the other physicalESS and the human is capable of doing the other physicalESS as a experiencer , then equal all the processes the human is qualified for and the collection
(=> (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 4174-4189	If a human is an instance of human and a collection is an instance of collection and for all a web page, a process and an experimenting if the web page is an instance of web page and the process is an instance of accessing web page and the experimenting is an instance of experimenting and the human is an agent of the process and the web page is a patient of the process and the web page is the object of study of the experimenting, then the process is a member of the collection , then equal the collection and all the treated web page views from the human
(=> (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 3332-3355	If a collection is an instance of collection and a corpuscular object is an instance of hyperlink and for all a physical the physical is a member of another collection and the physical is an instance of accessing web page and the other collection is a component of the corpuscular object, then there exists a third collection such that the third collection is an instance of collection and for all a process if the process is an instance of requesting hyperlink and the corpuscular object is a patient of the process, then the process is a member of the third collection and equal the rate of clicking through the corpuscular object in the collection and the number of instances in the third collection and the number of instances in the collection
(=> (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 3667-3703	If a collection is an instance of collection and another collection is an instance of collection and the other collection is a proper sub-collection of the collection and for all a physical if the physical is a member of the collection, then the physical is an instance of accessing web page and for all a process, an agent,, , another process,, , the process and an object if the agent is an instance of human and the process is an instance of buying and the other process is an instance of accessing web page and the object is an instance of web page and the other process is a member of the collection and the other process ends up at the object and the agent is an agent of the process and the agent is an agent of the other process and the time of existence of the process takes place during the time of existence of the other process and the object is an instrument for the process, then the process is a member of the other collection , then there exist a time interval, an entity_IN_INTERVAL and another entity_IN_INTERVAL such that equal purchases made in the collection during the time interval and the number of instances in the class described by the entity_IN_INTERVAL and the number of instances in the class described by the other entity_IN_INTERVAL

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	A year is an instance of the year the yearEAR and equal the male life expectancy at birth of a geopolitical area and the year and a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and equal the other integer and the number of instances in the class described by the symbolic string and the real number is an average of the list
(<=> (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	A year is an instance of the year an integer and equal the female life expectancy at birth of a geopolitical area and the year and a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and equal the other integer and the number of instances in the class described by the symbolic string and the real number is an average of the list
(<=> (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	A year is an instance of the year an integer and equal the life expectancy at birth of a geopolitical area and the year and a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and equal the other integer and the number of instances in the class described by the symbolic string and the real number is an average of the list
(<=> (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	A real number is an average of a list if and only if there exist another list and a positive integer such that equal length of the other list and length of the list and equal 1th element of the other list and 1th element of the list and for all another positive integer if the other positive integer is a member of the other list, then there exist another real number, the other real numberMINUSONE,, , a third positive integer and a fourth positive integer such that the other real number is greater than 1 and the other real number is less than or equal to length of the other list and equal the other positive integerth element of the other list and the other real number and the third positive integer is a member of the list and equal the other real number and the third positive integerth element of the list and the fourth positive integer is a member of the other list and equal the other real numberMINUSONE and (the other real number and 1) and equal the other real numberMINUSONE and the fourth positive integerth element of the other list and equal the other positive integer and (the third positive integer and the fourth positive integer) and equal the positive integer and length of the other list and equal the real number and the positive integerth element of the other list and the positive integer
(<=> (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 7868-7876	An object is larger than another object if and only if for all a real number, another real number and an unit of measure if the measure of the object is the real number the unit of measure(s) and the measure of the other object is the other real number the unit of measure(s) and the unit of measure is an instance of unit of length, then the real number is greater than the other real number
(<=> (subCollection ?COLL1 ?COLL2) (forall (?MEMBER) (=> (member ?MEMBER ?COLL1) (member ?MEMBER ?COLL2))))	Merge.kif 1332-1337	A collection is a proper sub-collection of another collection if and only if for all a physical if the physical is a member of the collection, then the physical is a member of the other collection
(=> (allRoomsPhysicalAmenity ?INV ?OBJ) (forall (?X) (=> (memberType ?INV ?X) (roomAmenity ?X ?OBJ))))	Hotel.kif 171-176	If all rooms in a room inventory have a kind of physical, then for all a kind of hotel unit if a kind of hotel unit is a member type of the room inventory, then a kind of physical is an amenity in the kind of hotel unit
(=> (allRoomsPolicy ?INV ?POLICY) (forall (?X) (=> (memberType ?INV ?X) (roomPolicy ?X ?POLICY))))	Hotel.kif 233-238	If all rooms in a room inventory have policy a policy, then for all a kind of hotel unit if a kind of hotel unit is a member type of the room inventory, then the policy is a policy that applies to the kind of hotel unit
(=> (allRoomsServiceAmenity ?INV ?OBJ) (forall (?X) (=> (memberType ?INV ?X) (roomAmenity ?X ?OBJ))))	Hotel.kif 218-223	If all rooms in a room inventory have service a kind of physical, then for all a kind of hotel unit if a kind of hotel unit is a member type of the room inventory, then a kind of physical is an amenity in the kind of hotel unit
(=> (and (attribute ?OBJ Monochromatic) (superficialPart ?PART ?OBJ) (attribute ?PART ?COLOR) (instance ?COLOR PrimaryColor)) (forall (?ELEMENT) (=> (superficialPart ?ELEMENT ?OBJ) (attribute ?ELEMENT ?COLOR))))	Merge.kif 17893-17902	If monochromatic is an attribute of an object and another object is a superficial part of the object and an attribute is an attribute of the other object and the attribute is an instance of primary color, then for all a third object if the third object is a superficial part of the object, then the attribute is an attribute of the third object
(=> (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	If a human is a citizen of a nation and universal suffrage law is a sub-proposition of the regional law of the nation, then the regional law of the nation allows the human to perform task of the type for all an entity, another entity and a third entity if the human is a citizen of the nation and the entity year duration(s) is a suffrage age minimum of the nation and the age of the human is the other entity year duration(s) and the other entity is greater than or equal to the entity and the third entity is an instance of the election of the nation, then there exists a fourth entity such that the fourth entity is an instance of the voting of the third entity and the human is an agent of the fourth entity
(=> (and (element ?X (PropertyFn ?HOTEL)) (instance ?X RoomInventory)) (forall (?Y) (=> (member ?Y ?X) (element ?Y (PropertyFn ?HOTEL)))))	Hotel.kif 147-154	If a collection is an element of belongings of an agent and the collection is an instance of room inventory, then for all a physical if the physical is a member of the collection, then the physical is an element of belongings of the agent
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0))))	Merge.kif 4914-4925	If equal the greatest common divisor of @ROW and an integer and equal the integer and 0, then for all another integer if the other integer is a member of (@ROW), then equal the other integer mod the integer and 0
(=> (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 4927-4941	If equal the greatest common divisor of @ROW and an integer and equal the integer and 0, then there doesn't exist another integer such that the other integer is greater than the integer and for all a third integer if the third integer is a member of (@ROW), then equal the third integer mod the other integer and 0
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0))))	Merge.kif 4999-5009	If equal the least common multiple of @ROW and an integer and equal the integer and 0, then for all another integer if the other integer is a member of (@ROW), then equal the integer mod the other integer and 0
(=> (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 5011-5025	If equal the least common multiple of @ROW and an integer and equal the integer and 0, then there doesn't exist another integer such that the other integer is less than the integer and for all a third integer if the third integer is a member of (@ROW), then equal the other integer mod the third integer and 0
(=> (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 938-948	If equal a kind of data storage device and the set of copies on a kind of data storage deviceS of an album and a third data storage device is an instance of the kind of data storage device, then for all an object if the object is a member of the album, then there exists a content bearing object such that the content bearing object is a copy of the object and the content bearing object is stored on the third data storage device
(=> (and (hole ?HOLE1 ?OBJ) (hole ?HOLE2 ?OBJ)) (forall (?HOLE3) (=> (part ?HOLE3 (MereologicalSumFn ?HOLE1 ?HOLE2)) (hole ?HOLE3 ?OBJ))))	Merge.kif 10054-10061	If a hole is a hole in a self connected object and another hole is a hole in the self connected object, then for all a third hole if the third hole is a part of the union of the parts of the hole and the other hole, then the third hole is a hole in the self connected object
(=> (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	If an agent is an instance of agent and a web site is an instance of web site, then there exists a collection such that the collection is an instance of collection and for all a web listing if the web listing is an instance of web listing and the web listing is hosted on the web site and the agent sells the web listing, then the web listing is a member of the collection and equal items for sale by the agent at the web site and the collection
(=> (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 1013-1027	If a process is an instance of grinding and an entity is a patient of the process and the entity is an instance of corpuscular object, then there exists another entity such that the other entity is a result of the process and the other entity is an instance of collection and for all a third entity if the third entity is a member of the other entity, then the third entity is a part of the entity holds during the end of the time of existence of the process
(=> (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 3375-3407	If a time interval is an instance of time interval and a web site is an instance of web site, then there exists a collection such that the collection is an instance of collection and for all an agent if the agent is a member of the collection, then there exists another time interval such that the agent is an instance of agent and the other time interval is an instance of buying and the agent is an agent of the other time interval and the web site is an instrument for the other time interval and the other time interval takes place during the time interval and there doesn't exist the time interval_BEFORE such that the time interval_BEFORE is an instance of time interval and the time interval_BEFORE happens earlier than the time interval and there exists the other time interval_BEFORE such that the other time interval_BEFORE is an instance of buying and the agent is an agent of the other time interval_BEFORE and the web site is an instrument for the other time interval_BEFORE and the other time interval_BEFORE takes place during the time interval holds during the time interval_BEFORE and equal new buyers at the web site during the time interval and the collection
(=> (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 3427-3454	If a time interval is an instance of time interval and a web site is an instance of web site, then there exists a collection such that the collection is an instance of collection and for all a physical if the physical is an instance of human and there doesn't exist the time interval_BEFORE such that the time interval_BEFORE is an instance of time interval and the time interval_BEFORE happens earlier than the time interval and the physical is a registered user of the web site holds during the time interval_BEFORE and there exists the time interval_DURING such that the time interval_DURING is an instance of time interval and the time interval_DURING takes place during the time interval and the physical is a registered user of the web site holds during the time interval, then the physical is a member of the collection and equal the collection and new registrations at the web site during the time interval
(=> (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 3474-3506	If a time interval is an instance of time interval and a web site is an instance of web site, then there exists a collection such that the collection is an instance of collection and for all an agent if the agent is a member of the collection, then there exists another time interval such that the agent is an instance of agent and the other time interval is an instance of selling and the agent is an agent of the other time interval and the web site is an instrument for the other time interval and the other time interval takes place during the time interval and there doesn't exist the time interval_BEFORE such that the time interval_BEFORE is an instance of time interval and the time interval_BEFORE happens earlier than the time interval and there exists the other time interval_BEFORE such that the other time interval_BEFORE is an instance of selling and the agent is an agent of the other time interval_BEFORE and the web site is an instrument for the other time interval_BEFORE and the other time interval_BEFORE takes place during the time interval holds during the time interval_BEFORE and equal new sellers at the web site during the time interval and the collection
(=> (and (instance ?KEEP Keeping) (patient ?KEEP ?OBJ)) (exists (?PLACE) (forall (?TIME) (=> (temporalPart ?TIME (WhenFn ?KEEP)) (holdsDuring ?TIME (located ?OBJ ?PLACE))))))	Merge.kif 12362-12370	If a process is an instance of keeping and an entity is a patient of the process, then there exists another entity such that for all a time position if the time position is a part of the time of existence of the process, then the entity is located at the other entity holds during the time position
(=> (and (instance ?POINT1 TimePoint) (instance ?POINT2 TimePoint) (instance ?INTERVAL TimeInterval) (equal (TimeIntervalFn ?POINT1 ?POINT2) ?INTERVAL)) (forall (?POINT) (<=> (temporallyBetweenOrEqual ?POINT1 ?POINT ?POINT2) (temporalPart ?POINT ?INTERVAL))))	Merge.kif 8565-8574	If a time point is an instance of time point and another time point is an instance of time point and a time interval is an instance of time interval and equal interval between the time point and the other time point and the time interval, then for all a third time point the third time point is between or at the time point and the other time point if and only if the third time point is a part of the time interval

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	For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING if ?ELECTION is an instance of the election of ?AGENT and ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING, then male is an attribute of ?VOTER contains information exclusive male suffrage
(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	For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER if ?COUNTRY is an instance of nation and ?ELECTION is an instance of the election of ?COUNTRY and ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING, then ?VOTER is a citizen of ?COUNTRY contains information voter citizenship requirement
(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	For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE if ?AGENT is a citizen of ?POLITY and ?VOTINGAGE year duration(s) is a suffrage age minimum of ?POLITY and the age of ?AGENT is ?AGE year duration(s) and ?AGE is greater than or equal to ?VOTINGAGE and ?ELECTION is an instance of the election of ?POLITY, then ?AGENT is capable of doing the voting of ?ELECTION as a agent contains information universal suffrage law
(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	For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE if ?VOTER is a citizen of ?POLITY and ?VOTINGAGE year duration(s) is a suffrage age minimum of ?POLITY and the age of ?VOTER is ?AGE year duration(s) and ?AGE is greater than or equal to ?VOTINGAGE and ?ELECTION is an instance of the election of ?POLITY, then there exists ?VOTING such that ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING contains information compulsory suffrage law
(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 1972-1980	There exists a time interval such that the time interval is an instance of time interval and the time interval finishes the time of existence of Jesus of Nazareth and the time interval starts the time of existence of Twelve apostles and for all an entity if the entity is a member of Twelve apostles holds during the time interval, then Jesus of Nazareth is a friend of the entity holds during the time interval

appearance as argument number 0

(forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1)))	Merge.kif 4789-4790	For all an integer equal (the integer+2) and (the integer and 1)
(forall (?NUMBER) (equal (SuccessorFn ?NUMBER) (AdditionFn ?NUMBER 1)))	Merge.kif 4773-4774	For all an integer equal (the integer+1) and (the integer and 1)
(forall (@ROW ?ITEM) (equal (ListLengthFn (ListFn @ROW ?ITEM)) (SuccessorFn (ListLengthFn (ListFn @ROW)))))	Merge.kif 3075-3078	For all @ROW and another entity equal length of (@ROW and the other entity) and (length of (@ROW)+1)
(forall (@ROW ?ITEM) (equal (ListOrderFn (ListFn @ROW ?ITEM) (ListLengthFn (ListFn @ROW ?ITEM))) ?ITEM))	Merge.kif 3080-3084	For all @ROW and another entity equal length of (@ROW and the other entity)th element of (@ROW and the other entity) and the other entity
(forall (@ROW ?ITEM) (initialList (ListFn @ROW) (ListFn @ROW ?ITEM)))	Merge.kif 3355-3356	For all @ROW and another entity (@ROW) starts (@ROW and the other entity)

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

KB Term:			Term intersection

English Word: