Conservative partial definitions specify defining axioms that are conservative
extensions of the language. A defining axiom is a conservative extension if
adding it to any given collection of sentences not containing the constant
being defined does not logically entail any additional sentences not
containing the constant being defined. The defining axioms specified by
complete definitions and the defining axioms produced directly from some forms of partial definitions are necessarily conservative extensions. However, the arbitrary sentences that can be included in partial definitions are not in
general conservative extensions of the language and therefore must be
transformed into a conditional form of defining axiom that is guaranteed to be
conservative. If a knowledge base contains conservative partial definitions
containing arbitrary sentences for a given constant, then those definitions
specify a single *conditional defining axiom* for that constant as
described below.

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

#&#Definition&Defining Axiom

There are two forms of conservative partial definitions for objects. In the
first form, the argument, , is the constant being defined, and the
definition simply declares that the constant denotes an object. In the second
form, the first argument, , is the constant being defined, and the
argument, , following the `:conservative-axiom` keyword is a
sentence. The second form of definition provides a sentence to be included in
the conditional defining axiom for , as described below.

There are two forms of conservative partial definitions for functions. In the
first form, the argument, , is the constant being defined, and the
definition simply declares that the constant denotes a function. In the
second form, the first argument, , is the constant being defined and the
argument, , following the `:conservative-axiom` keyword is a
sentence. The second form of definition provides a sentence to be included in
the conditional defining axiom for , as described below.

There are three basic forms of conservative partial definitions for relations.
In the first form, the argument, , is the constant being defined, and
the definition simply declares that the constant denotes a relation. In the
second form, the first argument, , is the constant being defined and the
argument, , following the `:conservative-axiom` keyword is a
sentence. The second form of definition provides a sentence to be included in
the conditional defining axiom for as described below.

The third form of conservative partial definition of a relation constant provides for the specification of necessary conditions for the relation to hold and optionally provides an arbitrary sentence to be included in the constant's conditional defining axiom. The third form has four variants, depending on whether the optional sentence is included and whether a sequence variable is included in the function's argument list.

In the third form of conservative partial definition of a relation constant,
the first argument, , 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; , in the
keyword-argument pair, `:=>` , is a sentence; and , in the
optional final keyword-argument pair, `:conservative-axiom` , is a
sentence. For example, the following definition defines a person to
necessarily be a mammal.

`(defrelation person (?x) :=> (mammal ?x))`

The defining axiom produced by this definition of `person` is:

(and (=> (member ?x person) (= (length ?x) 1)) (=> (person ?x) (mammal ?x)))

The sentences following the keyword `:conservative-axiom` in all of the
partial definitions for a given constant are used to form a single
conservative defining axiom for that constant. The defining axiom essentially states that if an entity exists in the domain of discourse having all the properties ascribed to the constant by its definitions, then the constant denotes such an entity and the sentences in the constant's definitions following the keyword `:conservative-axiom` are true. That defining axiom is formed as follows.

For a given knowledge base and a given constant , let
,..., be the sentences following the keyword
`:conservative-axiom` in partial definitions of in , and
,..., be the defining axioms otherwise specified in
partial definitions of in . The sentences
,..., specify the following conservative defining axiom:

`(=> (exists ?x ... )`` (and ... )),`

where ?x is an individual variable that does not occur in any , and
for each `j = 1,...,n`, is with the
following substitutions:

- Each occurrence of as a term is replaced by
`?x`. - Each occurrence of
`( <args>)`as a function term is replaced by`(value ?x <args>)`. - Each occurrence of
`( <args>)`as a relational sentence is replaced by`(holds ?x <args>)`.

This form of defining axiom cannot introduce an inconsistency into a knowledge base since any inconsistency will occur in the antecedent of the implication, thus making the antecedent false and blocking the entailment of the consequent. Also, this form of defining axiom cannot introduce a new domain fact about other constants (e.g., `(color Clyde grey)`), since such a domain fact will occur in the antecedent of the defining axiom and will therefore block the implication of the consequent if it is not already true.

Note that, in general, a constant can have infinitely many partial definitions
(meta-linguistically specified by a definition schema). However, if any of
the partial definitions of a constant contain a sentence following the keyword
`:conservative-axiom`, then the constant must have only a finite number of
definitions. Otherwise, the conditional defining axiom for that constant
would be an infinitely long sentence, which is not allowed in KIF.

As an example of conservative partial definitions containing arbitrary
sentences, consider the following conservative version of the definition given
above of `id`, a left and right identity for `f`.

`(defobject id :conservative-axiom (= (f ?x id) ?x))`

`(defobject id :conservative-axiom (= (f id ?x) ?x))`

Assuming there are no other definitions of `id` in the knowledge base,
these two partial definitions produce a single defining axiom for `id` as
follows:

(=> (exists ?y (and (= (f ?x ?y) ?x) (= (f ?y ?x) ?x))) (and (= (f ?x id) ?x) (= (f id ?x) ?x)))

This axiom states that if there exists a left and right identity for `f`,
then
`id` is that identity.

The following table summarizes all the forms of KIF definitions and the defining axioms specified by each.

#&#Definition&Defining Axiom

Wed Dec 7 13:23:42 PST 1994