The KIF vocabulary concerning numbers and arithmetic.

**Last modified:***Monday, 13 December 1993***Source code: kif-ontology.lisp****List of other known theories**

**No theories were included by Kif-Numbers.**

Kif-OntologyKif-ListsKif-OntologyKif-MetaConfiguration-DesignVt-DesignSimple-BikesVt-DomainVt-ExampleKif-OntologyKif-RelationsFrame-OntologyVt-Domain...Configuration-Design...Physical-QuantitiesUnary-Scalar-FunctionsCmlThermodynamicsDmeThermodynamicsStandard-UnitsSimple-BikesCml...Vt-Design...Unary-Scalar-Functions...Scalar-QuantitiesVt-Design...Vector-QuantitiesAbstract-AlgebraPhysical-Quantities...Jat-GenericJob-Assignment-TaskGeneric-BibliographySlot-Constraint-SugarGeneric-BibliographyKif-Ontology

NumberReal-NumberRational-NumberIntegerEven-IntegerOdd-IntegerNaturalPositive-IntegerNonnegative-IntegerPositiveNegativeComplex-NumberZero

*******+****-****/****1+****1-****Abs****Acos****Acosh****Ash****Asin****Asinh****Atan****Atanh****Boole****Ceiling****Cis****Conjugate****Cos****Cosh****Decode-Float****Denominator****Exp****Expt****Fceiling****Ffloor****Float****Float-Digits****Float-Precision****Float-Radix****Float-Sign****Floor****Fround****Ftruncate****Gcd****Imagpart****Integer-Decode-Float****Integer-Length****Isqrt****Lcm****Log****Logand****Logandc1****Logandc2****Logcount****Logeqv****Logior****Lognand****Lognor****Lognot****Logorc1****Logorc2****Logxor****Max****Min****Mod****Numerator****Phase****Rationalize****Realpart****Rem****Round****Scale-Float****Signum****Sin****Sinh****Sqrt****Tan****Tanh****Truncate**

**The following constants were used from theories not included:**

**Arity***defined as a***function***in theory***Frame-Ontology****Class***defined as a***class***in theory***Frame-Ontology****Documentation***defined as a***relation***in theory***Frame-Ontology****Domain***defined as a***relation***in theory***Frame-Ontology****Function***defined as a***class***in theory***Kif-Relations****Function***defined as a***class***in theory***Frame-Ontology****Inverse***defined as a***function***in theory***Kif-Relations****Inverse***defined as a***function***in theory***Frame-Ontology****Range***defined as a***relation***in theory***Frame-Ontology****Relation***defined as a***class***in theory***Kif-Relations****Relation***defined as a***class***in theory***Frame-Ontology****Subclass-Of***defined as a***relation***in theory***Frame-Ontology****Undefined***defined as a***class***in theory***Kif-Relations**

**All constants that were mentioned were defined.**

Number

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Real number

**Subclass-Of:**Number

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Rational number

**Subclass-Of:**Real-number

**Axioms:**

(<=> (Rational-Number ?X) (And (Real-Number ?X) (Exists (?Y) (And (Integer ?Y) (Integer (* ?X ?Y)))) ))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Integer

**Subclass-Of:**Rational-number

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Even integer

**Subclass-Of:**Integer

**Axioms:**

(=> (Even-Integer ?X) (= (Mod ?X 2) 0))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Odd integer

**Subclass-Of:**Integer

**Axioms:**

(=> (Odd-Integer ?X) (= (Mod ?X 2) 1))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Natural number

**Subclass-Of:**Integer

**>:**0

*Slots Of Instances:*

**Axioms:**

(<=> (Natural ?X) (And (Integer ?X) (> ?X 0)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

An integer greater than zero, not including zero. A less ambiguous name for KIF's NATURAL.

**Subclass-Of:**Integer

**>:**0

*Slots Of Instances:*

**Axioms:**

(<=> (Positive-Integer ?X) (And (Integer ?X) (> ?X 0)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Nonnegative integer

**Subclass-Of:**Integer

**>=:**0

*Slots Of Instances:*

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Positive number

**Subclass-Of:**Number

**>:**0

*Slots Of Instances:*

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Negative number

**Subclass-Of:**Number

**<:**0

*Slots Of Instances:*

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Complex number

**Subclass-Of:**Number

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The class containing 0. May be used as a predicate.

**Axioms:**

(<=> (Zero ?X) (= ?X 0))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The sentence {tt (logbit $tau_1$ $tau_2$)} is true if bit $tau_2$ of $tau_1$ is 1.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

If $tau_1$, ..., $tau_n$ denote numbers, then the term {tt (* $tau_1 ldots tau_n$)} denotes the product of those numbers.

**Axioms:**

(Undefined (Arity *))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Axioms:**

(Undefined (Arity +))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Axioms:**

(Undefined (Arity -))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Axioms:**

(Undefined (Arity /))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (1+ $tau$)} denotes the sum of the object denoted by $tau$ and 1.

**Arity:**2

**Axioms:**

(= (1+ ?X) (+ ?X 1))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (1- $tau$)} denotes the difference of the object denoted by $tau$ and 1.

**Arity:**2

**Axioms:**

(= (1- ?X) (- ?X 1))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (abs $tau$)} denotes the absolute value of the object denoted by $tau$.

**Arity:**2

**Axioms:**

(= (Abs ?X) (If (>= ?X 0) ?X (- ?X)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

If $tau$ denotes a number, then the term {tt (acos $tau$)} denotes the arc cosine of that number (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (acosh $tau$)} denotes the arc cosine of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (asin $tau$)} denotes the arc sine of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (asinh $tau$)} denotes the hyperbolic arc sine of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (atan $tau$)} denotes the arc tangent of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (atanh $tau$)} denotes the hyperbolic arc tangent of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Arity:**2**Domain:**Number**Range:**Complex-number

**Axioms:**

(=> (Cis ?Radians ?Complex) (Not (Complex-Number ?Radians)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

If $tau$ denotes a complex number, then the term {tt (conjugate $tau$)} denotes the complex conjugate of the number denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (cos $tau$)} denotes the cosine of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (cosh $tau$)} denotes the hyperbolic cosine of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (decode-float $tau$)} denotes the mantissa of the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (denominator $tau$)} denotes the denominator of the canonical reduced form of the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (exp $tau$)} denotes $e$ raised to the power the object denoted by $tau$.

**Arity:**2

**Axioms:**

(= (Exp ?X) (Expt The-Exponentiation-Constant-E ?X))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The constant often called 'e' using in exponentiation.

**Instance-Of:**Real-number

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

{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$.}

**Arity:**3

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (fceiling $tau$)} denotes the smallest integer (as a floating point number) greater than the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (ffloor $tau$)} denotes the largest integer (as a floating point number) less than the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (float $tau$)} denotes the floating point number equal to the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (float-digits $tau$)} denotes the number of digits used in the representation of a floating point number denoted by $tau$.

**Arity:**2**Range:**Nonnegative-integer

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (float-precision $tau$)} denotes the number of significant digits in the floating point number denoted by $tau$.

**Arity:**2**Range:**Nonnegative-integer

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Arity:**2**Range:**Natural

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (floor $tau$)} denotes the largest integer less than the object denoted by $tau$.

**Arity:**2**Range:**Integer

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (fround $tau$)} is equivalent to {tt (ffloor (+ 0.5 $tau$))}.

**Arity:**2

**Axioms:**

(= (Fround ?X) (Ffloor (+ 0.5 ?X)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (ftruncate $tau$)} denotes the largest integer (as a floating point number) less than the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (gcd $tau_1 ldots tau_n$)} denotes the greatest common divisor of the objects denoted by $tau_1$ through $tau_n$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (imagpart $tau$)} denotes the imaginary part of the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (integer-decode-float $tau$)} denotes the significand of the object denoted by $tau$.

**Arity:**2**Range:**Integer

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (integer-length $tau$)} denotes the number of bits required to store the absolute magnitude of the object denoted by $tau$.

**Arity:**2**Range:**Nonnegative-integer

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (isqrt $tau$)} denotes the integer square root of the object denoted by $tau$.

**Arity:**2**Range:**Nonnegative-integer

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (lcm $tau_1 ldots tau_n$)} denotes the least common multiple of the objects denoted by $tau_1,ldots,tau_n$.

**Axioms:**

(Undefined (Arity Lcm))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Arity:**3

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Axioms:**

(Undefined (Arity Logand))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (logandc1 $tau_1$ $tau_2$)} is equivalent to {tt (logand (lognot $tau_1$) $tau_2$)}.

**Arity:**3

**Axioms:**

(= (Logandc1 ?X ?Y) (Logand (Lognot ?X) ?Y))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (logandc2 $tau_1$ $tau_2$)} is equivalent to {tt (logand $tau_1$ (lognot $tau_2$))}.

**Arity:**3

**Axioms:**

(= (Logandc2 ?X ?Y) (Logand ?X (Lognot ?Y)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (logeqv $tau_1 ldots tau_n$)} denotes the logical-exclusive-or of the objects denoted by $tau_1,ldots,tau_n$.

**Axioms:**

(Undefined (Arity Logeqv))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Axioms:**

(Undefined (Arity Logior))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (lognand $tau_1$ $tau_2$)} is equivalent to {tt (lognot (logand $tau_1$ $tau_2$))}.

**Arity:**3

**Axioms:**

(= (Lognand ?X ?Y) (Lognot (Logand ?X ?Y)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (lognor $tau_1$ $tau_2$)} is equivalent to {tt (lognot (logior $tau_1$ $tau_2$))}.

**Arity:**3

**Axioms:**

(= (Lognor ?X ?Y) (Lognot (Logior ?X ?Y)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (lognot $tau$)} denotes the bit-wise logical not of the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (logorc1 $tau_1$ $tau_2$)} is equivalent to {tt (logior (lognot $tau_1$) $tau_2$)}.

**Arity:**3

**Axioms:**

(= (Logorc1 ?X ?Y) (Logior (Lognot ?X) ?Y))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (logorc2 $tau_1$ $tau_2$)} is equivalent to {tt (logior $tau_1$ (lognot $tau_2$))}.

**Arity:**3

**Axioms:**

(= (Logorc2 ?X ?Y) (Logior ?X (Lognot ?Y)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Axioms:**

(Undefined (Arity Logxor))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (max $tau_1 ldots tau_k$)} denotes the largest object denoted by $tau_1$ through $tau_n$.

**Axioms:**

(Undefined (Arity Max))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (min $tau_1 ldots tau_k$)} denotes the smallest object denoted by $tau_1$ through $tau_n$.

**Axioms:**

(Undefined (Arity Min))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (numerator $tau$)} denotes the numerator of the canonical reduced form of the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (phase $tau$)} denotes the angle part of the polar representation of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (rationalize $tau$)} denotes the rational representation of the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (realpart $tau$)} denotes the real part of the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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>}.

**Arity:**3

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Arity:**2**Range:**Integer

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Arity:**3

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (sin $tau$)} denotes the sine of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (sinh $tau$)} denotes the hyperbolic sine of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (sqrt $tau$)} denotes the principal square root of the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (tan $tau$)} denotes the tangent of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (tanh $tau$)} denotes the hyperbolic tangent of the object denoted by $tau$ (in radians).

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

The term {tt (truncate $tau$)} denotes the largest integer less than the object denoted by $tau$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

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$.

**Arity:**2

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

**Arity:**2**Inverse:**<

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

**Arity:**2

**Axioms:**

(<=> (=< ?X ?Y) (Or (= ?X ?Y) (< ?X ?Y)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

**Arity:**2

**Axioms:**

(<=> (>= ?X ?Y) (Or (> ?X ?Y) (= ?X ?Y)))

**Defined in theory: Kif-numbers****Source code: kif-ontology.lisp**

Formatting and translation code was written by