TreeView Knowledge Base Browser

appearance as argument number 1

(instance totalOrderingOn BinaryPredicate)	Merge.kif 3766-3766	total ordering on is an instance of binary predicate
(domain totalOrderingOn 1 BinaryRelation)	Merge.kif 3767-3767	The number 1 argument of total ordering on is an instance of binary relation
(domain totalOrderingOn 2 Class)	Merge.kif 3768-3768	The number 2 argument of total ordering on is an instance of class
(documentation totalOrderingOn EnglishLanguage "A BinaryRelation ?REL is a total ordering on a Class only if it is a partial ordering for which either (?REL ?INST1 ?INST2) or (?REL ?INST2 ?INST1) for every ?INST1 and ?INST2 in the Class.")	Merge.kif 3770-3773	The number 2 argument of total ordering on is an instance of class

appearance as argument number 2

(termFormat EnglishLanguage totalOrderingOn "total ordering on")	domainEnglishFormat.kif 58597-58597
(termFormat ChineseTraditionalLanguage totalOrderingOn "總訂貨量")	domainEnglishFormat.kif 58598-58598
(termFormat ChineseLanguage totalOrderingOn "总订货量")	domainEnglishFormat.kif 58599-58599
(format EnglishLanguage totalOrderingOn "%1 is %n total ordering on %2")	english_format.kif 194-194

antecedent

(=>
    (totalOrderingOn ?RELATION ?CLASS)
    (and
        (partialOrderingOn ?RELATION ?CLASS)
        (trichotomizingOn ?RELATION ?CLASS)))

If X is total ordering on Y, then X is partial ordering on Y and X is trichotomizing on Y

consequent

(=>
    (and
        (partialOrderingOn ?RELATION ?CLASS)
        (trichotomizingOn ?RELATION ?CLASS))
    (totalOrderingOn ?RELATION ?CLASS))

If X is partial ordering on Y and X is trichotomizing on Y, then X is total ordering on Y