The KIF vocabulary concerning numbers and arithmetic.
No theories were included by 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
Job-Assignment-Task
Generic-Bibliography
Slot-Constraint-Sugar
Generic-Bibliography
Kif-Ontology
Number
Real-Number
Rational-Number
Integer
Even-Integer
Odd-Integer
Natural
Positive-Integer
Nonnegative-Integer
Positive
Negative
Complex-Number
Zero
The following constants were used from theories not included:
All constants that were mentioned were defined.
Number
Real number
Rational number
(<=> (Rational-Number ?X)
(And (Real-Number ?X)
(Exists (?Y) (And (Integer ?Y) (Integer (* ?X ?Y)))) ))
Integer
Even integer
(=> (Even-Integer ?X) (= (Mod ?X 2) 0))
Odd integer
(=> (Odd-Integer ?X) (= (Mod ?X 2) 1))
Natural number
Slots Of Instances:
(<=> (Natural ?X) (And (Integer ?X) (> ?X 0)))
An integer greater than zero, not including zero. A less ambiguous name for KIF's NATURAL.
Slots Of Instances:
(<=> (Positive-Integer ?X) (And (Integer ?X) (> ?X 0)))
Nonnegative integer
Slots Of Instances:
Positive number
Slots Of Instances:
Negative number
Slots Of Instances:
Complex number
The class containing 0. May be used as a predicate.
(<=> (Zero ?X) (= ?X 0))
The sentence {tt (logbit $tau_1$ $tau_2$)} is true if bit $tau_2$ of $tau_1$ is 1.
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.
If $tau_1$, ..., $tau_n$ denote numbers, then the term {tt (* $tau_1 ldots tau_n$)} denotes the product of those numbers.
(Undefined (Arity *))
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.
(Undefined (Arity +))
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$.
(Undefined (Arity -))
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$.
(Undefined (Arity /))
The term {tt (1+ $tau$)} denotes the sum of the object denoted by $tau$ and 1.
(= (1+ ?X) (+ ?X 1))
The term {tt (1- $tau$)} denotes the difference of the object denoted by $tau$ and 1.
(= (1- ?X) (- ?X 1))
The term {tt (abs $tau$)} denotes the absolute value of the object denoted by $tau$.
(= (Abs ?X) (If (>= ?X 0) ?X (- ?X)))
If $tau$ denotes a number, then the term {tt (acos $tau$)} denotes the arc cosine of that number (in radians).
The term {tt (acosh $tau$)} denotes the arc cosine of the object denoted by $tau$ (in radians).
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$).
The term {tt (asin $tau$)} denotes the arc sine of the object denoted by $tau$ (in radians).
The term {tt (asinh $tau$)} denotes the hyperbolic arc sine of the object denoted by $tau$ (in radians).
The term {tt (atan $tau$)} denotes the arc tangent of the object denoted by $tau$ (in radians).
The term {tt (atanh $tau$)} denotes the hyperbolic arc tangent of the object denoted by $tau$ (in radians).
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$.
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$.
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.
(=> (Cis ?Radians ?Complex) (Not (Complex-Number ?Radians)))
If $tau$ denotes a complex number, then the term {tt (conjugate $tau$)} denotes the complex conjugate of the number denoted by $tau$.
The term {tt (cos $tau$)} denotes the cosine of the object denoted by $tau$ (in radians).
The term {tt (cosh $tau$)} denotes the hyperbolic cosine of the object denoted by $tau$ (in radians).
The term {tt (decode-float $tau$)} denotes the mantissa of the object denoted by $tau$.
The term {tt (denominator $tau$)} denotes the denominator of the canonical reduced form of the object denoted by $tau$.
The term {tt (exp $tau$)} denotes $e$ raised to the power the object denoted by $tau$.
(= (Exp ?X) (Expt The-Exponentiation-Constant-E ?X))
The constant often called 'e' using in exponentiation.
{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$.}
The term {tt (fceiling $tau$)} denotes the smallest integer (as a floating point number) greater than the object denoted by $tau$.
The term {tt (ffloor $tau$)} denotes the largest integer (as a floating point number) less than the object denoted by $tau$.
The term {tt (float $tau$)} denotes the floating point number equal to the object denoted by $tau$.
The term {tt (float-digits $tau$)} denotes the number of digits used in the representation of a floating point number denoted by $tau$.
The term {tt (float-precision $tau$)} denotes the number of significant digits in the floating point number denoted by $tau$.
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.
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$.
The term {tt (floor $tau$)} denotes the largest integer less than the object denoted by $tau$.
The term {tt (fround $tau$)} is equivalent to {tt (ffloor (+ 0.5 $tau$))}.
(= (Fround ?X) (Ffloor (+ 0.5 ?X)))
The term {tt (ftruncate $tau$)} denotes the largest integer (as a floating point number) less than the object denoted by $tau$.
The term {tt (gcd $tau_1 ldots tau_n$)} denotes the greatest common divisor of the objects denoted by $tau_1$ through $tau_n$.
The term {tt (imagpart $tau$)} denotes the imaginary part of the object denoted by $tau$.
The term {tt (integer-decode-float $tau$)} denotes the significand of the object denoted by $tau$.
The term {tt (integer-length $tau$)} denotes the number of bits required to store the absolute magnitude of the object denoted by $tau$.
The term {tt (isqrt $tau$)} denotes the integer square root of the object denoted by $tau$.
The term {tt (lcm $tau_1 ldots tau_n$)} denotes the least common multiple of the objects denoted by $tau_1,ldots,tau_n$.
(Undefined (Arity Lcm))
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$.
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$.
(Undefined (Arity Logand))
The term {tt (logandc1 $tau_1$ $tau_2$)} is equivalent to {tt (logand (lognot $tau_1$) $tau_2$)}.
(= (Logandc1 ?X ?Y) (Logand (Lognot ?X) ?Y))
The term {tt (logandc2 $tau_1$ $tau_2$)} is equivalent to {tt (logand $tau_1$ (lognot $tau_2$))}.
(= (Logandc2 ?X ?Y) (Logand ?X (Lognot ?Y)))
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.
The term {tt (logeqv $tau_1 ldots tau_n$)} denotes the logical-exclusive-or of the objects denoted by $tau_1,ldots,tau_n$.
(Undefined (Arity Logeqv))
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.
(Undefined (Arity Logior))
The term {tt (lognand $tau_1$ $tau_2$)} is equivalent to {tt (lognot (logand $tau_1$ $tau_2$))}.
(= (Lognand ?X ?Y) (Lognot (Logand ?X ?Y)))
The term {tt (lognor $tau_1$ $tau_2$)} is equivalent to {tt (lognot (logior $tau_1$ $tau_2$))}.
(= (Lognor ?X ?Y) (Lognot (Logior ?X ?Y)))
The term {tt (lognot $tau$)} denotes the bit-wise logical not of the object denoted by $tau$.
The term {tt (logorc1 $tau_1$ $tau_2$)} is equivalent to {tt (logior (lognot $tau_1$) $tau_2$)}.
(= (Logorc1 ?X ?Y) (Logior (Lognot ?X) ?Y))
The term {tt (logorc2 $tau_1$ $tau_2$)} is equivalent to {tt (logior $tau_1$ (lognot $tau_2$))}.
(= (Logorc2 ?X ?Y) (Logior ?X (Lognot ?Y)))
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.
(Undefined (Arity Logxor))
The term {tt (max $tau_1 ldots tau_k$)} denotes the largest object denoted by $tau_1$ through $tau_n$.
(Undefined (Arity Max))
The term {tt (min $tau_1 ldots tau_k$)} denotes the smallest object denoted by $tau_1$ through $tau_n$.
(Undefined (Arity Min))
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$.
The term {tt (numerator $tau$)} denotes the numerator of the canonical reduced form of the object denoted by $tau$.
The term {tt (phase $tau$)} denotes the angle part of the polar representation of the object denoted by $tau$ (in radians).
The term {tt (rationalize $tau$)} denotes the rational representation of the object denoted by $tau$.
The term {tt (realpart $tau$)} denotes the real part of the object denoted by $tau$.
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>}.
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.
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$.
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.
The term {tt (sin $tau$)} denotes the sine of the object denoted by $tau$ (in radians).
The term {tt (sinh $tau$)} denotes the hyperbolic sine of the object denoted by $tau$ (in radians).
The term {tt (sqrt $tau$)} denotes the principal square root of the object denoted by $tau$.
The term {tt (tan $tau$)} denotes the tangent of the object denoted by $tau$ (in radians).
The term {tt (tanh $tau$)} denotes the hyperbolic tangent of the object denoted by $tau$ (in radians).
The term {tt (truncate $tau$)} denotes the largest integer less than the object denoted by $tau$.
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$.
(<=> (=< ?X ?Y) (Or (= ?X ?Y) (< ?X ?Y)))
(<=> (>= ?X ?Y) (Or (> ?X ?Y) (= ?X ?Y)))