(<=>
(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 |
(=>
(and
(domain ?REL ?NUMBER ?CLASS)
(instance ?REL Predicate)
(?REL @ROW))
(instance
(ListOrderFn
(ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 2999-3004 |
|
(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS)
(instance ?REL Predicate)
(?REL @ROW))
(subclass
(ListOrderFn
(ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 3006-3011 |
|
(=>
(and
(equal ?A
(ListSumFn ?L))
(equal 1
(ListLengthFn ?L)))
(equal ?A
(ListOrderFn ?L 1))) |
Merge.kif 3253-3257 |
|
(=>
(and
(equal ?LIST1 ?LIST2)
(equal ?LIST1
(ListFn @ROW1))
(equal ?LIST2
(ListFn @ROW2)))
(equal
(ListOrderFn
(ListFn @ROW1) ?NUMBER)
(ListOrderFn
(ListFn @ROW2) ?NUMBER))) |
Merge.kif 295-302 |
|
(=>
(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 3084-3103 |
|
(=>
(and
(equal ?R
(SubListFn ?S ?E ?L))
(equal
(SubtractionFn ?E ?S) 1))
(equal ?R
(ListFn
(ListOrderFn ?L ?S)))) |
Merge.kif 3180-3189 |
|
(=>
(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 3191-3203 |
|
(=>
(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 1470-1481 |
|
(=>
(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 1437-1449 |
|
(=>
(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 2093-2103 |
|
(=>
(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 2075-2090 |
|
(=>
(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 2137-2150 |
|
(=>
(and
(instance ?LIST List)
(not
(equal ?LIST NullList)))
(equal
(FirstFn ?LIST)
(ListOrderFn ?LIST 1))) |
Merge.kif 3233-3238 |
|
(=>
(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 2388-2404 |
- If a process is an instance of search engine optimization and an entity is a patient of the process,
- then the process has the purpose there exist another entity_BEFORE, the other entity_AFTER,, , a third entity,, , a fourth entity,, , a fifth entity and a sixth entity such that the other entity_BEFORE is an instance of search results and the other entity_AFTER is an instance of search results and the entity is equal to the third entityth element of the other entity_BEFORE and the entity is equal to the fourth entityth element of the other entity_AFTER and the fifth entity is an instance of best match sort and the sixth entity is an instance of best match sort and the time of existence of the fifth entity happens earlier than the time of existence of the sixth entity and the time of existence of the process happens earlier than the time of existence of the sixth entity and the time of existence of the fifth entity happens earlier than the time of existence of the process and the third entity is greater than the fourth entity
|
(=>
(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 2210-2223 |
|
(=>
(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 2174-2187 |
|
(=>
(equal
(LastFn ?LIST) ?ITEM)
(exists (?NUMBER)
(and
(equal
(ListLengthFn ?LIST) ?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER) ?ITEM)))) |
Merge.kif 3213-3218 |
|
(=>
(exactCardinality ?REL ?ARG ?COUNT)
(exists (?EL @ARGS)
(equal
(CardinalityFn
(KappaFn ?EL
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG))))) ?COUNT))) |
Media.kif 2125-2134 |
|
(=>
(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 519-531 |
|
(=>
(inList ?ITEM ?LIST)
(exists (?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER) ?ITEM))) |
Merge.kif 3114-3117 |
|
(=>
(instance ?LIST UniqueList)
(forall (?NUMBER1 ?NUMBER2)
(=>
(equal
(ListOrderFn ?LIST ?NUMBER1)
(ListOrderFn ?LIST ?NUMBER2))
(equal ?NUMBER1 ?NUMBER2)))) |
Merge.kif 2911-2916 |
|
(=>
(maxCardinality ?REL ?ARG ?COUNT)
(exists (?EL @ARGS)
(lessThanOrEqualTo
(CardinalityFn
(KappaFn ?EL
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG))))) ?COUNT))) |
Media.kif 2198-2207 |
|
(=>
(minCardinality ?REL ?ARG ?COUNT)
(exists (?EL @ARGS)
(greaterThanOrEqualTo
(CardinalityFn
(KappaFn ?EL
(and
(?REL @ARGS)
(equal ?EL
(ListOrderFn
(ListFn @ARGS) ?ARG))))) ?COUNT))) |
Media.kif 2161-2170 |
|