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 .