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

For any constant ` s` and sentence

(defining-axiom 'For any constant's)p

(not (defining-axiom 'If a sentence's))p

(analytic-truth 'If a sentence)p

(not (analytic-truth 'In addition, defining axioms are true. That is, for any constant))p

(=> (defining-axiom ''s)p)p

(defobjectRelation constants are defined using thesp1...pn) (andp1...pn) (deffunctionfp1...pn) (and (functionf)p1...pn) (defrelationrp1...pn) (and (relationr)p1...pn)

(defrelation r (=> (> ?z 0) (r ?z)))This definition is partial in that it restricts the possible denotations of the constant

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,

(deffunction f (=> (number ?y) (> (f ?y) 1))))As in the previous example, this definition of

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,

(defobject id (= (f ?x id) ?x) (= (f id ?x) ?x))As in the previous examples, this definition of

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.

(defrelationIn the complete definition of a relation constant, the first argument,r(v1...vn[w]) :=) (<=> (prv1...vn[w])) (deffunctionpf(v1...vn[w]) :=t) (= (fv1...vn[w])t) (defobject:=st) (=st)

(defrelation bachelor (?x) := (and (man ?x) (not (married ?x))))The defining axiom specified by this definition of

(<=> (bachelor ?x) (and (man ?x) (not (married ?x))))In the complete definition of a function constant, the first argument,

(deffunction paternal-grandfather (?x) := (father (father ?x)))The defining axiom specified by this definition of

(= (paternal-grandfather ?x) (father (father ?x)))In the complete definition of an object constant, the first argument,

(defobject origin := (list 0 0 0))The defining axiom specified by this definition of

(= origin (list 0 0 0))

The following table shows the defining axiom(s) specified by each form of conservative partial definitions:

(defrelationIn the partial definition of a relation constant, the first argument,r(v1...vn[w]) :=>) (=> (prv1...vn[w]))) (deffunctionpf(v1...vn[w]]) :->v:=>p) (=> (= (fv1...vn[w])v)) (defobjectps:->v:=>) (=> (=psv))p

(defrelation parent (?x) :=> (exists ?y (child ?y ?x)))The defining axiom produced by this definition of

(=> (parent ?x) (exists ?y (child ?y ?x)))In the partial definition of a function constant, the first argument,

(deffunction father (?x) :-> ?y :=> (male ?y))The defining axiom specified by this definition of

(=> (= (father ?x) ?y) (male ?y))In the partial definition of an object constant, the first argument,

(defobject first.day.of.week :-> ?x :=> (or (= ?x 'Sunday) (= ?x 'Monday)))The defining axiom specified by this definition of

(=> (= ?x first.day.of.week) (or (= ?x 'Sunday) (= ?x 'Monday)))

Richard Fikes