(=>
(contraryAttribute @ROW)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Attribute))) |
Merge.kif 456-460 |
Assuming @ROW is the opposite of, it follows that: if Y is a member of (@ROW), then Y is an instance of attribute |
(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall (?ATTR1)
(=>
(instance ?ATTR1 ?CLASS)
(exists (?ATTR2)
(and
(inList ?ATTR2
(ListFn @ROW))
(equal ?ATTR1 ?ATTR2)))))) |
Merge.kif 501-509 |
If @ROW are all the attributes of Y, then For all Entity Z: if Z is an instance of Y, then there exists W such that W is a member of (@ROW) and equal Z and W |
(=>
(exhaustiveDecomposition @ROW)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class))) |
Merge.kif 550-554 |
Assuming @ROW is covered by @ROW, it follows that: if Y is a member of (@ROW), then Y is an instance of class |
(=>
(disjointDecomposition @ROW)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class))) |
Merge.kif 566-570 |
Assuming @ROW is disjointly decomposed into @ROW, it follows that: if Y is a member of (@ROW), then Y is an instance of class |
(=>
(exhaustiveDecomposition ?CLASS @ROW)
(forall (?OBJ)
(=>
(instance ?OBJ ?CLASS)
(exists (?ITEM)
(and
(inList ?ITEM
(ListFn @ROW))
(instance ?OBJ ?ITEM)))))) |
Merge.kif 3051-3059 |
If X is covered by @ROW, then For all Entity Z: if Z is an instance of X, then there exists W such that W is a member of (@ROW) and Z is an instance of W |
(=>
(disjointDecomposition ?CLASS @ROW)
(forall (?ITEM)
(=>
(inList ?ITEM
(ListFn @ROW))
(subclass ?ITEM ?CLASS)))) |
Merge.kif 3061-3066 |
If X is disjointly decomposed into @ROW, then For all Class Z: if Z is a member of (@ROW), then Z is a subclass of X |
(=>
(disjointDecomposition ?CLASS @ROW)
(forall (?ITEM1 ?ITEM2)
(=>
(and
(inList ?ITEM1
(ListFn @ROW))
(inList ?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2)))) |
Merge.kif 3068-3077 |
If X is disjointly decomposed into @ROW, then For all Classes Z and W: if Z is a member of (@ROW), W is a member of (@ROW), and equal Z and W, then Z is disjoint from W |
(=>
(equal
(GreatestCommonDivisorFn @ROW) ?NUMBER)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Number))) |
Merge.kif 4966-4971 |
Assuming equal the greatest common divisor of @ROW and Y, it follows that: if Z is a member of (@ROW), then Z is an instance of number |
(=>
(and
(equal
(GreatestCommonDivisorFn @ROW) ?NUMBER)
(not
(equal ?NUMBER 0)))
(forall (?ELEMENT)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER) 0)))) |
Merge.kif 4973-4984 |
If equal the greatest common divisor of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Z mod Y 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 4986-5000 |
If equal the greatest common divisor of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is greater than Y and W W is a member of (@ROW)equal W mod Z and 0 |
(=>
(equal
(LeastCommonMultipleFn @ROW) ?NUMBER)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Number))) |
Merge.kif 5051-5056 |
Assuming equal the least common multiple of @ROW and Y, it follows that: if Z is a member of (@ROW), then Z is an instance of number |
(=>
(and
(equal
(LeastCommonMultipleFn @ROW) ?NUMBER)
(not
(equal ?NUMBER 0)))
(forall (?ELEMENT)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 5058-5068 |
If equal the least common multiple of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Y mod Z 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 5070-5084 |
If equal the least common multiple of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is less than Y and W W is a member of (@ROW)equal Z mod W and 0 |
(=>
(average ?LIST ?AVERAGE)
(forall (?LISTITEM)
(=>
(inList ?LISTITEM ?LIST)
(instance ?LISTITEM RealNumber)))) |
Merge.kif 5492-5497 |
If X is an average of Y, then For all Entity Z: if Z is a member of Y, then Z is an instance of real number |
(=>
(and
(amount ?S ?CO
(MeasureFn ?N ?U))
(instance ?SI ?S)
(measure ?SI
(MeasureFn ?N2 ?U))
(part ?SI ?CO))
(exists (?L)
(and
(inList
(MeasureFn ?N2 ?U) ?L)
(equal ?L
(AmountsFn ?S ?CO ?U))
(equal ?N
(ListSumFn ?L))))) |
Merge.kif 7740-7755 |
If amount X, Y and Z W(s), V is an instance of X, the measure of V is U W(s), and V is a part of Y, then there exists T such that U W(s) is a member of T and equal T and Amounts fn X, Y and W and equal Z and the sum of T |
(=>
(and
(instance ?O Odometer)
(instance ?V Vehicle)
(part ?O ?V)
(instance ?T Translocation)
(instrument ?T ?V)
(path ?T ?P)
(distanceOnPath
(MeasureFn ?D ?U) ?P)
(instance ?U LengthMeasure))
(hasPurpose ?O
(exists (?M ?L ?DIST)
(and
(instance ?M Measuring)
(instrument ?M ?O)
(measurementReading ?O ?DIST)
(inList ?D ?L)
(holdsDuring
(WhenFn
(EndFn ?M))
(and
(equal ?DIST
(MeasureFn
(ListSumFn ?L) ?U))
(not
(attribute ?O ResetMeasuringDevice)))))))) |
Cars.kif 2824-2850 |
If All of the following hold: (1) X is an instance of odometer (2) Y is an instance of vehicle (3) X is a part of Y (4) Z is an instance of translocation (5) Y is an instrument for Z (6) W is path along which Z occurs (7) the distance of W is V U(s) (8) U is an instance of length measure, then X has the purpose there exist T, S and R such that T is an instance of measuring and X is an instrument for T and R is a measurement reading of X and V is a member of S and equal R and the sum of S U(s) and reset measuring device is not an attribute of X holds during the time of existence of the end of T |
(=>
(and
(instance ?X OrderingParts)
(patient ?X ?P))
(hasPurpose ?X
(exists (?L)
(and
(instance ?L List)
(inList ?P ?L))))) |
Economy.kif 2096-2104 |
If X is an instance of Ordering parts and Y is a patient of X, then X has the purpose there exists Z such that Z is an instance of list and Y is a member of Z |
(=>
(instance ?SVC ShuttleService)
(exists (?LIST ?VEHICLE ?AGENT)
(and
(agent ?SVC ?AGENT)
(possesses ?AGENT ?VEHICLE)
(instance ?VEHICLE Automobile)
(instance ?LIST List)
(forall (?X)
(=>
(inList ?X ?LIST)
(and
(instance ?X PostalPlace)
(exists (?TRANSPORT)
(and
(instance ?TRANSPORT Transportation)
(agent ?TRANSPORT ?AGENT)
(instrument ?TRANSPORT ?VEHICLE)
(destination ?TRANSPORT ?X))))))))) |
Hotel.kif 2053-2071 |
If X is an instance of shuttle, then All of the following hold: (1) there exist Y, Z (2) W such that W is an agent of X (3) W possesses Z (4) Z is an instance of automobile (5) Y is an instance of list (6) V V is a member of YV is an instance of postal place (7) there exists U such that U is an instance of transportation (8) W is an agent of U (9) Z is an instrument for U (10) U ends up at V |
(=>
(and
(instance ?OBJ DigitalDataStorageDevice)
(part ?PART ?OBJ)
(instance ?PART DigitalData))
(exists (?SCHEME ?LIST ?NUM)
(and
(codeMapping ?SCHEME ?PART ?NUM)
(represents ?LIST ?SCHEME)
(=>
(inList ?NUM ?LIST)
(instance ?NUM BinaryNumber))))) |
Media.kif 799-810 |
If X is an instance of digital data storage device, Y is a part of X, and Y is an instance of digital data, then there exist Z, W, V such that Y in Z denotes V, W expresses Z, and V is a member of WV is an instance of binary number |
(=>
(instance ?L Album)
(forall (?X)
(=>
(inList ?X ?L)
(instance ?X Recording)))) |
Music.kif 53-58 |
If X is an instance of album, then For all Entity Y: if Y is a member of X, then Y is an instance of recording |
(=>
(albumArtist ?A ?P)
(exists (?R ?M)
(and
(instance ?R Recording)
(inList ?R ?A)
(record ?R ?M)
(agent ?M ?P)))) |
Music.kif 280-287 |
If X is a performer on Y, then there exist Z, W such that Z is an instance of recording, Z is a member of Y, Z is a record of W, and X is an agent of W |
(=>
(and
(equal ?D
(AlbumCopiesFn ?A ?DS))
(instance ?X ?D))
(forall (?S)
(=>
(inList ?S ?A)
(exists (?C)
(and
(copy ?C ?S)
(dataStored ?C ?X)))))) |
Music.kif 938-948 |
If equal X and the set of copies on Y of Z and W is an instance of X, then For all Object V: if V is a member of Z, then there exists U such that U is a copy of V and W is stored on U |
(=>
(instance ?X MusicChart)
(exists (?P ?OBJ)
(causesProposition
(and
(instance ?P Selecting)
(patient ?P ?X))
(inList ?OBJ ?X)))) |
Music.kif 1127-1134 |
If X is an instance of music charts, then there exist Y, Z such that Z is a member of X is a causes proposition of Y is an instance of selecting, and X is a patient of Y |
(=>
(instance ?X SinglesChart)
(exists (?MR)
(and
(instance ?MR MusicRecording)
(inList ?MR ?X)))) |
Music.kif 1141-1146 |
If X is an instance of singles chart, then there exists Y such that Y is an instance of music recording and Y is a member of X |
(=>
(instance ?X AlbumChart)
(exists (?A)
(and
(instance ?A Album)
(inList ?A ?X)))) |
Music.kif 1153-1158 |
If X is an instance of album chart, then there exists Y such that Y is an instance of album and Y is a member of X |
|
| Display limited to 25 items. Show next 25 |
|
| Display limited to 25 items. Show next 25 |
Medicine