Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - NullList
NullList

appearance as argument number 1
-------------------------


(documentation NullList ChineseLanguage "这是一个没有项目的 ListNullList 的独特之处是因为 List 是可以延伸,也就是说俩个含有相同项目以相同顺序排列的列表是一样的。") chinese_format.kif 1960-1961
(documentation NullList EnglishLanguage "The List that has no items. The uniqueness of NullList follows from the extensionality of Lists, i.e. the fact that two Lists with the same items in the same order are identical.") Merge.kif 2808-2810
(instance NullList List) Merge.kif 2806-2806 instance NullList and List

appearance as argument number 2
-------------------------


(termFormat ChineseLanguage NullList "空列表") domainEnglishFormat.kif 41338-41338
(termFormat ChineseTraditionalLanguage NullList "空列表") domainEnglishFormat.kif 41337-41337
(termFormat EnglishLanguage NullList "null list") domainEnglishFormat.kif 41336-41336

antecedent
-------------------------


(<=>
    (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 2972-2988 equal List and ListConcatenateFn List and List equal List and NullList equal List and NullList PositiveInteger PositiveInteger
(=>
    (and
        (instance ?LIST List)
        (not
            (equal ?LIST NullList)))
    (equal
        (FirstFn ?LIST)
        (ListOrderFn ?LIST 1)))
Merge.kif 3115-3120

consequent
-------------------------


(=>
    (and
        (equal ?R
            (SubListFn ?S ?E ?L))
        (equal
            (SubtractionFn ?E ?S) 0))
    (equal ?R NullList))
Merge.kif 3058-3065


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)



Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners