An interpretation of consists of a domain DI
which is the set of all feature graphs, and an interpretation function
.I (see definition 1). Variables and constants will
denote feature graphs, relative to some assignment.
The denotation of a variable X with respect to an assignment
is simply
. The denotation of a constant C is the feature
graph (c,
) (for any assignment). The denotation of a
descriptor sp is the subgraph at path p of the graph denoted by s.
An interpretation satisfies an atomic constraint
relative to an assignment
, if the descriptors
are both defined and the same, i.e.,
iff
=
A constraint is called satisfiable if it has a solution, and two
constraints and
are called equivalent if they have the
same solutions, i.e., if
.
Clearly, not all constraints are satisfiable. For example, the constraint
is not satisfiable, since both denote different graphs for all
assignments.
The problem of whether a constraint is satisfiable is decidable. For example in [Smolka1992] an algorithm for a more powerful feature logic is presented. In [VanNoord1993] a decidable algorithm for the constraint language is presented, which we briefly summarize in the next paragraph.
Satisfiability of a constraint is shown by transforming
into a constraint of a specific form, called the normal form.
This transformation is performed in two steps. Firstly, all complex
paths (paths containing more than one label) are removed by
introduction of some new variables. The resulting constraint (also
called basic) is shown to be satisfiable iff the original
constraint was. The next step then rewrites constraints without complex
path expressions into normal form.
If the resulting normal constraint is clash free, i.e., if it does not contain any constraints of the following form:
then it is called a solved clause. A solved clause C
is of the form or
.