# Theory KIF-NUMBERS

The KIF vocabulary concerning numbers and arithmetic.

No theories were included by Kif-Numbers.

### Theories that include Kif-Numbers:

```    Kif-Ontology
Kif-Lists
Kif-Ontology
Kif-Meta
Configuration-Design
Vt-Design
Simple-Bikes
Vt-Domain
Vt-Example
Kif-Ontology
Kif-Relations
Frame-Ontology
Vt-Domain ...
Configuration-Design ...
Physical-Quantities
Unary-Scalar-Functions
Cml
Thermodynamics
Dme
Thermodynamics
Standard-Units
Simple-Bikes
Cml ...
Vt-Design ...
Unary-Scalar-Functions ...
Scalar-Quantities
Vt-Design ...
Vector-Quantities
Abstract-Algebra
Physical-Quantities ...
Jat-Generic
Generic-Bibliography
Slot-Constraint-Sugar
Generic-Bibliography
Kif-Ontology```

### 13 classes defined:

```    Number
Real-Number
Rational-Number
Integer
Even-Integer
Odd-Integer
Natural
Positive-Integer
Nonnegative-Integer
Positive
Negative
Complex-Number
Zero```

### 2 instances defined:

The following constants were used from theories not included:

All constants that were mentioned were defined.

Number

## Class REAL-NUMBER

Real number
Subclass-Of: Number

## Class RATIONAL-NUMBER

Rational number
Subclass-Of: Real-number
Axioms:
```(<=> (Rational-Number ?X)
(And (Real-Number ?X)
(Exists (?Y) (And (Integer ?Y) (Integer (* ?X ?Y)))) ))

```

## Class INTEGER

Integer
Subclass-Of: Rational-number

## Class EVEN-INTEGER

Even integer
Subclass-Of: Integer
Axioms:
```(=> (Even-Integer ?X) (= (Mod ?X 2) 0))

```

## Class ODD-INTEGER

Odd integer
Subclass-Of: Integer
Axioms:
```(=> (Odd-Integer ?X) (= (Mod ?X 2) 1))

```

## Class NATURAL

Natural number
Subclass-Of: Integer

Slots Of Instances:

>: 0
Axioms:
```(<=> (Natural ?X) (And (Integer ?X) (> ?X 0)))

```

## Class POSITIVE-INTEGER

An integer greater than zero, not including zero. A less ambiguous name for KIF's NATURAL.
Subclass-Of: Integer

Slots Of Instances:

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

```

## Class NONNEGATIVE-INTEGER

Nonnegative integer
Subclass-Of: Integer

Slots Of Instances:

>=: 0

## Class POSITIVE

Positive number
Subclass-Of: Number

Slots Of Instances:

>: 0

## Class NEGATIVE

Negative number
Subclass-Of: Number

Slots Of Instances:

<: 0

## Class COMPLEX-NUMBER

Complex number
Subclass-Of: Number

## Class ZERO

The class containing 0. May be used as a predicate.
Axioms:
```(<=> (Zero ?X) (= ?X 0))

```

## Relation LOGBIT

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

## Relation LOGTEST

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

## Function *

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 *))

```

## Function +

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 +))

```

## Function -

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

```

## Function /

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 /))

```

## Function 1+

The term {tt (1+ \$tau\$)} denotes the sum of the object denoted by \$tau\$ and 1.
Arity: 2
Axioms:
```(= (1+ ?X) (+ ?X 1))

```

## Function 1-

The term {tt (1- \$tau\$)} denotes the difference of the object denoted by \$tau\$ and 1.
Arity: 2
Axioms:
```(= (1- ?X) (- ?X 1))

```

## Function ABS

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

```

## Function ACOS

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

## Function ACOSH

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

## Function ASH

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

## Function ASIN

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

## Function ASINH

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

## Function ATAN

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

## Function ATANH

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

## Function BOOLE

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

## Function CEILING

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

## Function CIS

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

```

## Function CONJUGATE

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

## Function COS

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

## Function COSH

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

## Function DECODE-FLOAT

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

## Function DENOMINATOR

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

## Function EXP

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

```

## Real-number THE-EXPONENTIATION-CONSTANT-E

The constant often called 'e' using in exponentiation.
Instance-Of: Real-number

## Function EXPT

{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

## Function FCEILING

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

## Function FFLOOR

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

## Function FLOAT

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

## Function FLOAT-DIGITS

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

## Function FLOAT-PRECISION

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

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

## Function FLOAT-SIGN

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

## Function FLOOR

The term {tt (floor \$tau\$)} denotes the largest integer less than the object denoted by \$tau\$.
Arity: 2
Range: Integer

## Function FROUND

The term {tt (fround \$tau\$)} is equivalent to {tt (ffloor (+ 0.5 \$tau\$))}.
Arity: 2
Axioms:
```(= (Fround ?X) (Ffloor (+ 0.5 ?X)))

```

## Function FTRUNCATE

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

## Function GCD

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

## Function IMAGPART

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

## Function INTEGER-DECODE-FLOAT

The term {tt (integer-decode-float \$tau\$)} denotes the significand of the object denoted by \$tau\$.
Arity: 2
Range: Integer

## Function INTEGER-LENGTH

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

## Function ISQRT

The term {tt (isqrt \$tau\$)} denotes the integer square root of the object denoted by \$tau\$.
Arity: 2
Range: Nonnegative-integer

## Function LCM

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

```

## Function LOG

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

## Function LOGAND

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

```

## Function LOGANDC1

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

```

## Function LOGANDC2

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

```

## Function LOGCOUNT

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

## Function LOGEQV

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

```

## Function LOGIOR

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

```

## Function LOGNAND

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

```

## Function LOGNOR

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

```

## Function LOGNOT

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

## Function LOGORC1

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

```

## Function LOGORC2

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

```

## Function LOGXOR

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

```

## Function MAX

The term {tt (max \$tau_1 ldots tau_k\$)} denotes the largest object denoted by \$tau_1\$ through \$tau_n\$.
Axioms:
```(Undefined (Arity Max))

```

## Function MIN

The term {tt (min \$tau_1 ldots tau_k\$)} denotes the smallest object denoted by \$tau_1\$ through \$tau_n\$.
Axioms:
```(Undefined (Arity Min))

```

## Function MOD

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

## Function NUMERATOR

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

## Function PHASE

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

## Function RATIONALIZE

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

## Function REALPART

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

## Function REM

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

## Function ROUND

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

## Function SCALE-FLOAT

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

## Function SIGNUM

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

## Function SIN

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

## Function SINH

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

## Function SQRT

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

## Function TAN

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

## Function TANH

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

## Function TRUNCATE

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

## Relation <

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

Arity: 2
Inverse: <

## Relation =<

Arity: 2
Axioms:
```(<=> (=< ?X ?Y) (Or (= ?X ?Y) (< ?X ?Y)))

```

## Relation >=

Arity: 2
Axioms:
```(<=> (>= ?X ?Y) (Or (> ?X ?Y) (= ?X ?Y)))

```

This document was generated using Ontolingua.
Formatting and translation code was written by
François Gerbaux and Tom Gruber