ListFn |
appearance as argument number 1 |
![]() |
(documentation ListFn ChineseLanguage "这是一个可以接受任何数量的参数,然后交出含有跟哪些参数完全 相同顺序的 Function。") | chinese_format.kif 1962-1963 | |
(documentation ListFn EnglishLanguage "A Function that takes any number of arguments and returns the List containing those arguments in exactly the same order.") | Merge.kif 2937-2938 | |
(documentation ListFn JapaneseLanguage "任意の数の引数を受け取り、それらの引数を含む List を まったく同じ順序で返す Function。") | japanese_format.kif 594-595 | |
(domain ListFn 1 Entity) | Merge.kif 2933-2933 | Le nombre 1 argument de ListFn est une instance de entit� |
(instance ListFn Function) | Merge.kif 2931-2931 | ListFn est une instance de function |
(instance ListFn VariableArityRelation) | Merge.kif 2932-2932 | ListFn est une instance de relation a arit� variable |
(range ListFn List) | Merge.kif 2935-2935 | Le domaine de ListFn est une instance de liste |
appearance as argument number 2 |
![]() |
(format ChineseLanguage ListFn "(%*[,])") | chinese_format.kif 261-261 | |
(format EnglishLanguage ListFn "(%*[,])") | english_format.kif 266-266 | |
(format FrenchLanguage ListFn "(%*[,])") | french_format.kif 149-149 | |
(format ItalianLanguage ListFn "(%*[,]") | relations-it.txt 167-167 | |
(format JapaneseLanguage ListFn "(%*[,])") | japanese_format.kif 1977-1977 | |
(format PortugueseLanguage ListFn "(%*[,])") | portuguese_format.kif 101-101 | |
(format cz ListFn "(%*[,])") | relations-cz.txt 158-158 | |
(format de ListFn "(%*[,])") | relations-de.txt 336-336 | |
(format hi ListFn "(%*[,]") | relations-hindi.txt 206-206 | |
(format ro ListFn "(%*[,])") | relations-ro.kif 168-168 | |
(format sv ListFn "(%*[,])") | relations-sv.txt 155-155 | |
(format tg ListFn "(%*[,]") | relations-tg.txt 333-333 | |
(termFormat ChineseLanguage ListFn "名单") | domainEnglishFormat.kif 34691-34691 | |
(termFormat ChineseLanguage ListFn "表列函数") | chinese_format.kif 262-262 | |
(termFormat ChineseTraditionalLanguage ListFn "名單") | domainEnglishFormat.kif 34690-34690 | |
(termFormat EnglishLanguage ListFn "list") | domainEnglishFormat.kif 34689-34689 | |
(termFormat de ListFn "ListeFn") | terms-de.txt 107-107 | |
(termFormat tg ListFn "tungkulin ng talaan") | relations-tg.txt 334-334 |
antecedent |
![]() |
consequent |
![]() |
(=> (and (domain ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (instance (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 2998-3003 | |
(=> (and (domainSubclass ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (subclass (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 3005-3010 | |
(=> (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 ?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 ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 1)) (equal ?R (ListFn (ListOrderFn ?L ?S)))) |
Merge.kif 3179-3188 |
|
(=> (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 3190-3202 |
|
(=> (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 (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 |
|
(=> (and (valence ?REL ?NUMBER) (instance ?REL Predicate)) (forall (@ROW) (=> (?REL @ROW) (equal (ListLengthFn (ListFn @ROW)) ?NUMBER)))) |
Merge.kif 3048-3055 |
|
(=> (contraryAttribute @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Attribute))) |
Merge.kif 464-468 | |
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM) (=> (inList ?ITEM (ListFn @ROW)) (subclass ?ITEM ?CLASS)))) |
Merge.kif 2950-2955 | |
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM1 ?ITEM2) (=> (and (inList ?ITEM1 (ListFn @ROW)) (inList ?ITEM2 (ListFn @ROW)) (not (equal ?ITEM1 ?ITEM2))) (disjoint ?ITEM1 ?ITEM2)))) |
Merge.kif 2957-2966 | |
(=> (disjointDecomposition @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Class))) |
Merge.kif 574-578 | |
(=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number))) |
Merge.kif 4854-4859 | |
(=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number))) |
Merge.kif 4939-4944 | |
(=> (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 |
|
(=> (exhaustiveAttribute ?CLASS @ROW) (forall (?ATTR1) (=> (instance ?ATTR1 ?CLASS) (exists (?ATTR2) (and (inList ?ATTR2 (ListFn @ROW)) (equal ?ATTR1 ?ATTR2)))))) |
Merge.kif 509-517 | |
(=> (exhaustiveDecomposition ?CLASS @ROW) (forall (?OBJ) (=> (instance ?OBJ ?CLASS) (exists (?ITEM) (and (inList ?ITEM (ListFn @ROW)) (instance ?OBJ ?ITEM)))))) |
Merge.kif 2940-2948 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
![]() |
(forall (@ROW ?ITEM) (equal (ListLengthFn (ListFn @ROW ?ITEM)) (SuccessorFn (ListLengthFn (ListFn @ROW))))) |
Merge.kif 3037-3040 | @ROW Entit� longueur de (@ROW + entit�) est longueur de (@ROW)+1) |
(forall (@ROW ?ITEM) (equal (ListOrderFn (ListFn @ROW ?ITEM) (ListLengthFn (ListFn @ROW ?ITEM))) ?ITEM)) |
Merge.kif 3042-3046 | @ROW Entit� longueur de (@ROW + entit�)th entit�) est entit� |
(forall (@ROW ?ITEM) (initialList (ListFn @ROW) (ListFn @ROW ?ITEM))) |
Merge.kif 3315-3316 | @ROW Entit� (@ROW) commence (@ROW + entit�) |
![]() |
![]() |