partialOrderingOn - Sigma Knowledge base Browser

appearance as argument number 1

(instance partialOrderingOn BinaryPredicate)	Merge.kif 3750-3750	partial ordering on is an instance of binary predicate
(domain partialOrderingOn 1 BinaryRelation)	Merge.kif 3751-3751	The number 1 argument of partial ordering on is an instance of binary relation
(domain partialOrderingOn 2 Class)	Merge.kif 3752-3752	The number 2 argument of partial ordering on is an instance of class
(documentation partialOrderingOn EnglishLanguage "A BinaryRelation is a partial ordering on a Class only if the relation is reflexiveOn the Class, and it is both an AntisymmetricRelation, and a TransitiveRelation.")	Merge.kif 3754-3757	The number 2 argument of partial ordering on is an instance of class

appearance as argument number 2

(termFormat EnglishLanguage partialOrderingOn "partial ordering on")	domainEnglishFormat.kif 44537-44537
(termFormat ChineseTraditionalLanguage partialOrderingOn "部分訂購在")	domainEnglishFormat.kif 44538-44538
(termFormat ChineseLanguage partialOrderingOn "部分订购在")	domainEnglishFormat.kif 44539-44539
(format EnglishLanguage partialOrderingOn "%1 is %n partial ordering on %2")	english_format.kif 164-164

antecedent

(=> (partialOrderingOn ?RELATION ?CLASS) (and (reflexiveOn ?RELATION ?CLASS) (instance ?RELATION TransitiveRelation) (instance ?RELATION AntisymmetricRelation)))	Merge.kif 3759-3764	If X is partial ordering on Y, then X is reflexive on Y, X is an instance of transitive relation, and X is an instance of antisymmetric relation
(=> (and (partialOrderingOn ?RELATION ?CLASS) (trichotomizingOn ?RELATION ?CLASS)) (totalOrderingOn ?RELATION ?CLASS))	Merge.kif 3781-3785	If X is partial ordering on Y and X is trichotomizing on Y, then X is total ordering on Y

consequent

(=>
    (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