Definitions


Introduction

KIF includes a sublanguage for declaring the category and defining axioms (e.g. ``Triangles are polygons with 3 sides.'') for constants. Defining axioms are true "by definition" in a way that distinguishes them from sentences that express contingent properties of the world. Definitions are declarations and have no truth values in the sense that sentences have. KIF definitions can be complete in that they specify an expression that is equivalent to a constant, or partial in that they specify a defining axiom that restricts the possible denotations of a constant.

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)

Unrestricted Definitions

Three basic forms are available for declaring the category and defining axioms for constants. These forms can be used to specify any sentence as a defining axiom. Definitions that use these forms are therefore referred to as unrestricted definitions. The following table shows the defining axiom specified by each form of unrestricted definition:

    (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.

Restricted Definitions

Representation formalisms typically impose restrictions on the sentences that can occur in definitions. For example, traditional predicate logics allow only complete definitions which provide an expression that is equivalent to the constant being defined. Given such a complete definition, the defined constant can be removed from a theory by replacing each occurrence of the constant by the equivalent defining expression.

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.

Complete Definitions

Complete definitions specify an equivalent term or sentence for the constant being defined as described below. The following table shows the defining axiom specified by each form of complete definition:

    (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))

Conservative Partial Definitions

This section describes syntactic forms for partial definitions that specify necessary conditions on the relation, function, or object being defined. Such definitions specify 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. The partial definitions for relations specify conditions that necessarily hold for tuples that satisfy the relation. The partial definitions for functions specify conditions that necessarily hold for the arguments and value of the function being defined when the function has a value for a given set of arguments. The partial definitions for objects specify conditions that necessarily hold if the object being defined exists.

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)))

Richard Fikes