;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-
;;; The KIF ontology is composed of a family of theories, corresponding
;;; roughly to chapters in the specification.
;;; We define them as theories in this file, first giving their
;;; theory relationships and then the definitions in each theory
;;; in sequence. In practice we maintain each theory in a separate
;;; file; they are merged here for convenience.
;;; 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-theory KIF-SETS ()
"The KIF vocabulary for set theory as defined in the KIF 3.0 specification."
)
(define-theory KIF-NUMBERS ()
"The KIF vocabulary concerning numbers and arithmetic."
)
(define-theory KIF-LISTS (kif-numbers)
"The KIF vocabulary for lists as defined in the KIF 3.0 specification."
)
(define-theory KIF-RELATIONS (kif-sets kif-lists)
"The KIF vocabulary concerning relations and functions."
)
(define-theory KIF-META (kif-sets kif-lists)
"The KIF vocabulary for representing metalinguistic knowledge."
)
(define-theory KIF-ONTOLOGY (KIF-SETS
KIF-LISTS
KIF-NUMBERS
KIF-RELATIONS
KIF-META
)
"The ontology of KIF vocabulary defined in the KIF 3.0 specification.
It consists of the union of other theories corresponding the chapters
in specification document."
)
(in-theory 'kif-sets)
(define-class SET (?x)
"A set is a collection of objects, both individuals and sets of
various sorts. It is a KIF primitive."
:axiom-def (exhaustive-subclass-partition SET
(setof simple-set proper-set)))
(define-class BOUNDED (?x)
"Something that can be a member of a set."
:iff-def (forall ?bounded-object
(member ?x (setofall ?bounded-object true))))
(define-class UNBOUNDED (?x)
"Something in the universe of discourse that can't be a member of a set.
Paradoxical beasts go here."
:iff-def (not (bounded ?x)))
(define-relation MEMBER (?element ?set)
"The sentence {\tt (member $\tau_1$ $\tau_2$)} is true if and only if the
object denoted by $\tau_1$ is contained in the set denoted by $\tau_2$.
As mentioned above, an object can be a member of another object if and only
if the former is bounded and the latter is a set."
:def (and (bounded ?element)
(set ?set)))
(define-function SETOF (@members) :-> ?set
"SETOF is the set constructor function for KIF. It takes any finite
number of arguments and denotes the set of those things."
:def (set ?set))
(define-axiom EXTENSIONALITY-PROPERTY-OF-SETS
"Two sets are identical if and only if they have the same members."
:= (=> (and (set ?s1) (set ?s2))
(<=> (forall (?x) (<=> (member ?x ?s1) (member ?x ?s2)))
(= ?s1 ?s2))))
(define-class INDIVIDUAL (?x)
"An individual is something that is not a set."
:iff-def (not (set ?x))
:issues ("Disjointness with SET is defined with THING,
but repeated here for clarity."))
(define-class SIMPLE-SET (?x)
"A simple set is a set that can be a member of another set."
:def (set ?x))
(define-class PROPER-SET (?x)
"A proper set is a set that cannot be a member of another set."
:def (set ?x))
(define-relation EMPTY (?x)
"True of the empty set."
:iff-def (= ?x (setof)))
(define-function CARDINALITY (?set) :-> ?integer
:iff-def (and (set ?set)
(integer ?integer)
(exists @elements
(and (= ?set (setof @elements))
(= ?integer (length (listof @elements)))))))
(define-class FINITE-SET (?f-set)
"A set that has only finite elements"
:iff-def (and (set ?f-set)
(exists @elements
(= ?f-set (setof @elements))))
:issues ("not explicitly defined in the KIF spec"))
(define-function UNION (@sets) :-> ?set
:lambda-body (setofall ?x
(exists ?s
(and (item ?s (listof @sets))
(member ?x ?s))))
:def (and (=> (item ?s (listof @sets))
(set ?s))
(set ?set)))
(define-function INTERSECTION (@sets) :-> ?set
:lambda-body (setofall ?x
(exists ?s
(=> (item ?s (listof @sets))
(member ?x ?s))))
:def (and (=> (item ?s (listof @sets))
(set ?s))
(set ?set)))
(define-function DIFFERENCE (?set @sets) :-> ?diff-set
:lambda-body (setofall ?x
(and (member ?x ?set)
(forall ?s
(=> (item ?s (listof @sets))
(not (member ?x ?s))))))
:def (and (=> (item ?s (listof @sets))
(set ?s))
(set ?set)
(set ?diff-set)))
(define-function COMPLEMENT (?s) :-> ?set
:lambda-body (setofall ?x (not (member ?x ?s)))
:def (and (set ?s) (set ?set)))
(define-function GENERALIZED-UNION (?set-of-sets) :-> ?set
:lambda-body (setofall ?x
(exists (?s)
(and (member ?s ?set-of-sets) (member ?x ?s))))
:def (and (set ?set-of-sets)
(forall (?s) (=> (member ?s ?set-of-sets) (set ?s)))
(set ?set)))
(define-function GENERALIZED-INTERSECTION (?set-of-sets) :-> ?set
:lambda-body (setofall ?x
(exists (?s)
(=> (member ?s ?set-of-sets)
(member ?x ?s))))
:def (and (set ?set-of-sets)
(forall (?s) (=> (member ?s ?set-of-sets) (set ?s)))
(set ?set)))
(define-relation SUBSET (?s1 ?s2)
"The sentence {\tt (subset $\tau_1$ $\tau_2$)} is true if
and only if $\tau_1$ and $\tau_2$ are sets and the objects in the set
denoted by $\tau_1$ are contained in the set denoted by $\tau_2$."
:iff-def (and (set ?s1) (set ?s2)
(forall ?x (=> (member ?x ?s1) (member ?x ?s2)))))
(define-relation PROPER-SUBSET (?s1 ?s2)
"The sentence {\tt (proper-subset $\tau_1$ $\tau_2$)} is true if
the set denoted by $\tau_1$ is a subset of the set denoted by $\tau_2$
but not vice-versa."
:iff-def (and (subset ?s1 ?s2)
(not (subset ?s2 ?s1))))
(define-relation DISJOINT (?s1 ?s2)
"Two sets are disjoint if and only if there is no object that is a
member of both sets."
:iff-def (empty (intersection ?s1 ?s2)))
(define-relation PAIRWISE-DISJOINT (@sets)
"Sets are pairwise-disjoint if and only if every
set is disjoint from every other set."
:iff-def (forall (?s1 ?s2)
(=> (item ?s1 (listof @sets))
(item ?s2 (listof @sets))
(or (= ?s1 ?s2) (disjoint ?s1 ?s2)))))
(define-relation MUTUALLY-DISJOINT (@sets)
"Sets are mutually-disjoint if and only if there is no object that
is a member of all of the sets."
:iff-def (empty (intersection @sets)))
(define-relation SET-PARTITION (?s @sets)
:iff-def (and (= ?s (union @sets))
(pairwise-disjoint @sets)))
(define-relation SET-COVER (?s @sets)
:iff-def (subset ?s (union @sets)))
(define-axiom AXIOM-OF-REGULARITY
"every non-empty set has an element with which it has no members in
common."
:= (forall (?s)
(=> (not (empty ?s))
(exists (?u) (and (member ?u ?s) (disjoint ?u ?s))))))
(define-axiom AXIOM-OF-CHOICE
"There is a set that associates every bounded set with a
distinguished element of that set. In effect, it {\it chooses} an
element from every bounded set."
:= (exists (?s)
(and (set ?s)
(forall (?x) (=> (member ?x ?s) (double ?x)))
(forall (?x ?y ?z) (=> (and (member (listof ?x ?y) ?s)
(member (listof ?x ?z) ?s))
(= ?y ?z)))
(forall (?u)
(=> (and (bounded ?u) (not (empty ?u)))
(exists (?v) (and (member ?v ?u)
(member (listof ?u ?v) ?s))))))))
(define-axiom FINITE-SET-AXIOM
"Any finite set of bounded sets is itself a bounded set."
:= (=> (finite-set ?s) (bounded ?s)))
(define-axiom SUBSET-AXIOM
"The set of all of subsets of a bounded set is also a bounded set."
:= (=> (bounded ?v) (bounded (setofall ?u (subset ?u ?v)))))
(define-axiom UNION-AXIOM
:= (=> (and (bounded ?u) (forall (?x) (=> (member ?x ?u) (bounded ?x))))
(bounded (generalized-union ?u))))
(define-axiom INTERSECTION-AXIOM
"The intersection of a bounded set and any other set is a bounded
set. So long as one of the sets defining the intersection is bounded,
the resulting set is bounded."
:= (=> (and (bounded ?u) (set ?s))
(bounded (intersection ?u ?s))))
(define-axiom AXIOM-OF-INFINITY
"There is a bounded set containing a set, a set that properly
contains that set, a third set that properly contains the second set,
and so forth. In short, there is at least one bounded set of infinite
cardinality."
:= (exists (?u)
(and (bounded ?u)
(not (empty ?u))
(forall (?x)
(=> (member ?x ?u)
(exists (?y) (and (member ?y ?u)
(proper-subset ?x ?y))))))))
;;; Equality is built in to KIF; these are operators.
;;; However, it helps to have them be proper relations in the ontology.
;;; For instance, other relations may be subsumed by them in a taxonomy.
;;; We put the equality relations in the SET ontology, because it is
;;; the most primitive ontology in KIF and equality is intrinsic to
;;; the definition of set membership.
(define-relation = (?x ?y)
"= is the equality relation for KIF. It is defined as an operator,
but is in practice like every other relation. Two things are = to
each other if they are exactly the same thing. How these two things
are denoted in some theory is an entirely different issue.
= is an operator in KIF.")
(define-relation /= (?x ?y)
"/= means not equal. It is a KIF operator."
:iff-def (not (= ?x ?y)))
(in-theory 'kif-numbers)
(define-class NUMBER (?x)
"Number")
(define-class REAL-NUMBER (?x)
"Real number"
:def (number ?x))
(define-class RATIONAL-NUMBER (?x)
"Rational number"
:iff-def (and (real-number ?x)
(exists (?y)
(and (integer ?y)
(integer (* ?x ?y))))))
(define-class INTEGER (?x)
"Integer"
:def (rational-number ?x))
(define-class EVEN-INTEGER (?x)
"Even integer"
:def (and (integer ?x)
(= (mod ?x 2) 0)))
(define-class ODD-INTEGER (?x)
"Odd integer"
:def (and (integer ?x)
(= (mod ?x 2) 1)))
(define-class NATURAL (?x)
"Natural number"
:iff-def (and (integer ?x)
(> ?x 0)))
;;; POSITIVE-INTEGER is only proposed, is not in the 3.0 spec:
(define-class POSITIVE-INTEGER (?x)
"An integer greater than zero, not including zero.
A less ambiguous name for KIF's NATURAL."
:iff-def (and (integer ?x)
(> ?x 0)))
(define-class NONNEGATIVE-INTEGER (?x)
"Nonnegative integer"
:def (and (integer ?x)
(>= ?x 0)))
(define-class POSITIVE (?x)
"Positive number"
:def (and (number ?x)
(> ?x 0)))
(define-class NEGATIVE (?x)
"Negative number"
:def (and (number ?x)
(< ?x 0)))
(define-class COMPLEX-NUMBER (?x)
"Complex number"
:def (number ?x))
(define-class ZERO (?x)
"The class containing 0. May be used as a predicate."
:iff-def (= ?x 0))
(define-relation LOGBIT (?x ?y)
"The sentence {\tt (logbit $\tau_1$ $\tau_2$)} is true if bit $\tau_2$
of $\tau_1$ is 1.")
(define-relation LOGTEST (?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-function 1+ (?x) :-> ?result
"The term {\tt (1+ $\tau$)} denotes the sum of the object denoted by
$\tau$ and 1."
:lambda-body (+ ?x 1))
(define-function 1- (?x) :-> ?result
"The term {\tt (1- $\tau$)} denotes the difference of the object denoted by
$\tau$ and 1."
:lambda-body (- ?x 1))
(define-function ABS (?x)
"The term {\tt (abs $\tau$)} denotes the absolute value of the object
denoted by $\tau$. "
:lambda-body (if (>= ?x 0) ?x (- ?x)))
(define-function ACOS (?x)
"If $\tau$ denotes a number, then the term {\tt (acos $\tau$)} denotes
the arc cosine of that number (in radians).")
(define-function ACOSH (?x)
"The term {\tt (acosh $\tau$)} denotes the arc cosine of the
object denoted by $\tau$ (in radians).")
(define-function ASH (?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-function ASIN (?x)
"The term {\tt (asin $\tau$)} denotes the arc sine of the object
denoted by $\tau$ (in radians).")
(define-function ASINH (?x)
"The term {\tt (asinh $\tau$)} denotes the hyperbolic arc sine of the object denoted by $\tau$ (in radians).")
(define-function ATAN (?x)
"The term {\tt (atan $\tau$)} denotes the arc tangent of the object
denoted by $\tau$ (in radians).")
(define-function ATANH (?x)
"The term {\tt (atanh $\tau$)} denotes the hyperbolic arc tangent
of the object denoted by $\tau$ (in radians).")
(define-function BOOLE (?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-function CEILING (?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-function CIS (?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-function CONJUGATE (?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-function COS (?x)
"The term {\tt (cos $\tau$)} denotes the cosine of the object
denoted by $\tau$ (in radians).")
(define-function COSH (?x)
"The term {\tt (cosh $\tau$)} denotes the hyperbolic cosine of the
object denoted by $\tau$ (in radians).")
(define-function DECODE-FLOAT (?x)
"The term {\tt (decode-float $\tau$)} denotes the mantissa of the
object denoted by $\tau$.")
(define-function DENOMINATOR (?x)
"The term {\tt (denominator $\tau$)} denotes the denominator of the
canonical reduced form of the object denoted by $\tau$.")
(define-function EXP (?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-instance the-exponentiation-constant-E (real-number)
"The constant often called 'e' using in exponentiation.")
(define-function EXPT (?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-function FCEILING (?x)
"The term {\tt (fceiling $\tau$)} denotes the smallest integer (as
a floating point number) greater than the object denoted by $\tau$.")
(define-function FFLOOR (?x)
"The term {\tt (ffloor $\tau$)} denotes the largest integer (as a floating point number) less than
the object denoted by $\tau$.")
(define-function FLOAT (?x)
"The term {\tt (float $\tau$)} denotes the floating point number
equal to the object denoted by $\tau$.")
(define-function FLOAT-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-function FLOAT-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-function FLOAT-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-function FLOAT-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-function FLOOR (?x) :-> ?integer
"The term {\tt (floor $\tau$)} denotes the largest integer less
than the object denoted by $\tau$."
:def (integer ?integer))
(define-function FROUND (?x)
"The term {\tt (fround $\tau$)} is equivalent to {\tt (ffloor (+ 0.5 $\tau$))}."
:lambda-body (ffloor (+ 0.5 ?x)))
(define-function FTRUNCATE (?x)
"The term {\tt (ftruncate $\tau$)} denotes the largest integer (as
a floating point number) less than the object denoted by $\tau$.")
(define-function GCD (?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-function IMAGPART (?x)
"The term {\tt (imagpart $\tau$)} denotes the imaginary part of the
object denoted by $\tau$.")
(define-function INTEGER-DECODE-FLOAT (?x) :-> ?integer
"The term {\tt (integer-decode-float $\tau$)} denotes the significand
of the object denoted by $\tau$."
:def (integer ?integer))
(define-function INTEGER-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-function ISQRT (?x) :-> ?integer
"The term {\tt (isqrt $\tau$)} denotes the integer square root of the
object denoted by $\tau$."
:def (nonnegative-integer ?integer))
(define-function LCM (@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-function LOG (?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-function LOGAND (@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-function LOGANDC1 (?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-function LOGANDC2 (?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-function LOGCOUNT (?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-function LOGEQV (@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-function LOGIOR (@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-function LOGNAND (?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-function LOGNOR (?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-function LOGNOT (?x)
"The term {\tt (lognot $\tau$)} denotes the bit-wise logical not of
the object denoted by $\tau$.")
(define-function LOGORC1 (?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-function LOGORC2 (?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-function LOGXOR (@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-function MAX (@args)
"The term {\tt (max $\tau_1 \ldots \tau_k$)} denotes the largest object
denoted by $\tau_1$ through $\tau_n$.")
(define-function MIN (@args)
"The term {\tt (min $\tau_1 \ldots \tau_k$)} denotes the smallest
object denoted by $\tau_1$ through $\tau_n$.")
(define-function MOD (?x)
"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-function NUMERATOR (?x)
"The term {\tt (numerator $\tau$)} denotes the numerator of the
canonical reduced form of the object denoted by $\tau$.")
(define-function PHASE (?x)
"The term {\tt (phase $\tau$)} denotes the angle part of the polar
representation of the object denoted by $\tau$ (in radians).")
(define-function RATIONALIZE (?x)
"The term {\tt (rationalize $\tau$)} denotes the rational
representation of the object denoted by $\tau$.")
(define-function REALPART (?x)
"The term {\tt (realpart $\tau$)} denotes the real part of the
object denoted by $\tau$.")
(define-function REM (?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-function ROUND (?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-function SCALE-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-function SIGNUM (?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-function SIN (?x)
"The term {\tt (sin $\tau$)} denotes the sine of the object denoted by $\tau$ (in radians).")
(define-function SINH (?x)
"The term {\tt (sinh $\tau$)} denotes the hyperbolic sine of the object denoted by $\tau$ (in radians).")
(define-function SQRT (?x)
"The term {\tt (sqrt $\tau$)} denotes the principal square root of the object denoted by $\tau$.")
(define-function TAN (?x)
"The term {\tt (tan $\tau$)} denotes the tangent of the object denoted by $\tau$ (in radians).")
(define-function TANH (?x)
"The term {\tt (tanh $\tau$)} denotes the hyperbolic tangent of the
object denoted by $\tau$ (in radians).")
(define-function TRUNCATE (?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)))
(in-theory 'kif-lists)
(define-class LIST (?x)
"A list is a sequence --- an ordered bag --- of elements.
It is KIF primitive.")
(define-class NULL (?list)
"True of the list with no items."
:iff-def (and (list ?list)
(= (length ?list) 0)))
(define-instance NIL (null)
"The list with no items, of length 0.
All null lists are equal to this object, called NIL.")
(define-function LISTOF (@items) :-> ?list
"LISTOF is the sequence constructor function for KIF. It takes any finite
number of arguments and denotes the list (i.e., sequence, tuple) of
those items.
LISTOF is an operator in KIF."
:def (list ?list))
(define-relation SINGLE (?list)
"A list of length 1."
:iff-def (and (list ?list)
(= (length ?list) 1)))
(define-relation DOUBLE (?list)
"A list of length 2."
:iff-def (and (list ?list)
(= (length ?list) 2)))
(define-relation TRIPLE (?list)
"A list of length 3."
:iff-def (and (list ?list)
(= (length ?list) 3)))
(define-function FIRST (?list)
:def (list ?list)
:lambda-body (if (exists @items
(= (listof ?x @items) ?list))
?x))
;;; THIS IS NOT IN THE 3.0 SPEC!
(define-function SECOND (?list)
"the SECOND of a list is the second item in the list.
It is undefined if the length of the list is not at least 2."
:def (list ?list)
:lambda-body (first (rest ?list)))
(define-function REST (?list) :-> ?rest-list
:iff-def (or (and (null ?list)
(= ?rest-list ?list))
(exists (?x @items)
(and (= ?list (listof ?x @items))
(= ?rest-list (listof @items))))))
(define-function LAST (?list)
:def (list ?list)
:lambda-body (cond ((null ?list) bottom)
((null (rest ?list)) (first ?list))
(true (last (rest ?list)))))
(define-function BUTLAST (?list)
:lambda-body (cond ((null ?list) bottom)
((null (rest ?list)) nil)
(true (cons (first ?list) (butlast (rest ?list))))))
(define-relation ITEM (?x ?list)
"The sentence {\tt (item $\tau_1$ $\tau_2$)} is true if and only if
the object denoted by $\tau_2$ is a non-empty list and the object
denoted by $\tau_1$ is either the first item of that list or an item in
the rest of the list."
:def (and (list ?list)
(not (null ?list))
(or (= ?x (first ?list)) (item ?x (rest ?list)))))
(define-relation SUBLIST (?l1 ?l2)
"The sentence {\tt (sublist $\tau_1$ $\tau_2$)} is true if and only if
the object denoted by $\tau_1$ is a final segment of the list denoted by
$\tau_2$."
:def (and (list ?l1)
(list ?l2)
(or (= ?l1 ?l2)
(sublist ?l1 (rest ?l2)))))
(define-function CONS (?x ?list) :-> ?new-list
"The function {\tt cons} adds the object specified as its first
argument to the front of the list specified as its second argument."
:def (and (list ?list)
(list ?new-list))
:lambda-body (if (= ?list (listof @l)) (listof ?x @l)))
(define-function APPEND (?l1 ?l2) :-> ?new-list
"The function {\tt append} adds the items in the list specified as its first
argument to the list specified as its second argument. ."
:def (and (list ?l1)
(list ?l2)
(list ?new-list))
:lambda-body (if (null ?l1)
(if (list ?l2) ?l2)
(cons (first ?l1) (append (rest ?l1) ?l2))))
(define-function REVAPPEND (?l1 ?l2) :-> ?new-list
"The function {\tt revappend} is similar to append, except that it
adds the items in reverse order."
:def (and (list ?l1)
(list ?l2)
(list ?new-list))
:lambda-body (if (null ?l1)
(if (list ?l2) ?l2)
(revappend (rest ?l1) (cons (first ?l1) ?l2))))
(define-function REVERSE (?list) :-> ?new-list
"The function {\tt reverse} produces a list in which the order of items is the
reverse of that in the list supplied as its single argument."
:def (and (list ?list)
(list ?new-list))
:lambda-body (revappend ?list (listof)))
(define-function ADJOIN (?x ?list) :-> ?new-list
"The functions {\tt adjoin} and {\tt remove} construct lists by adding or
removing objects from the lists specified as their arguments."
:def (and (list ?list)
(list ?new-list))
:lambda-body (if (item ?x ?list) ?list (cons ?x ?list)))
(define-function REMOVE (?x ?list) :-> ?new-list
"The functions {\tt adjoin} and {\tt remove} construct lists by adding or
removing objects from the lists specified as their arguments."
:def (and (list ?list)
(list ?new-list))
:lambda-body (cond ((null ?list) nil)
((and (= ?x (first ?list)) (list ?list))
(remove ?x (rest ?list)))
((list ?list) (cons ?x (remove ?x (rest ?list))))))
(define-function SUBST (?x ?y ?z)
"The value of {\tt subst} is the object or list obtained by
substituting the object supplied as first argument for all occurrences
of the object supplied as second argument in the object or list
supplied as third argument."
:lambda-body (cond ((= ?y ?z) ?x)
((null ?z) nil)
((list ?z) (cons (subst ?x ?y (first ?z))
(subst ?x ?y (rest ?z))))
(true ?z)))
(define-function LENGTH (?list) :-> ?n
"The function constant {\tt length} gives the number of items in a list."
:def (and (list ?list)
(nonnegative-integer ?n))
:lambda-body (cond ((null ?list) 0)
((list ?list) (1+ (length (rest ?list))))))
(define-function NTH (?list ?n)
"{\tt nth} returns the item in the list specified as its first
argument in the position specified as its second argument."
:def (and (list ?list)
(natural ?n))
:lambda-body (cond ((= ?n 1) (first ?list))
((positive ?n) (nth (rest ?list) (1- ?n)))))
(define-function NTHREST (?list ?n) :-> ?new-list
"{\tt nthrest} returns the list specified as its first argument
minus the first $n$ items, where $n$ is the number specified as its
second argument."
:def (and (list ?list)
(natural ?n)
(list ?new-list))
:lambda-body (cond ((= ?n 0) (if (list ?list) ?list))
((positive ?n)) (nthrest (rest ?list) (1- ?n))))
;;; STRING IS NOT IN THE KIF3.0 SPEC! It's proposed in kif-extensions.lisp
(define-class STRING (?s)
"A string is a sequence of characters."
:def (list ?s))
(in-theory 'kif-relations)
;;; Functions and relations are defined in the frame ontology.
;;; Inserted here for completeness.
;;; REDEFINED-IN-FRAME-ONTOLOGY!
(define-class RELATION (?r)
:iff-def (and (set ?r)
(forall ?x
(=> (member ?x ?r)
(list ?x)))))
;;; REDEFINED-IN-FRAME-ONTOLOGY!
(define-class FUNCTION (?f)
:iff-def (and (relation ?f)
(forall (?l ?m)
(=> (member ?l ?f)
(member ?m ?f)
(= (butlast ?l) (butlast ?m))
(= (last ?l) (last ?m))))))
(define-instance BOTTOM (undefined)
"The unique object which is the value of functions when
applied to arguments on which they are not defined.")
;;; UNDEFINED is not in the 3.0 spec, but is proposed
(define-relation UNDEFINED (?value)
"True of terms denoting the bottom object,
usually meaning that a function is undefined
on given arguments. There is exactly one
object in the universe of discourse that is
undefined, called BOTTOM. Functional terms that
are undefined are equal to this special element."
:iff-def (= ?value BOTTOM))
;;; DEFINED is not in the 3.0 spec, but is proposed
(define-relation DEFINED (?x)
"A term is defined if it does not denote the undefined object,
called bottom. (defined (F x)) means that the function F is
defined for the object x. (F x) denotes its value. In relational
terminology, (defined (F x)) means (exists ?y (F x ?y))."
:iff-def (not (undefined ?x)))
(define-relation HOLDS (?r @args)
"If $\tau$ denotes a relation, then the sentence
{\tt (holds $\tau$ $\tau_1$ ... $\tau_k$)} is true if and only if
the list of objects denoted by $\tau_1$,...,$\tau_k$ is a member of
that relation."
:iff-def (and (relation ?r)
(member (listof @args) ?r)))
(define-function VALUE (?f @args)
"If $\tau$ denotes a function with a value for the objects denoted by
$\tau_1$,..., $\tau_k$, then the term {\tt (value $\tau$ $\tau_1$ ...
$\tau_k$)} denotes the value of applying that function to the objects
denoted by $\tau_1$,...,$\tau_k$. Otherwise, the value is undefined."
:lambda-body (if (and (function ?f)
(member ?list ?f)
(= (butlast ?list) (listof @args)))
(last ?list)))
;; IDENTITY is not in the 3.0 spec, but is proposed
(define-function IDENTITY (?x)
"The value of the identity function is just its argument.")
(define-function APPLY (?f ?list)
:lambda-body (if (and (function ?f) (= ?list (listof @args)))
(value ?f @args)))
(define-function MAP (?f ?list)
:lambda-body (if (null ?list)
(listof)
(cons (value ?f (first ?list))
(map ?f (rest ?list)))))
(define-function UNIVERSE (?r) :-> ?set
"The universe of a relation is the set of all objects occurring in some
list contained in that relation."
:lambda-body (if (relation ?r)
(setofall ?x
(exists (?list) (and (member ?list ?r)
(item ?x ?list))))))
;;; REDEFINED-IN-FRAME-ONTOLOGY!
(define-relation UNARY-RELATION (?r)
"A unary relation is a non-empty relation in which all lists have
exactly one item."
:iff-def (and (relation ?r)
(not (empty ?r))
(forall (?list) (=> (member ?list ?r) (single ?list)))))
;;; REDEFINED-IN-FRAME-ONTOLOGY!
(define-relation BINARY-RELATION (?r)
"A binary relation is a non-empty relation in which all lists have
exactly two items."
:iff-def (and (relation ?r)
(not (empty ?r))
(forall (?list) (=> (member ?list ?r) (double ?list)))))
;;; REDEFINED-IN-FRAME-ONTOLOGY!
(define-function INVERSE (?r) :-> ?relation
"The inverse of a binary relation is a binary relation with all
tuples reversed."
:lambda-body (if (binary-relation ?r)
(setofall (listof ?y ?x) (holds ?r ?x ?y))))
;;; REDEFINED-IN-FRAME-ONTOLOGY!
(define-function COMPOSITION (?r1 ?r2) :-> ?relation
"The composition of a binary relation $r_1$ and a binary
relation $r_2$ is a binary relation in which an object $x$ is related to an
object $z$ if and only if there is an object $y$ such that $x$ is related to
$y$ by $r_1$ and $y$ is related to $z$ by $r_2$."
:lambda-body (if (and (binary-relation ?r1)
(binary-relation ?r2))
(setofall (listof ?x ?z)
(exists (?y)
(and (holds ?r1 ?x ?y)
(holds ?r2 ?y ?z))))))
(define-relation ONE-ONE (?r)
:iff-def (and (binary-relation ?r)
(function ?r)
(function (inverse ?r))))
(define-relation MANY-ONE (?r)
:iff-def (and (binary-relation ?r)
(function ?r)))
(define-relation ONE-MANY (?r)
:iff-def (and (binary-relation ?r)
(function (inverse ?r))))
(define-relation MANY-MANY (?r)
:iff-def (and (binary-relation ?r)
(not (function ?r))
(not (function (inverse ?r)))))
;;; REDEFINED-IN-FRAME-ONTOLOGY!
(define-relation UNARY-FUNCTION (?f)
"A unary function is a function with a single argument and a single
value. Hence, it is also a binary relation."
:iff-def (and (function ?f)
(binary-relation ?f)))
(define-relation BINARY-FUNCTION (?f)
"A binary function is a function with two arguments and one value. Hence, it
is a relation with three arguments."
:iff-def (and (function ?f)
(not (empty ?f))
(forall (?list) (=> (member ?list ?f) (triple ?list)))))
(in-theory 'kif-meta)
(define-class EXPRESSION (?expr)
"KIF expression is either a word or a list of expressions."
:iff-def (or (word ?expr)
(and (list ?expr)
(forall ?subexpr
(=> (item ?subexpr ?expr)
(expression ?subexpr))))))
(define-class WORD (?expr)
"An atom in a KIF expression."
:def (and (expression ?expr)
(not (list ?expr)))
:axiom-def (exhaustive-subclass-partition
WORD (setof variable operator constant)))
(define-class VARIABLE (?expr)
"KIF variable"
:def (word ?expr)
:axiom-def (exhaustive-subclass-partition
VARIABLE (setof indvar seqvar)))
(define-class OPERATOR (?expr)
"KIF operator"
:def (word ?expr)
:axiom-def (exhaustive-subclass-partition OPERATOR
(setof termop sentop ruleop defop)))
(define-class CONSTANT (?expr)
"A constant used in a KIF expression."
:def (word ?expr)
:axiom-def (exhaustive-subclass-partition CONSTANT
(setof funconst relconst objconst)))
(define-class FUNCONST (?symbol)
"A symbol that denotes a function. Used as the functor of a
term expression."
:def (constant ?symbol))
(define-class RELCONST (?symbol)
"A symbol that denotes a relation (may also be a function).
Cannot be used as a functor of a term expression, even if it denotes
a function."
:def (constant ?symbol))
(define-class OBJCONST (?symbol)
"A symbol that denotes a KIF object other than a relation."
:def (constant ?symbol))
(define-class INDVAR (?expression)
"An individual variable in a KIF expression.
For every individual variable $\nu$, there is an axiom asserting that it is
indeed an individual variable. Each such axiom is a defining axiom for the
{\tt indvar} relation."
:def (variable ?expression))
(define-class SEQVAR (?expression)
"A sequence variable in a KIF expression.
For every sequence variable $\omega$, there is an axiom asserting that it is a
sequence variable. Each such axiom is a defining axiom for the {\tt seqvar}
relation."
:def (variable ?expression))
(define-class TERMOP (?expr)
"KIF term operator"
:iff-def (and (operator ?expr)
(member ?expr
(setof 'quote 'listof 'cond 'the 'setof
'setofall 'kappa 'lambda))))
(define-class SENTOP (?expr)
"KIF sentence operator"
:iff-def (and (operator ?expr)
(member ?expr
(setof 'not 'and 'or
'=> '<= '<=>
'forall 'exists))))
(define-class RULEOP (?expr)
"KIF rule operator"
:iff-def (and (operator ?expr)
(member ?expr
(setof '=>> '<<=))))
(define-class DEFOP (?expr)
"KIF definitional operator"
:iff-def (and (operator ?expr)
(member ?expr
(setof 'defobject 'define-function 'defrelation
':= ':=> ':axiom
':conservative-axiom))))
(define-class TERM (?expr)
"KIF term expression"
:iff-def (expression ?expr)
:axiom-def (exhaustive-subclass-partition TERM
(setof variable constant listterm setterm
quoterm logterm quanterm)))
(define-class FUNTERM (?expr)
"KIF function term expression."
:iff-def (and (term ?expr)
(list ?expr)
(funconst (first ?expr))))
(define-class LISTTERM (?expr)
"KIF list term expression"
:iff-def (and (term ?expr)
(list ?expr)
(= (first ?expr) 'listof)))
(define-class SETTERM (?expr)
"KIF set term expression"
:iff-def (and (term ?expr)
(list ?expr)
(= (first ?expr) 'setof)))
(define-class QUOTERM (?expr)
"KIF quoted term expression."
:iff-def (and (term ?expr)
(list ?expr)
(= (first ?expr) 'quote)
(expression (first (first ?expr)))))
(define-class LOGTERM (?x)
:iff-def (or (exists (?p1 ?t1)
(and (sentence ?p1) (term ?t1)
(= ?x (listof 'if ?p1 ?t1))))
(exists (?p1 ?t1 ?t2)
(and (sentence ?p1)
(term ?t1)
(term ?t2)
(= ?x (listof 'if ?p1 ?t1 ?t2))))
(exists ?clist
(and (list ?clist)
(=> (item ?c ?clist)
(exists (?p ?t)
(and (sentence ?p) (term ?t)
(= ?c (listof ?p ?t)))))
(= ?x (cons 'cond ?clist)))))
:constraints (term ?x))
(define-class QUANTERM (?x)
:iff-def (or (exists (?t ?p)
(and (term ?t) (sentence ?p)
(= ?x (listof 'the ?t ?p))))
(exists (?t ?p)
(and (term ?t) (sentence ?p)
(= ?x (listof 'setof ?t ?p))))
(exists (?vlist ?p)
(and (list ?vlist) (sentence ?p)
(>= (length ?vlist) 1)
(=> (item ?v ?vlistp) (indvar ?v))
(= ?x (listof 'kappa ?vlistp ?p))))
(exists (?vlist ?sv ?p)
(and (list ?vlist) (seqvar ?sv) (sentence ?p)
(=> (item ?v ?vlist) (indvar ?v))
(= ?x (listof 'kappa (append ?vlist (listof ?sv)) ?p))))
(exists (?vlist ?t)
(and (list ?vlist) (term ?t)
(>= (length ?vlist) 1)
(=> (item ?v ?vlistp) (indvar ?v))
(= ?x (listof 'lambda ?vlistp ?t))))
(exists (?vlist ?sv ?t)
(and (list ?vlist) (seqvar ?sv) (sentence ?t)
(=> (item ?v ?vlist) (indvar ?v))
(= ?x (listof 'lambda
(append ?vlist (listof ?sv))
?t)))))
:constraints (term ?x))
(define-class SENTENCE (?expr)
"KIF sentence expression. Has a truth value."
:def (expression ?expr)
:axiom-def (exhaustive-subclass-partition SENTENCE
(setof logconst relsent equation inequality
logsent quantsent)))
(define-class LOGCONST (?x)
"A KIF logical constant."
:def (sentence ?x))
(define-class RELSENT (?x)
:iff-def (exists (?r ?tlist)
(and (or (relconst ?r) (funconst ?r)) (list ?tlist)
(>= (length ?tlist) 1)
(=> (item ?t ?tlist) (term ?t))
(= ?x (cons ?r ?tlist))))
:constraints (sentence ?x))
(define-class EQUATION (?x)
:iff-def (exists (?t1 ?t2)
(and (term ?t1) (term ?t2)
(= ?x (listof '= ?t1 ?t2))))
:constraints (sentence ?x))
(define-class INEQUALITY (?x)
:iff-def (exists (?t1 ?t2)
(and (term ?t1) (term ?t2)
(= ?x (listof '/= ?t1 ?t2))))
:constraints (sentence ?x))
(define-class LOGSENT (?expr)
"KIF logical sentence."
:def (sentence ?expr)
:axiom-def (exhaustive-subclass-partition LOGSENT
(setof negation conjunction disjunction
implication reverse-implication equivalence)))
(define-class NEGATION (?x)
:iff-def (exists (?p)
(and (sentence ?p)
(= ?x (listof 'not ?p))))
:constraints (logsent ?x))
(define-class CONJUNCTION (?x)
:iff-def (exists ?plist
(and (list ?plist)
(>= (length ?plist) 1)
(=> (item ?p ?plist) (sentence ?p))
(= ?x (cons 'and ?plist))))
:constraints (logsent ?x))
(define-class DISJUNCTION (?x)
:iff-def (exists ?plist
(and (list ?plist)
(>= (length ?plist) 1)
(=> (item ?p ?plist) (sentence ?p))
(= ?x (cons 'or ?plist))))
:constraints (logsent ?x))
(define-class IMPLICATION (?x)
:iff-def (exists (?plist)
(and (list ?plist)
(>= (length ?plist) 2)
(=> (item ?p ?plist) (sentence ?p))
(= ?x (cons '=> ?plist))))
:constraints (logsent ?x))
(define-class REVERSE-IMPLICATION (?x)
:iff-def (exists (?plist)
(and (list ?plist)
(>= (length ?plist) 2)
(=> (item ?p ?plist) (sentence ?p))
(= ?x (cons '<= ?plist))))
:constraints (logsent ?x))
(define-class EQUIVALENCE (?x)
:iff-def (exists (?p1 ?p2)
(and (sentence ?p1)
(sentence ?p2)
(= ?x (listof '<=> ?p1 ?p2))))
:constraints (logsent ?x))
(define-class QUANTSENT (?x)
:iff-def (or (exists (?v ?p)
(and (indvar ?v) (sentence ?p)
(or (= ?x (listof 'forall ?v ?p))
(= ?x (listof 'exists ?v ?p)))))
(exists (?vlist ?p)
(and (list ?vlist) (sentence ?p)
(>= (length ?vlist) 1)
(=> (item ?v ?vlist) (indvar ?v))
(or (= ?x (listof 'forall ?vlist ?p))
(= ?x (listof 'exists ?vlist ?p))))))
:constraints (sentence ?x))
(define-function DENOTATION (?x)
"The term {\tt (denotation $\tau$)} denotes the object denoted by the object
denoted by $\tau$. A quotation denotes the quoted expression; the denotation
of any other object is $\bot$."
)
(define-function NAME (?x)
"The term {\tt (name $\tau$)} denotes the standard name for the object denoted
by the term $\tau$. The standard name for an expression $\tau$ is
{\tt (quote $\tau$)}; the standard name for a non-expression is at the
discretion of the user. (Note that there are only a countable number of
terms in KIF, but there can be models with uncountable cardinality;
consequently, it is not always possible for every object in the universe of
discourse to have a unique name.)")
(define-relation TRUTH (?sentence)
"A level-crossing relation used to state that a sentence is true."
:def (sentence ?sentence)
:issues ((:example (truth '(=> (sentence ?p) (listof '=> ?p ?p))))))
(define-relation DEFINING-AXIOM (?constant ?sentence)
"a defining axiom for a constant is a sentence that
helps define the constant. See the KIF specification
for details."
:def (and (constant ?constant)
(sentence ?sentence)))
(define-relation ANALYTIC-TRUTH (?sentence)
"Given a knowledge base $\Delta$, the sentence {\tt (analytic-truth '$\phi$)}
means that the sentence $\phi$ is logically entailed by the defining axioms of
the definitions in knowledge base $\Delta$."
:def (sentence ?sentence))
This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber