forall
|
|
Sigma KEE - forall
appearance as argument number 2
|
|
antecedent
|
|
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 the male life expectancy at birth of a geopolitical area and the year is equal to 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 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 the female life expectancy at birth of a geopolitical area and the year is equal to 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 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 the life expectancy at birth of a geopolitical area and the year is equal to 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 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 length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all another positive integer and the positive integer is equal to length of the other list and the real number is equal to 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 7758-7766 |
An object is larger than another object if and only if for all a real number, another real number and an unit of measure |
(<=>
(subCollection ?COLL1 ?COLL2)
(forall (?MEMBER)
(=>
(member ?MEMBER ?COLL1)
(member ?MEMBER ?COLL2)))) |
Merge.kif 1297-1302 |
A collection is a proper sub-collection of another collection if and only if for all a physical |
(=>
(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 4990-4998 |
|
(=>
(and
(attribute ?OBJ Monochromatic)
(superficialPart ?PART ?OBJ)
(attribute ?PART ?COLOR)
(instance ?COLOR PrimaryColor))
(forall (?ELEMENT)
(=>
(superficialPart ?ELEMENT ?OBJ)
(attribute ?ELEMENT ?COLOR)))) |
Merge.kif 17688-17697 |
|
(=>
(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 1132-1152 |
|
(=>
(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 4861-4872 |
|
(=>
(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 4874-4888 |
|
(=>
(and
(equal
(LeastCommonMultipleFn @ROW) ?NUMBER)
(not
(equal ?NUMBER 0)))
(forall (?ELEMENT)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 4946-4956 |
|
(=>
(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 4958-4972 |
|
(=>
(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 9894-9901 |
|
(=>
(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 12930-12941 |
|
(=>
(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 1241-1248 |
For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING 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 923-931 |
For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER 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 1092-1103 |
For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE 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 1160-1174 |
For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE 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 1970-1978 |
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 |
|