Conservative Partial Definitions



next up previous
Next: References Up: Partial Definitions Previous: Unrestricted Partial Definitions

Conservative Partial Definitions

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


(defobject )&(objconst (quote ))&(defobject :conservative-axiom )&The conditional defining axiom for &(deffunction )&(funconst (quote ))&(deffunction :conservative-axiom )&The conditional defining axiom for &(defrelation )&(relconst (quote ))&(defrelation :conservative-axiom )&The conditional defining axiom for &(defrelation ( ... ) :=> )&(and (=> (member ?x )& (= (length ?x) n))& (=> ( ... ) ))&(defrelation ( ... ) :=> )&(and (=> (member ?x )& (>= (length ?x) n))& (=> ( ... ) ))&(defrelation ( ... )&(and (=> (member ?x ) :=> :conservative-axiom )& (= (length ?x) n))& (=> ( ... ) ))&The conditional defining axiom for &(defrelation ( ... )&(and (=> (member ?x ) :=> :conservative-axiom )& (>= (length ?x) n))& (=> ( ... ) ))&The conditional defining axiom for

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:

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


(defobject := )&(= )&(defobject ... )&(and ... )&(defobject )&(objconst (quote ))&(defobject :conservative-axiom )&The conditional defining axiom for &&(deffunction ( ... []) := )&(= (lambda ( ... []) ))&(deffunction ... )&(and ... )&(deffunction )&(funconst (quote ))&(deffunction :conservative-axiom )&The conditional defining axiom for &&(defrelation ( ... []) := )&(= (kappa ( ... []) ))&(defrelation ... )&(and ... )&(defrelation )&(relconst (quote ))&(defrelation :conservative-axiom )&The conditional defining axiom for &(defrelation ( ... )&(and (=> (member ?x ) (= (length ?x) n)) :=> [:axiom ])& (=> ( ... ) ))& [])&(defrelation ( ... )&(and (=> (member ?x ) (>= (length ?x) n)) :=> [:axiom ])& (=> ( ... ) ))& [])&(defrelation ( ... )&(and (=> (member ?x ) (= (length ?x) n)) :=> [:conservative-axiom ])& (=> ( ... ) ))&[The conditional defining axiom for ]&(defrelation ( ... )&(and (=> (member ?x ) (>= (length ?x) n)) :=> [:conservative-axiom ])& (=> ( ... ) ))&[The conditional defining axiom for ]



next up previous
Next: References Up: Partial Definitions Previous: Unrestricted Partial Definitions



Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994