(=>
(and
(equal ?LIST1 ?LIST2)
(equal ?LIST1
(ListFn @ROW1))
(equal ?LIST2
(ListFn @ROW2)))
(equal
(ListOrderFn
(ListFn @ROW1) ?NUMBER)
(ListOrderFn
(ListFn @ROW2) ?NUMBER))) |
Merge.kif 289-296 |
If equal X and Y, equal X and (@ROW1), and equal Y and (@ROW2), then equal V element of (@ROW1) and V element of (@ROW2) |
(=>
(exhaustiveAttribute ?ATTRCLASS @ROW)
(not
(exists (?EL)
(and
(instance ?EL ?ATTRCLASS)
(not
(exists (?ATTR ?NUMBER)
(and
(equal ?EL ?ATTR)
(equal ?ATTR
(ListOrderFn
(ListFn @ROW) ?NUMBER))))))))) |
Merge.kif 511-523 |
If @ROW are all the attributes of Y, then there doesn't exist Z such that Z is an instance of Y and there don't exist W and V such that equal Z and W and equal W and U element of (@ROW) |
(=>
(instance ?LIST UniqueList)
(forall (?NUMBER1 ?NUMBER2)
(=>
(equal
(ListOrderFn ?LIST ?NUMBER1)
(ListOrderFn ?LIST ?NUMBER2))
(equal ?NUMBER1 ?NUMBER2)))) |
Merge.kif 3021-3026 |
If X is an instance of unique list, then For all PositiveIntegers Y and Z: if equal W element of X and V element of X, then equal Y and Z |
(=>
(and
(domain ?REL ?NUMBER ?CLASS)
(instance ?REL Predicate)
(?REL @ROW))
(instance
(ListOrderFn
(ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 3109-3114 |
If the number X argument of Y is an instance of Z, Y is an instance of predicate, and Y @ROW, then V element of (@ROW) is an instance of Z |
(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS)
(instance ?REL Predicate)
(?REL @ROW))
(subclass
(ListOrderFn
(ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 3116-3121 |
If the number X argument of Y is a subclass of Z, Y is an instance of predicate, and Y @ROW, then V element of (@ROW) is a subclass of Z |
(=>
(and
(equal ?LIST3
(ListConcatenateFn ?LIST1 ?LIST2))
(not
(equal ?LIST1 NullList))
(not
(equal ?LIST2 NullList))
(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 3194-3213 |
If All of the following hold: (1) equal X, the list composed of Y, and Z (2) equal Y and null list (3) equal Z and null list (4) W is less than or equal to length of Y (5) V is less than or equal to length of Z (6) W is an instance of positive integer (7) V is an instance of positive integer, then equal U element of X and U element of Y and equal (length of Y and V)th element of X and T element of Z |
(=>
(inList ?ITEM ?LIST)
(exists (?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER) ?ITEM))) |
Merge.kif 3224-3227 |
If X is a member of Y, then there exists Z such that equal W element of Y and X |
(=>
(and
(equal ?R
(SubListFn ?S ?E ?L))
(equal
(SubtractionFn ?E ?S) 1))
(equal ?R
(ListFn
(ListOrderFn ?L ?S)))) |
Merge.kif 3290-3299 |
If equal X and the sub-list from Y to Z of W and equal (Z and Y) and 1, then equal X and (V element of W) |
(=>
(and
(equal ?R
(SubListFn ?S ?E ?L))
(greaterThan
(SubtractionFn ?E ?S) 1))
(equal ?R
(ListConcatenateFn
(ListFn
(ListOrderFn ?L ?S))
(SubListFn
(AdditionFn 1 ?S) ?E ?L)))) |
Merge.kif 3301-3313 |
If equal X and the sub-list from Y to Z of W and (Z and Y) is greater than 1, then equal X and the list composed of (V element of W) and the sub-list from (1 and Y) to Z of W |
(=>
(equal
(LastFn ?LIST) ?ITEM)
(exists (?NUMBER)
(and
(equal
(ListLengthFn ?LIST) ?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER) ?ITEM)))) |
Merge.kif 3323-3328 |
If equal the last of X and Y, then there exists Z such that equal length of X, Z, equal W element of X, and Y |
(=>
(and
(instance ?LIST List)
(not
(equal ?LIST NullList)))
(equal
(FirstFn ?LIST)
(ListOrderFn ?LIST 1))) |
Merge.kif 3343-3348 |
If X is an instance of list and equal X and null list, then equal the first of X and 1th element of X |
(=>
(and
(equal ?A
(ListSumFn ?L))
(equal 1
(ListLengthFn ?L)))
(equal ?A
(ListOrderFn ?L 1))) |
Merge.kif 3363-3367 |
If equal X and the sum of Y and equal 1 and length of Y, then equal X and 1th element of Y |
(=>
(and
(exactCardinality ?REL ?ARG 1)
(instance ?REL Predicate))
(exists (?X @ARGS)
(and
(?REL @ARGS)
(equal ?X
(ListOrderFn
(ListFn @ARGS) ?ARG))
(not
(exists (?Y)
(and
(equal ?Y
(ListOrderFn
(ListFn @ARGS) ?ARG))
(not
(equal ?X ?Y)))))))) |
Media.kif 2022-2037 |
If there can be 1 values to argument X of Y and Y is an instance of predicate, then there exist Z and @ARGS such that Y @ARGS and equal Z and V element of (@ARGS) and there doesn't exist U such that equal U and V element of (@ARGS) and equal Z and U |
(=>
(and
(exactCardinality ?REL ?ARG 1)
(instance ?REL Predicate)
(?REL @ARGS)
(equal ?X
(ListOrderFn
(ListFn @ARGS) ?ARG)))
(not
(exists (?Y)
(and
(equal ?Y
(ListOrderFn
(ListFn @ARGS) ?ARG))
(not
(equal ?X ?Y)))))) |
Media.kif 2040-2050 |
If there can be 1 values to argument X of Y, Y is an instance of predicate, Y @ARGS, and equal W and V element of (@ARGS), then there doesn't exist U such that equal U and V element of (@ARGS) and equal W and U |
(=>
(exactCardinality ?REL ?ARG ?COUNT)
(exists (?EL @ARGS)
(equal
(CardinalityFn
(KappaFn ?EL
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG))))) ?COUNT))) |
Media.kif 2072-2081 |
If there can be X values to argument Y of Z, then there exist W, @ARGS such that equal the number of instances in the class described by W, and X |
(=>
(and
(exactCardinality ?REL ?ARG ?COUNT)
(instance ?REL Predicate))
(exists (?S ?EL @ARGS)
(and
(instance ?S SetOrClass)
(=>
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG)))
(and
(instance ?EL ?S)
(equal
(CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2084-2097 |
If there can be X values to argument Y of Z and Z is an instance of predicate, then there exist W, V and @ARGS such that W is an instance of set or class and Z @ARGS and equal V and T element of (@ARGS)V is an instance of W and equal the number of instances in W and X |
(=>
(minCardinality ?REL ?ARG ?COUNT)
(exists (?EL @ARGS)
(greaterThanOrEqualTo
(CardinalityFn
(KappaFn ?EL
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG))))) ?COUNT))) |
Media.kif 2108-2117 |
If there are at least X values to argument Y of Z, then there exist W and @ARGS such that the number of instances in the class described by W is greater than or equal to X |
(=>
(and
(minCardinality ?REL ?ARG ?COUNT)
(instance ?REL Predicate))
(exists (?S ?EL @ARGS)
(and
(instance ?S SetOrClass)
(=>
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG)))
(and
(instance ?EL ?S)
(greaterThanOrEqualTo
(CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2121-2134 |
If there are at least X values to argument Y of Z and Z is an instance of predicate, then there exist W, V and @ARGS such that W is an instance of set or class and Z @ARGS and equal V and T element of (@ARGS)V is an instance of W and the number of instances in W is greater than or equal to X |
(=>
(maxCardinality ?REL ?ARG ?COUNT)
(exists (?EL @ARGS)
(lessThanOrEqualTo
(CardinalityFn
(KappaFn ?EL
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG))))) ?COUNT))) |
Media.kif 2145-2154 |
If there can be at most X values to argument Y of Z, then there exist W and @ARGS such that the number of instances in the class described by W is less than or equal to X |
(=>
(and
(maxCardinality ?REL ?ARG ?COUNT)
(instance ?REL Predicate))
(exists (?S ?EL @ARGS)
(and
(instance ?S SetOrClass)
(=>
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG)))
(and
(instance ?EL ?S)
(lessThanOrEqualTo
(CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2157-2170 |
If there can be at most X values to argument Y of Z and Z is an instance of predicate, then there exist W, V and @ARGS such that W is an instance of set or class and Z @ARGS and equal V and T element of (@ARGS)V is an instance of W and the number of instances in W is less than or equal to X |
(=>
(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 306-327 |
If X is an average of Y, then there exist Z and W such that equal length of Z and length of Y and equal 1th element of Z and 1th element of Y and V V is a member of Zthere exist U, T,, , S and R such that U is greater than 1 and U is less than or equal to length of Z and equal Q element of Z and U and S is a member of Y and equal U and P element of Y and R is a member of Z and equal T and (U and 1) and equal T and O element of Z and equal V and (S and R) and equal W and length of Z and equal X and N element of Z and W |
(=>
(and
(instance ?SEO SEO)
(patient ?SEO ?PAGE))
(hasPurpose ?SEO
(exists (?SRPRESULT_BEFORE ?SRPRESULT_AFTER ?BEFORE ?AFTER ?BM1 ?BM2)
(and
(instance ?SRPRESULT_BEFORE SRPResults)
(instance ?SRPRESULT_AFTER SRPResults)
(equal ?PAGE
(ListOrderFn ?SRPRESULT_BEFORE ?BEFORE))
(equal ?PAGE
(ListOrderFn ?SRPRESULT_AFTER ?AFTER))
(instance ?BM1 BestMatchAlgorithm)
(instance ?BM2 BestMatchAlgorithm)
(earlier
(WhenFn ?BM1)
(WhenFn ?BM2))
(earlier
(WhenFn ?SEO)
(WhenFn ?BM2))
(earlier
(WhenFn ?BM1)
(WhenFn ?SEO))
(greaterThan ?BEFORE ?AFTER))))) |
UXExperimentalTerms.kif 2389-2405 |
If X is an instance of search engine optimization and Y is a patient of X, then All of the following hold: (1) X has the purpose there exist ?SRPRESULT_BEFORE, ?SRPRESULT_AFTER,, , W,, , V,, , U (2) T such that ?SRPRESULT_BEFORE is an instance of search results (3) ?SRPRESULT_AFTER is an instance of search results (4) equal Y (5) S element of ?SRPRESULT_BEFORE (6) equal Y (7) R element of ?SRPRESULT_AFTER (8) U is an instance of best match sort (9) T is an instance of best match sort (10) the time of existence of U happens earlier than the time of existence of T (11) the time of existence of X happens earlier than the time of existence of T (12) the time of existence of U happens earlier than the time of existence of X (13) W is greater than V |
(=>
(and
(equal ?VA
(VarianceAverageFn ?M ?L))
(greaterThan
(ListLengthFn ?L) 1))
(equal ?VA
(AdditionFn
(VarianceAverageFn ?M
(ListOrderFn ?L 1))
(VarianceAverageFn ?M
(SubListFn 2
(ListLengthFn ?L) ?L))))) |
Weather.kif 2763-2775 |
If equal X and VarianceAverageFn of Y with the mean of Z and length of Y is greater than 1, then equal X and (VarianceAverageFn of 1th element of Y with the mean of Z and VarianceAverageFn of the sub-list from 2 to length of Y of Y with the mean of Z) |
(=>
(and
(equal ?VA
(VarianceAverageFn ?M ?L))
(equal 1
(ListLengthFn ?L)))
(equal ?VA
(MultiplicationFn
(SubtractionFn ?M
(ListOrderFn ?L 1))
(SubtractionFn ?M
(ListOrderFn ?L 1))))) |
Weather.kif 2796-2807 |
If equal X and VarianceAverageFn of Y with the mean of Z and equal 1 and length of Y, then equal X and (Z and 1th element of Y) and (Z and 1th element of Y) |