A definition associates with the constant being defined a defining axiom. Intuitively, the meaning of a definition is that its defining axiom is true and that its defining axiom is an analytic truth. Analytic truths are considered to be those sentences that are logically entailed from defining axioms. For example, term subsumption in the KL-ONE family of representation languages is an analytic truth in that it is determined solely on the basis of term definitions. The semantics of defining axiom and analytic truth is formally defined as follows.
Given a knowledge base D, the definitions in D specify a set D' of constant-sentence pairs.
For any constant s and sentence p, if the pair s-p is a member of set D', then knowledge base D is said to indexically entail the sentence:
(defining-axiom 's 'p)
For any constant s and sentence p, if the pair
s-p is not a member of set D', then
knowledge base D is said to indexically entail the sentence:
(not (defining-axiom 's 'p))
If a sentence p is logically entailed by the defining axioms in the pairs
in set D', then knowledge base D is said to indexically entail
the sentence:
(analytic-truth 'p)
If a sentence p is not logically entailed by the defining
axioms in the pairs in set D', then knowledge base D is said
to indexically entail the sentence:
(not (analytic-truth 'p))
In addition, defining axioms are true. That is, for any constant
s and sentence p, the following axiom schema
holds:
(=> (defining-axiom 's 'p) p)
(defobject s p1 ... pn)
(and p1 ... pn)
(deffunction f p1 ... pn)
(and (function f) p1 ... pn)
(defrelation r p1 ... pn)
(and (relation r) p1 ... pn)
Relation constants are defined using the defrelation operator. In an
unrestricted partial definition of a relation constant, the first argument,
r, is the constant being defined and the remaining arguments,
p1 ... pn, are sentences. For example, the
following definition defines r to be a relation that holds for all
single arguments that are positive numbers.
(defrelation r (=> (> ?z 0) (r ?z)))
This definition is partial in that it restricts the possible denotations of the
constant r, but does not specify an expression that is equivalent to
r. The defining axiom specified by this definition is the conjunction
of (relation r) and the second argument in the definition. The defining
axiom is unrestricted in that it may contradict other definitions of
R.Function constants are defined using the deffunction operator. In an unrestricted definition of a function constant, the first argument, pi, is the constant being defined and the remaining arguments, p1 ... pn, are sentences. For example, the following definition defines f to be a function which has a value that is greater than 1 for all numbers.
(deffunction f (=> (number ?y) (> (f ?y) 1))))
As in the previous example, this definition of f is partial, and the
defining axiom is unrestricted.Object constants are defined using the defobject operator. In an unrestricted definition of an object constant, the first argument, s, is the constant being defined, and the remaining arguments, p1 ... pn, are sentences. For example, the following definition defines the constant id to be a left and right identity for the binary function f.
(defobject id (= (f ?x id) ?x) (= (f id ?x) ?x))
As in the previous examples, this definition of id is partial and
unrestricted. In particular, f may not have a left and right identiy so that
there is no object id satisfying this definition.
Enderton extends the traditional notion of complete definitions by allowing partial definitions. However, he restricts partial definitions to be conservative extensions to a logical theory in the sense that adding a constant and its defining axioms to a theory not containing that constant does not logically entail any additional theorems not containing that constant. Object-oriented representation formalisms typically allow a form of conservative definitions for relation constants that specifies necessary conditions on the tuples that satisfy the relation.
Because of their pervasiveness in representation formalisms, KIF provides syntactic forms for complete definitions and for conservative partial definitions that specify necessary conditions as described in the following sections.
(defrelation r (v1 ... vn [w]) := p)
(<=> (r v1 ... vn [w]) p)
(deffunction f (v1 ... vn [w]) := t)
(= (f v1 ... vn [w]) t)
(defobject s := t)
(= s t)
In the complete definition of a relation constant, the first argument,
r, is the constant being defined, the second argument is a list
of individual variables with an optional final sequence variable specifying the
arguments of the relation; and the argument, p, following the
:= keyword, is a sentence. For example, the following sentence
defines a bachelor to be an unmarried man.
(defrelation bachelor (?x) := (and (man ?x) (not (married ?x))))
The defining axiom specified by this definition of bachelor is:
(<=> (bachelor ?x) (and (man ?x) (not (married ?x))))
In the complete definition of a function constant, the first argument,
f, is
the constant being defined, the second argument is a list of individual
variables with an optional final sequence variable specifying the arguments of
the function, and the argument, t, following the := keyword is a
term. For example, the following definition defines the function
paternal-grandfather in terms of the father function.
(deffunction paternal-grandfather (?x) := (father (father ?x)))
The defining axiom specified by this definition of
paternal-grandfather is:
(= (paternal-grandfather ?x) (father (father ?x)))
In the complete definition of an object constant, the first argument, s,
is the constant being defined, and the argument, f, following the :=
keyword, is a term. For example, the following definition defines the constant
origin to be the list (0,0,0).
(defobject origin := (list 0 0 0))
The defining axiom specified by this definition of origin is:
(= origin (list 0 0 0))
The following table shows the defining axiom(s) specified by each form of conservative partial definitions:
(defrelation r (v1 ... vn [w]) :=> p)
(=> (r v1 ... vn [w]) p))
(deffunction f (v1 ... vn [w]]) :-> v :=> p)
(=> (= (f v1 ... vn [w]) v) p)
(defobject s :-> v :=> p)
(=> (= s v) p)
In the partial definition of a relation constant, the first argument, r, is
the constant being defined, the second argument is a list of individual
variables with an optional final sequence variable specifying the arguments of
the relation; and the argument, p, following the :=>
keyword, is a sentence. For example, the following definition of a
parent specifies that a parent necessarily has a child.
(defrelation parent (?x) :=> (exists ?y (child ?y ?x)))
The defining axiom produced by this definition of person is:
(=> (parent ?x) (exists ?y (child ?y ?x)))
In the partial definition of a function constant, the first argument, f, is
the constant being defined and the second argument is a list of individual
variables with an optional final sequence variable specifying the arguments of
the function. The list of variables is followed by :->, an individual
variable, the keyword :=>, and the argument, p, which
is a sentence in which the variables specifying the arguments and value of
f are free. For example, the following definition of the function
father specifies that a father is necesarily a male.
(deffunction father (?x) :-> ?y :=> (male ?y))
The defining axiom specified by this definition of father is:
(=> (= (father ?x) ?y) (male ?y))
In the partial definition of an object constant, the first argument, s,
is the constant being defined. The constant is followed by :->, an
individual variable, the keyword :=>, and the second argument,
p, which is a sentence in which the individual variable is
free. For example, the following definition of the constant
first.day.of.week specifies that first.day.of.week must be either
Sunday or Monday.
(defobject first.day.of.week
:-> ?x :=> (or (= ?x 'Sunday) (= ?x 'Monday)))
The defining axiom specified by this definition of first.day.of.week
is:
(=> (= ?x first.day.of.week) (or (= ?x 'Sunday) (= ?x 'Monday)))