(<=>
(and
(equal ?LIST3
(ListConcatenateFn ?LIST1 ?LIST2))
(not
(equal ?LIST1 NullList))
(not
(equal ?LIST2 NullList)))
(forall (?NUMBER1 ?NUMBER2)
(=>
(and
(lessThanOrEqualTo ?NUMBER1
(ListLengthFn ?LIST1))
(lessThanOrEqualTo ?NUMBER2
(ListLengthFn ?LIST2))
(instance ?NUMBER1 PositiveInteger)
(instance ?NUMBER2 PositiveInteger))
(and
(equal
(ListOrderFn ?LIST3 ?NUMBER1)
(ListOrderFn ?LIST1 ?NUMBER1))
(equal
(ListOrderFn ?LIST3
(AdditionFn
(ListLengthFn ?LIST1) ?NUMBER2))
(ListOrderFn ?LIST2 ?NUMBER2)))))) 
Merge.kif 29722988 
A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer 
(<=>
(and
(instance ?REL TotalValuedRelation)
(instance ?REL Predicate))
(exists (?VALENCE)
(and
(instance ?REL Relation)
(valence ?REL ?VALENCE)
(=>
(forall (?NUMBER ?ELEMENT ?CLASS)
(=>
(and
(lessThan ?NUMBER ?VALENCE)
(domain ?REL ?NUMBER ?CLASS)
(equal ?ELEMENT
(ListOrderFn
(ListFn @ROW) ?NUMBER)))
(instance ?ELEMENT ?CLASS)))
(exists (?ITEM)
(?REL @ROW ?ITEM)))))) 
Merge.kif 21112128 
A relation is an instance of total valued relation and the relation is an instance of predicate if and only if there exists a positive integer such that the relation is an instance of relation and the relation %&has the positive integer argument(s) and 
(<=>
(average ?LIST1 ?AVERAGE)
(exists (?LIST2)
(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 285306 
A real number is an average of a list if and only if there exists another list 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 a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer 
(<=>
(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 411442 
The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
(<=>
(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 323353 
The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
(<=>
(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 367398 
The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
(<=>
(instance ?OBJ SelfConnectedObject)
(forall (?PART1 ?PART2)
(=>
(equal ?OBJ
(MereologicalSumFn ?PART1 ?PART2))
(connected ?PART1 ?PART2)))) 
Merge.kif 89578962 
An object is an instance of self connected object if and only if for all another object and a third object 
(<=>
(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 73587366 
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 11911196 
A collection is a proper subcollection of another collection if and only if for all an object 
(<=>
(subset ?SUBSET ?SET)
(forall (?ELEMENT)
(=>
(element ?ELEMENT ?SUBSET)
(element ?ELEMENT ?SET)))) 
Merge.kif 51155120 
A set is a subset of another set if and only if for all an entity 
(=>
(allRoomsPhysicalAmenity ?INV ?OBJ)
(forall (?X)
(=>
(memberType ?INV ?X)
(roomAmenity ?X ?OBJ)))) 
Hotel.kif 166171 

(=>
(allRoomsPolicy ?INV ?POLICY)
(forall (?X)
(=>
(memberType ?INV ?X)
(roomPolicy ?X ?POLICY)))) 
Hotel.kif 228233 

(=>
(allRoomsServiceAmenity ?INV ?OBJ)
(forall (?X)
(=>
(memberType ?INV ?X)
(roomAmenity ?X ?OBJ)))) 
Hotel.kif 213218 

(=>
(and
(attribute ?OBJ ?SPHERE)
(instance ?SPHERE Sphere))
(exists (?CENTER ?DIST)
(forall (?PT)
(=>
(pointOfFigure ?PT ?OBJ)
(geometricDistance ?PT ?CENTER ?DIST))))) 
Midlevelontology.kif 52935301 

(=>
(and
(attribute ?OBJ Monochromatic)
(superficialPart ?PART ?OBJ)
(attribute ?PART ?COLOR)
(instance ?COLOR PrimaryColor))
(forall (?ELEMENT)
(=>
(superficialPart ?ELEMENT ?OBJ)
(attribute ?ELEMENT ?COLOR)))) 
Merge.kif 1646416473 

(=>
(and
(attribute ?X DutyFree)
(instance ?X Store))
(forall (?OBJ)
(=>
(and
(instance ?SELL Selling)
(patient ?SELL ?OBJ)
(located ?SELL ?X)
(instance ?OBJ Product))
(attribute ?OBJ DutyFree)))) 
Hotel.kif 14271438 

(=>
(and
(citizen ?AGENT ?POLITY)
(subProposition UniversalSuffrageLaw
(RegionalLawFn ?POLITY)))
(confersRight
(forall (?VOTINGAGE ?AGE ?ELECTION)
(=>
(and
(citizen ?AGENT ?POLITY)
(suffrageAgeMinimum ?POLITY ?VOTINGAGE)
(age ?AGENT ?AGE)
(greaterThanOrEqualTo ?AGE ?VOTINGAGE)
(instance ?ELECTION
(ElectionFn ?POLITY)))
(exists (?VOTING)
(and
(instance ?VOTING
(VotingFn ?ELECTION))
(agent ?VOTING ?AGENT)))))
(RegionalLawFn ?POLITY) ?AGENT)) 
Government.kif 10961114 

(=>
(and
(courseWRTMagneticNorth ?OBJ1 ?OBJ2 ?MAGDEGREE)
(partlyLocated ?OBJ1 ?AREA)
(partlyLocated ?OBJ2 ?AREA)
(magneticVariation ?AREA ?DEGREE ?DIRECTION))
(exists (?DIFFDEGREE ?TRUEDEGREE)
(and
(=>
(and
(equal ?DIRECTION East)
(equal ?DIFFDEGREE
(AdditionFn ?MAGDEGREE ?DEGREE)))
(courseWRTTrueNorth ?OBJ1 ?OBJ2 ?TRUEDEGREE))
(=>
(and
(equal ?DIRECTION West)
(equal ?DIFFDEGREE
(SubtractionFn ?MAGDEGREE ?DEGREE)))
(courseWRTTrueNorth ?OBJ1 ?OBJ2 ?TRUEDEGREE))))) 
Geography.kif 36323649 

(=>
(and
(element ?X
(PropertyFn ?HOTEL))
(instance ?X RoomInventory))
(forall (?Y)
(=>
(member ?Y ?X)
(element ?Y
(PropertyFn ?HOTEL))))) 
Hotel.kif 142149 

(=>
(and
(equal
(MaximalWeightedPathFn ?NODE1 ?NODE2) ?PATH)
(equal
(PathWeightFn ?PATH) ?NUMBER1))
(forall (?PATH2)
(=>
(and
(instance ?PATH2
(GraphPathFn ?NODE1 ?NODE2))
(equal
(PathWeightFn ?PATH2) ?NUMBER2))
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1)))) 
Merge.kif 57275736 

(=>
(and
(equal
(MinimalWeightedPathFn ?NODE1 ?NODE2) ?PATH)
(equal
(PathWeightFn ?PATH) ?NUMBER1))
(forall (?PATH2)
(=>
(and
(instance ?PATH2
(GraphPathFn ?NODE1 ?NODE2))
(equal
(PathWeightFn ?PATH2) ?NUMBER2))
(greaterThanOrEqualTo ?NUMBER2 ?NUMBER1)))) 
Merge.kif 57025711 

(=>
(and
(equal ?D
(AlbumCopiesFn ?A ?DS))
(instance ?X ?D))
(forall (?S)
(=>
(inList ?S ?A)
(exists (?C)
(and
(copy ?C ?S)
(stored ?C ?D)))))) 
Music.kif 930940 

(=>
(and
(exactCardinality ?REL ?ARG ?COUNT)
(instance ?REL Predicate))
(exists (?S)
(and
(instance ?S SetOrClass)
(=>
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG)))
(and
(instance ?EL ?S)
(equal
(CardinalityFn ?S) ?COUNT)))))) 
Media.kif 21342147 

(=>
(and
(hole ?HOLE1 ?OBJ)
(hole ?HOLE2 ?OBJ))
(forall (?HOLE3)
(=>
(part ?HOLE3
(MereologicalSumFn ?HOLE1 ?HOLE2))
(hole ?HOLE3 ?OBJ)))) 
Merge.kif 93069313 

(=>
(and
(instance ?AGENT Agent)
(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 11851201 


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 