Subsections

## Definite clauses of ()

I follow the construction defined by [32] to extend , giving (), by adding a set of relation symbols , conjunction, negation and existential quantification. The syntax I use for these will be clear from the definition of the interpretations of () (essentially Prolog syntax where appropriate).

The interpretation of () is defined in terms of the interpretation of . The expression [s X] defines the assignment which is exactly like , except possibly for the variable X which gets assigned the element s. An interpretation of () is obtained from ( is said to be based on ) by choosing for every relation symbol r a relation r on taking the right number of arguments. Furthermore, let

1.
= def;
2.
= def; for a constraint.
3.
r() = def{ ASS|() r};
4.
for the empty conjunction , = defASS;
5.
(F, G) = defF G;
6.
(F) = defASS - F;
7.
(X.F) = def{[s X]| F, s }

Implication, universal quantification and disjunction may be defined in terms of these connectives. The formalism consists of definite clauses of (). I write such a definite clause as:

where p,q1...qn are atoms and is a constraint. Atoms look as r(X1,...,Xn) where r R and X1...Xn V.

A partial order on the set of all () interpretations is defined as follows: iff for all r R,r r. The union of a set of () interpretations is obtained by joining the denotations of the relation symbols and is again an () interpretation. A model M of a set of definite clauses is defined as an () interpretation such that M satisfies , i.e., M = ASSM.

The use of definite clauses is motivated by the following theorem, proven in [32] for the general case.

#### Theorem

Let be a set of definite clauses in (), and a interpretation. Define for all r

This defines a chain 0 1 ... of () interpretations, based on . Moreover, the union

is the least model of extending .

This theorem says that if is a set of definite clauses, then uniquely defines the relations of ; i.e. defines unique minimal denotations for the relation symbols of .

Example 10   As an example, let C = {c}, L = {l}, V = {XX1...} and R = {p,q}. Furthermore, consider the following definite program:

Clearly, p0 and q0 are both the empty set. Because the assignments are based on we know the solutions of the constraints. Therefore, we obtain

 p1 = {(X)| (X c)0} = {(X)| (X c)} = {(X)|X = c} = {(c,)}

But the denotation of the relation q is still empty. In the next round, it is clear that p2 = p1. The denotation of the relation q becomes interesting now:
 q2 = {(X)| (p(Y),X Y)1} = {(X)| p(Y)1 (X Y)1} = {(X)|(Y) = (c,) (X) = (Y)} = {(c,)}

The process continues like that, and we obtain the following diagram. The feature graphs f1, f2, f3... are those given in figure 2.4.

The denotation of the relation symbols is given by the following figure, where I write c for the feature graph (c,). 2.2

 0 1 2 3 4 5 ... p { c} { c} { c} { c} { c} ... q { c} { c, f1} { c, f1, f2} { c, f1, f2, f3} ...

A goal or query is a possibly empty conjunction of ()-atoms and a -constraint, written as:

An answer to a goal is a satisfiable constraint , such that p1...pn, is valid (given a set of clauses ) in the minimal model of . For example, for the previous definite clause program a possible answer to the goal