Unrestricted partial definitions can specify any sentence as a defining axiom, as described below. The following table shows the defining axiom specified by each form of unrestricted partial definition:

#&#Definition&Defining Axiom

In an unrestricted partial definition of an object constant, the first
argument, , is the constant being defined, and the remaining
arguments, ... , 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))`

The defining axiom specified by this definition of `id` (which is just the

conjunction of the second and third arguments in the definition) is
unrestricted in that it may contradict other partial definitions of `id`
and `f` may not have a left and right identity.

In an unrestricted partial definition of a function constant, the first
argument, , is the constant being defined and the remaining arguments,
... , 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)))`

The defining axiom specified by this definition of `f` is just the
implication that is the second argument in the definition.

There are two basic forms of unrestricted partial definitions for relations. Both forms allow inclusion of an arbitrary sentence to be a defining axiom for the constant being defined. The second form additionally provides for the specification of necessary conditions for the relation to hold. The second form has two variants, depending on whether a sequence variable is included in the function's argument list.

In the first form of unrestricted partial definition of a relation constant,
the first argument, , is the constant being defined and the remaining
arguments, ... , 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)))`

The defining axiom specified by this definition of `R` is just the
implication that is the second argument in the definition.

In the second form of unrestricted partial definition of a relation constant,
the first argument, , is the constant being defined, the second argument
is a list of individual variables specifying the arguments of the relation,
and the arguments, and , following the `:=>` and `:axiom` keywords, are sentences. The form has two variants, depending on
whether the argument list includes a sequence variable. The following is an
example of this form of definition in which `above` is defined to be a
binary transitive relation that holds only for "located objects".

(defrelation above (?b1 ?b2) :=> (and (located-object ?b1) (located-object ?b2)) :axiom (transitive above))

The defining axiom specified by this definition of `above` is:

(and (=> (member ?x above) (= (length ?x) 2)) (=> (above ?b1 ?b2) (and (located-object ?b1) (located-object ?b2))) (transitive above))

Wed Dec 7 13:23:42 PST 1994