;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-;;; If you load this file (with translation into the "KIF" implementation;;; -- the default ), then the definitions are saved on property lists;;; and can be used for online documentation and in cross-reference reports.(in-package "ONTOLINGUA-USER") ;inherits from the KIF package;all constants defined here are exported;from the KIF package.(define-theoryKIF-NUMBERS() "The KIF vocabulary concerning numbers and arithmetic.") (in-theory 'kif-numbers) (define-classNUMBER(?x) "Number") (define-classREAL-NUMBER(?x) "Real number" :def (number ?x)) (define-classRATIONAL-NUMBER(?x) "Rational number" :iff-def (and (real-number ?x) (exists (?y) (and (integer ?y) (integer (* ?x ?y)))))) (define-classINTEGER(?x) "Integer" :def (rational-number ?x)) (define-classEVEN-INTEGER(?x) "Even integer" :def (and (integer ?x) (= (mod ?x 2) 0))) (define-classODD-INTEGER(?x) "Odd integer" :def (and (integer ?x) (= (mod ?x 2) 1))) (define-classNATURAL(?x) "Natural number" :iff-def (and (integer ?x) (> ?x 0))) (define-classNONNEGATIVE-INTEGER(?x) "Nonnegative integer" :def (and (integer ?x) (>= ?x 0))) (define-classPOSITIVE(?x) "Positive number" :def (and (number ?x) (> ?x 0))) (define-classNEGATIVE(?x) "Negative number" :def (and (number ?x) (<?x 0))) (define-classCOMPLEX-NUMBER(?x) "Complex number" :def (number ?x)) (define-classZERO(?x) "The class containing 0. May be used as a predicate." :iff-def (= ?x 0)) (define-relationLOGBIT(?x ?y) "The sentence {\tt (logbit $\tau_1$ $\tau_2$)} is true if bit $\tau_2$ of $\tau_1$ is 1.") (define-relationLOGTEST(?x ?y) "The sentence {\tt (logtest $\tau_1$ $\tau_2$)} is true if the logical {\it and} of the two's-complement representation of the integers $\tau_1$ and $\tau_2$ is not zero.");;;---Arithmetic Functions and friends;;; These are deliberately not axiomatized, waiting for a;;; proper treatment. Might want to leave room for operator;;; overloading.(define-function*(@args) :-> ?product "If $\tau_1$, ..., $\tau_n$ denote numbers, then the term {\tt (* $\tau_1 \ldots \tau_n$)} denotes the product of those numbers.") (define-function+(@args) :-> ?sum "If $\tau_1$, ..., $\tau_n$ are numerical constants, then the term {\tt (+ $\tau_1 ... \tau_n$)} denotes the sum $\tau$ of the numbers corresponding to those constants.") (define-function-(@args) :-> ?difference "If $\tau$ and $\tau_1$, ..., $\tau_n$ denote numbers, then the term {\tt (- $\tau$ $\tau_1 ... \tau_n$)} denotes the difference between the number denoted by $\tau$ and the numbers denoted by $\tau_1$ through $\tau_n$. An exception occurs when $n=0$, in which case the term denotes the negation of the number denoted by $\tau$.") (define-function/(@args) :-> ?result "If $\tau_1$, ..., $\tau_n$ are numbers, then the term {\tt (/ $\tau_1 ... \tau_n$)} denotes the result $\tau$ obtained by dividing the number denoted by $\tau_1$ by the numbers denoted by $\tau_2$ through $\tau_n$. An exception occurs when $n=1$, in which case the term denotes the reciprocal $\tau$ of the number denoted by $\tau_1$.") (define-function1+(?x) :-> ?result "The term {\tt (1+ $\tau$)} denotes the sum of the object denoted by $\tau$ and 1." :lambda-body (+ ?x 1)) (define-function1-(?x) :-> ?result "The term {\tt (1- $\tau$)} denotes the difference of the object denoted by $\tau$ and 1." :lambda-body (- ?x 1)) (define-functionABS(?x) "The term {\tt (abs $\tau$)} denotes the absolute value of the object denoted by $\tau$. " :lambda-body (if (>= ?x 0) ?x (- ?x))) (define-functionACOS(?x) "If $\tau$ denotes a number, then the term {\tt (acos $\tau$)} denotes the arc cosine of that number (in radians).") (define-functionACOSH(?x) "The term {\tt (acosh $\tau$)} denotes the arc cosine of the object denoted by $\tau$ (in radians).") (define-functionASH(?x) "The term {\tt (ash $\tau_1$ $\tau_2$)} denotes the result of arithmetically shifting the object denoted by $\tau_1$ by the number of bits denoted by $\tau_2$ (left or right shifting depending on the sign of $\tau_2$).") (define-functionASIN(?x) "The term {\tt (asin $\tau$)} denotes the arc sine of the object denoted by $\tau$ (in radians).") (define-functionASINH(?x) "The term {\tt (asinh $\tau$)} denotes the hyperbolic arc sine of the object denoted by $\tau$ (in radians).") (define-functionATAN(?x) "The term {\tt (atan $\tau$)} denotes the arc tangent of the object denoted by $\tau$ (in radians).") (define-functionATANH(?x) "The term {\tt (atanh $\tau$)} denotes the hyperbolic arc tangent of the object denoted by $\tau$ (in radians).") (define-functionBOOLE(?x) "The term {\tt (boole $\tau$ $\tau_1$ $\tau_2$)} denotes the result of applying the operation denoted by $\tau$ to the objects denoted by $\tau_1$ and $\tau_2$.") (define-functionCEILING(?x) "If $\tau$ denotes a real number, then the term {\tt (ceiling $\tau$)} denotes the smallest integer greater than or equal to the anumber denoted by $\tau$.") (define-functionCIS(?radians) :-> ?complex "The term {\tt (cis $\tau$)} denotes the complex number denoted by $cos(\tau) + i sin(\tau)$. The argument is any non-complex number of radians." :def (and (number ?radians) (not (complex-number ?radians)) (complex-number ?complex))) (define-functionCONJUGATE(?c) :-> ?complex "If $\tau$ denotes a complex number, then the term {\tt (conjugate $\tau$)} denotes the complex conjugate of the number denoted by $\tau$.") (define-functionCOS(?x) "The term {\tt (cos $\tau$)} denotes the cosine of the object denoted by $\tau$ (in radians).") (define-functionCOSH(?x) "The term {\tt (cosh $\tau$)} denotes the hyperbolic cosine of the object denoted by $\tau$ (in radians).") (define-functionDECODE-FLOAT(?x) "The term {\tt (decode-float $\tau$)} denotes the mantissa of the object denoted by $\tau$.") (define-functionDENOMINATOR(?x) "The term {\tt (denominator $\tau$)} denotes the denominator of the canonical reduced form of the object denoted by $\tau$.") (define-functionEXP(?x) "The term {\tt (exp $\tau$)} denotes $e$ raised to the power the object denoted by $\tau$." :lambda-body (expt the-exponentiation-constant-E ?x)) (define-instancethe-exponentiation-constant-E(real-number) "The constant often called 'e' using in exponentiation.") (define-functionEXPT(?x ?power) "{The term {\tt (expt $\tau_1$ $\tau_2$)} denotes the object denoted by $\tau_1$ raised to the power the object denoted by $\tau_2$.}") (define-functionFCEILING(?x) "The term {\tt (fceiling $\tau$)} denotes the smallest integer (as a floating point number) greater than the object denoted by $\tau$.") (define-functionFFLOOR(?x) "The term {\tt (ffloor $\tau$)} denotes the largest integer (as a floating point number) less than the object denoted by $\tau$.") (define-functionFLOAT(?x) "The term {\tt (float $\tau$)} denotes the floating point number equal to the object denoted by $\tau$.") (define-functionFLOAT-DIGITS(?x) :-> ?integer "The term {\tt (float-digits $\tau$)} denotes the number of digits used in the representation of a floating point number denoted by $\tau$." :def (nonnegative-integer ?integer)) (define-functionFLOAT-PRECISION(?x) :-> ?integer "The term {\tt (float-precision $\tau$)} denotes the number of significant digits in the floating point number denoted by $\tau$." :def (nonnegative-integer ?integer)) (define-functionFLOAT-RADIX(?x) :-> ?n "The term {\tt (float-radix $\tau$)} denotes the radix of the floating point number denoted by $\tau$. The most common values are 2 and 16." :def (natural ?n)) (define-functionFLOAT-SIGN(?x) "The term {\tt (float-sign $\tau_1$ $\tau_2$)} denotes a floating-point number with the same sign as the object denoted by $\tau_1$ and the same absolute value as the object denoted by $\tau_2$.") (define-functionFLOOR(?x) :-> ?integer "The term {\tt (floor $\tau$)} denotes the largest integer less than the object denoted by $\tau$." :def (integer ?integer)) (define-functionFROUND(?x) "The term {\tt (fround $\tau$)} is equivalent to {\tt (ffloor (+ 0.5 $\tau$))}." :lambda-body (ffloor (+ 0.5 ?x))) (define-functionFTRUNCATE(?x) "The term {\tt (ftruncate $\tau$)} denotes the largest integer (as a floating point number) less than the object denoted by $\tau$.") (define-functionGCD(?x) "The term {\tt (gcd $\tau_1 \ldots \tau_n$)} denotes the greatest common divisor of the objects denoted by $\tau_1$ through $\tau_n$.") (define-functionIMAGPART(?x) "The term {\tt (imagpart $\tau$)} denotes the imaginary part of the object denoted by $\tau$.") (define-functionINTEGER-DECODE-FLOAT(?x) :-> ?integer "The term {\tt (integer-decode-float $\tau$)} denotes the significand of the object denoted by $\tau$." :def (integer ?integer)) (define-functionINTEGER-LENGTH(?x) :-> ?integer "The term {\tt (integer-length $\tau$)} denotes the number of bits required to store the absolute magnitude of the object denoted by $\tau$." :def (nonnegative-integer ?integer)) (define-functionISQRT(?x) :-> ?integer "The term {\tt (isqrt $\tau$)} denotes the integer square root of the object denoted by $\tau$." :def (nonnegative-integer ?integer)) (define-functionLCM(@args) "The term {\tt (lcm $\tau_1 \ldots \tau_n$)} denotes the least common multiple of the objects denoted by $\tau_1,\ldots,\tau_n$.") (define-functionLOG(?number ?base) "The term {\tt (log $\tau_1$ $\tau_2$)} denotes the logarithm of the object denoted by $\tau_1$ in the base denoted by $\tau_2$.") (define-functionLOGAND(@args) "The term {\tt (logand $\tau_1 \ldots \tau_n$)} denotes the bit-wise logical and of the objects denoted by $\tau_1$ through $\tau_n$.") (define-functionLOGANDC1(?x ?y) "The term {\tt (logandc1 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logand (lognot $\tau_1$) $\tau_2$)}." :lambda-body (logand (lognot ?x) ?y)) (define-functionLOGANDC2(?x ?y) "The term {\tt (logandc2 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logand $\tau_1$ (lognot $\tau_2$))}." :lambda-body (logand ?x (lognot ?y))) (define-functionLOGCOUNT(?x) "The term {\tt (logcount $\tau$)} denotes the number of {\it on} bits in the object denoted by $\tau$. If the denotation of $\tau$ is positive, then the one bits are counted; otherwise, the zero bits in the twos-complement representation are counted.") (define-functionLOGEQV(@args) "The term {\tt (logeqv $\tau_1 \ldots \tau_n$)} denotes the logical-exclusive-or of the objects denoted by $\tau_1,\ldots,\tau_n$.") (define-functionLOGIOR(@args) "The term {\tt (logior $\tau_1 \ldots \tau_n$)} denotes the bit-wise logical inclusive or of the objects denoted by $\tau_1$ through $\tau_n$. It denotes 0 if there are no arguments.") (define-functionLOGNAND(?x ?y) "The term {\tt (lognand $\tau_1$ $\tau_2$)} is equivalent to {\tt (lognot (logand $\tau_1$ $\tau_2$))}." :lambda-body (lognot (logand ?x ?y))) (define-functionLOGNOR(?x ?y) "The term {\tt (lognor $\tau_1$ $\tau_2$)} is equivalent to {\tt (lognot (logior $\tau_1$ $\tau_2$))}." :lambda-body (lognot (logior ?x ?y))) (define-functionLOGNOT(?x) "The term {\tt (lognot $\tau$)} denotes the bit-wise logical not of the object denoted by $\tau$.") (define-functionLOGORC1(?x ?y) "The term {\tt (logorc1 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logior (lognot $\tau_1$) $\tau_2$)}." :lambda-body (logior (lognot ?x) ?y)) (define-functionLOGORC2(?x ?y) "The term {\tt (logorc2 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logior $\tau_1$ (lognot $\tau_2$))}." :lambda-body (logior ?x (lognot ?y))) (define-functionLOGXOR(@args) "The term {\tt (logxor $\tau_1 \ldots \tau_n$)} denotes the bit-wise logical exclusive or of the objects denoted by $\tau_1$ through $\tau_n$. It denotes 0 if there are no arguments.") (define-functionMAX(@args) "The term {\tt (max $\tau_1 \ldots \tau_k$)} denotes the largest object denoted by $\tau_1$ through $\tau_n$.") (define-functionMIN(@args) "The term {\tt (min $\tau_1 \ldots \tau_k$)} denotes the smallest object denoted by $\tau_1$ through $\tau_n$.") (define-functionMOD(?x ?y) "The term {\tt (mod $\tau_1$ $\tau_2$)} denotes the root of the object denoted by $\tau_1$ modulo the object denoted by $\tau_2$. The result will have the same sign as denoted by $\tau_1$.") (define-functionNUMERATOR(?x) "The term {\tt (numerator $\tau$)} denotes the numerator of the canonical reduced form of the object denoted by $\tau$.") (define-functionPHASE(?x) "The term {\tt (phase $\tau$)} denotes the angle part of the polar representation of the object denoted by $\tau$ (in radians).") (define-functionRATIONALIZE(?x) "The term {\tt (rationalize $\tau$)} denotes the rational representation of the object denoted by $\tau$.") (define-functionREALPART(?x) "The term {\tt (realpart $\tau$)} denotes the real part of the object denoted by $\tau$.") (define-functionREM(?number ?divisor) "The term {\tt (rem<number><divisor>)} denotes the remainder of the object denoted by {\tt<number>} divided by the object denoted by {\tt<divisor>}. The result has the same sign as the object denoted by {\tt<divisor>}.") (define-functionROUND(?x) :-> ?integer "The term {\tt (round $\tau$)} denotes the integer nearest to the object denoted by $\tau$. If the object denoted by $\tau$ is halfway between two integers (for example 3.5), it denotes the nearest integer divisible by 2." :def (integer ?integer)) (define-functionSCALE-FLOAT(?x ?y) "The term {\tt (scale-float $\tau_1$ $\tau_2$)} denotes a floating-point number that is the representational radix of the object denoted by $\tau_1$ raised to the integer denoted by $\tau_2$.") (define-functionSIGNUM(?x) "The term {\tt (signum $\tau$)} denotes the sign of the object denoted by $\tau$. This is one of -1, 1, or 0 for rational numbers and one of -1.0, 1.0, or 0.0 for floating point numbers.") (define-functionSIN(?x) "The term {\tt (sin $\tau$)} denotes the sine of the object denoted by $\tau$ (in radians).") (define-functionSINH(?x) "The term {\tt (sinh $\tau$)} denotes the hyperbolic sine of the object denoted by $\tau$ (in radians).") (define-functionSQRT(?x) "The term {\tt (sqrt $\tau$)} denotes the principal square root of the object denoted by $\tau$.") (define-functionTAN(?x) "The term {\tt (tan $\tau$)} denotes the tangent of the object denoted by $\tau$ (in radians).") (define-functionTANH(?x) "The term {\tt (tanh $\tau$)} denotes the hyperbolic tangent of the object denoted by $\tau$ (in radians).") (define-functionTRUNCATE(?x) "The term {\tt (truncate $\tau$)} denotes the largest integer less than the object denoted by $\tau$.");;;--- Arithetic relations ----(define-relation<(?x ?y) "The sentence {\tt (<$\tau_1$ $\tau_2$)} is true if and only if the number denoted by $\tau_1$ is less than the number denoted by $\tau_2$.") (define-relation>(?x ?y) :iff-def (<?y ?x)) (define-relation=<(?x ?y) :iff-def (or (= ?x ?y) (<?x ?y))) (define-relation>=(?x ?y) :iff-def (or (> ?x ?y) (= ?x ?y)))