Knowledge Interchange Format Specification

Chapter 4: Numbers


Introduction

The referent of every numerical constant in KIF is assumed to be the number for which that constant is the base 10 representation. Among other things, this means that we can infer inequality of all distinct numerical constants, i.e. for every t1 and distinct t2 the following sentence is true.
    (/= t1 t2)
We use the intended meaning of numerical constants in defining the numerical functions and relations in this chapter. In effect, we require that these functions and relations behave correctly on all numbers represented in this way. Note that this does mean that it is incorrect to apply these functions and relations to terms other than numbers. For example, a nonnumerical term may refer to a number, e.g. the term two may be defined to be the same as the number 2 in which case it is perfectly proper to write (+ two two). We may also want to extend these functions and relations to apply to objects other than numbers, e.g. sets and lists.

Functions on Numbers

* -- If t1, ..., tn denote numbers, then the term (* t1 ... tn) denotes the product of those numbers.

+ -- If t1, ..., tn are numerical constants, then the term (+ t1 ... tn) denotes the sum t of the numbers corresponding to those constants.

- -- If t and t1, ..., tn denote numbers, then the term (- t t1 ... tn) denotes the difference between the number denoted by t and the numbers denoted by t1 through tn. An exception occurs when n=0, in which case the term denotes the negation of the number denoted by t.

/ -- If t1, ..., tn are numbers, then the term (/ t1 ... tn) denotes the result t obtained by dividing the number denoted by t1 by the numbers denoted by t2 through tn. An exception occurs when n=1, in which case the term denotes the reciprocal t of the number denoted by t1.

1+ -- The term (1+ t) denotes the sum of the object denoted by t and 1.

(deffunction 1+ (?x) := (+ ?x 1))
1- -- The term (1- t) denotes the difference of the object denoted by t and 1.

(deffunction 1- (?x) := (- ?x 1))
abs -- The term (abs t) denotes the absolute value of the object denoted by t.

(deffunction abs (?x) := (if (>= ?x 0) ?x (- ?x)))
acos -- If t denotes a number, then the term (acos t) denotes the arc cosine of that number (in radians).

acosh -- The term (acosh t) denotes the arc cosine of the object denoted by t (in radians).

ash -- The term (ash t1 t2) denotes the result of arithmetically shifting the object denoted by t1 by the number of bits denoted by t2 (left or right shifting depending on the sign of t2).

asin -- The term (asin t) denotes the arc sine of the object denoted by t (in radians).

asinh -- The term (asinh t) denotes the hyperbolic arc sine of the object denoted by t (in radians).

atan -- The term (atan t) denotes the arc tangent of the object denoted by t (in radians).

atanh -- The term (atanh t) denotes the hyperbolic arc tangent of the object denoted by t (in radians).

boole -- The term (boole t t1 t2) denotes the result of applying the operation denoted by t to the objects denoted by t1 and t2.

ceiling -- If t denotes a real number, then the term (ceiling t) denotes the smallest integer greater than or equal to the number denoted by t.

cis -- The term (cis t) denotes the complex number cos(t) + i sin(t). The argument is any non-complex number of radians.

conjugate -- If t denotes a complex number, then the term (conjugate t) denotes the complex conjugate of the number denoted by t.

(deffunction conjugate (?c) := (complex (realpart ?c) (- (imagpart ?c))))
cos -- The term (cos t) denotes the cosine of the object denoted by t (in radians).

cosh -- The term (cosh t) denotes the hyperbolic cosine of the object denoted by t (in radians).

decode-float -- The term (decode-float t) denotes the mantissa of the object denoted by t.

denominator -- The term (denominator t) denotes the denominator of the canonical reduced form of the object denoted by t.

exp -- The term (exp t) denotes e raised to the power the object denoted by t.

(deffunction exp (?x) := (expt e ?x))
expt -- The term (expt t1 t2) denotes the object denoted by t1 raised to the power the object denoted by t2.

fceiling -- The term (fceiling t) denotes the smallest integer (as a floating point number) greater than the object denoted by t.

ffloor -- The term (ffloor t) denotes the largest integer (as a floating point number) less than the object denoted by t.

float -- The term (float t) denotes the floating point number equal to the object denoted by t.

float-digits -- The term (float-digits t) denotes the number of digits used in the representation of a floating point number denoted by t.

float-precision -- The term (float-precision t) denotes the number of significant digits in the floating point number denoted by t.

float-radix -- The term (float-radix t) denotes the radix of the floating point number denoted by t. The most common values are 2 and 16.

float-sign -- The term (float-sign t1 t2) denotes a floating-point number with the same sign as the object denoted by t1 and the same absolute value as the object denoted by t2.

floor -- The term (floor t) denotes the largest integer less than the object denoted by t.

fround -- The term (fround t) is equivalent to (ffloor (+ 0.5 t)).

ftruncate -- The term (ftruncate t) denotes the largest integer (as a floating point number) less than the object denoted by t.

gcd -- The term (gcd t1 ... tn) denotes the greatest common divisor of the objects denoted by t1 through tn.

imagpart -- The term (imagpart t) denotes the imaginary part of the object denoted by t.

integer-decode-float -- The term (integer-decode-float t) denotes the significand of the object denoted by t.

integer-length -- The term (integer-length t) denotes the number of bits required to store the absolute magnitude of the object denoted by t.

isqrt -- The term (isqrt t) denotes the integer square root of the object denoted by t.

lcm -- The term (lcm t1 ... tn) denotes the least common multiple of the objects denoted by t1,...,tn.

log -- The term (log t1 t2) denotes the logarithm of the object denoted by t1 in the base denoted by t2.

logand -- The term (logand t1 ... tn) denotes the bit-wise logical and of the objects denoted by t1 through tn.

logandc1 -- The term (logandc1 t1 t2) is equivalent to (logand (lognot t1) t2).

logandc2 -- The term (logandc2 t1 t2) is equivalent to (logand t1 (lognot t2)).

logcount -- The term (logcount t) denotes the number of it on bits in the object denoted by t. If the denotation of t is positive, then the one bits are counted; otherwise, the zero bits in the twos-complement representation are counted.

logeqv -- The term (logeqv t1 ... tn) denotes the logical-exclusive-or of the objects denoted by t1,...,tn.

logior -- The term (logior t1 ... tn) denotes the bit-wise logical inclusive or of the objects denoted by t1 through tn. It denotes 0 if there are no arguments.

lognand -- The term (lognand t1 t2) is equivalent to (lognot (logand t1 t2)).

lognor -- The term (lognor t1 t2) is equivalent to (not (logior t1 t2)).

lognot -- The term (lognot t) denotes the bit-wise logical not of the object denoted by t.

logorc1 -- The term (logorc1 t1 t2) is equivalent to (logior (lognot t1) t2).

logorc2 -- The term (logorc2 t1 t2) is equivalent to (logior t1 (lognot t2)).

logxor -- The term (logxor t1 ... tn) denotes the bit-wise logical exclusive or of the objects denoted by t1 through tn. It denotes 0 if there are no arguments.

max -- The term (max t1 ... tk) denotes the largest object denoted by t1 through tn.

min -- The term (min t1 ... tk) denotes the smallest object denoted by t1 through tn.

mod -- The term (mod t1 t2) denotes the root of the object denoted by t1 modulo the object denoted by t2. The result will have the same sign as denoted by t1.

numerator -- The term (numerator t) denotes the numerator of the canonical reduced form of the object denoted by t.

phase -- The term (phase t) denotes the angle part of the polar representation of the object denoted by t (in radians).

rationalize -- The term (rationalize t) denotes the rational representation of the object denoted by t.

realpart -- The term (realpart t) denotes the real part of the object denoted by t.

rem -- The term (rem t1 t2) denotes the remainder of the object denoted by t1 divided by the object denoted by t2. The result has the same sign as the object denoted by t2.

round -- The term (round t) denotes the integer nearest to the object denoted by t. If the object denoted by t is halfway between two integers (for example 3.5), it denotes the nearest integer divisible by 2.

scale-float -- The term (scale-float t1 t2) denotes a floating-point number that is the representational radix of the object denoted by t1 raised to the integer denoted by t2.

signum -- The term (signum t) denotes the sign of the object denoted by t. 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.

sin -- The term (sin t) denotes the sine of the object denoted by t (in radians).

sinh -- The term (sinh t) denotes the hyperbolic sine of the object denoted by t (in radians).

sqrt -- The term (sqrt t) denotes the principal square root of the object denoted by t.

tan -- The term (tan t) denotes the tangent of the object denoted by t (in radians).

tanh -- The term (tanh t) denotes the hyperbolic tangent of the object denoted by t (in radians).

truncate -- The term (truncate t) denotes the largest integer less than the object denoted by t.

Relations on Numbers

integer -- The sentence (integer t) means that the object denoted by t is an integer.

real -- The sentence (real t) means that the object denoted by t is a real number.

complex -- The sentence (complex t) means that the object denoted by t is a complex number.

(defrelation number (?x) := (or (real ?x) (complex ?x))) (defrelation natural (?x) := (and (integer ?x) (>= ?x 0))) (defrelation rational (?x) := (exists (?y) (and (integer ?y) (integer (* ?x ?y)))))
< -- The sentence (< t1 t2) is true if and only if the number denoted by t1 is less than the number denoted by t2.

(defrelation > (?x ?y) := (< ?y ?x)) (defrelation =< (?x ?y) := (or (= ?x ?y) (< ?x ?y))) (defrelation >= (?x ?y) := (or (> ?x ?y) (= ?x ?y))) (defrelation positive (?x) := (> ?x 0)) (defrelation negative (?x) := (< ?x 0)) (defrelation zero (?x) := (= ?x 0)) (defrelation odd (?x) := (integer (/ (+ ?x 1) 2)) (defrelation even (?x) := (integer (/ ?x 2))
logbit -- The sentence (logbit t1 t2) is true if bit t2 of t1 is 1.

logtest -- The sentence (logtest t1 t2) is true if the logical and of the two's-complement representation of the integers t1 and t2 is not zero.


Michael R. Genesereth