NegativeRealNumber - Sigma Knowledge base Browser

appearance as argument number 1

(subclass NegativeRealNumber RealNumber)	Merge.kif 2047-2047	Negative real number is a subclass of real number
(documentation NegativeRealNumber EnglishLanguage "A RealNumber that is less than zero.")	Merge.kif 2049-2050	Negative real number is a subclass of real number
(externalImage NegativeRealNumber "http://upload.wikimedia.org/wikipedia/ commons/ 0/ 09/ Number_line.gif")	pictureList.kif 10143-10143	Negative real number is a subclass of real number

appearance as argument number 2

(partition RealNumber NegativeRealNumber NonnegativeRealNumber)	Merge.kif 1996-1996	Real number is exhaustively partitioned into negative real number and nonnegative real number
(subclass NegativeInteger NegativeRealNumber)	Merge.kif 2090-2090	Negative integer is a subclass of negative real number
(termFormat EnglishLanguage NegativeRealNumber "negative real number")	english_format.kif 936-936	Negative integer is a subclass of negative real number

antecedent

(<=> (instance ?NUMBER NegativeRealNumber) (and (lessThan ?NUMBER 0) (instance ?NUMBER RealNumber)))	Merge.kif 2052-2056	X is an instance of negative real number if, only if X is less than 0, and X is an instance of real number
(=> (instance ?NUMBER NegativeRealNumber) (equal (SignumFn ?NUMBER) -1))	Merge.kif 5317-5319	If X is an instance of negative real number, then equal the sign of X and -1

consequent

(<=>
    (and
        (equal
            (AbsoluteValueFn ?NUMBER1) ?NUMBER2)
        (instance ?NUMBER1 RealNumber)
        (instance ?NUMBER2 RealNumber))
    (or
        (and
            (instance ?NUMBER1 NonnegativeRealNumber)
            (equal ?NUMBER1 ?NUMBER2))
        (and
            (instance ?NUMBER1 NegativeRealNumber)
            (equal ?NUMBER2
                (SubtractionFn 0.0 ?NUMBER1)))))