$E$, then $s=t$;

2.  if $(y,f,s)$ is in $E$, then there is a path from $x$ to $y$ in $E$.

An [*attribute-value language*]{} ${\cal A}(A,V,L)$ consists of sets of logical formulas that describe feature graphs, by expressing constraints on the type of paths that can exist within the graphs.

-   The terms of an attribute-value language ${\cal A}(A,V,L)$ are the constants and the variables $s,t\in A\cup V$.

-   The formulas of an attribute-value language ${\cal A}(A,V,L)$ are path equations and Boolean combinations of path equations. Thus all formulas are either $ps\doteq qt$, where $ps$ and $qt$ are paths, or $\phi \wedge \psi$, $\phi \vee \psi$, or $\neg \phi$, where $\phi$ and $\psi$ are formulas.

Assume a finite set ${\mathord{\rm Lex}}$ (of lexical forms) and a finite set ${\mathord{\rm Cat}}$ (of categories). ${\mathord{\rm Lex}}$ will play the role of the set of terminals and ${\mathord{\rm Cat}}$ will play the role of the set of nonterminals in the productions.

A [*constituent structure tree*]{} (CST) is a labeled tree in which the internal nodes are labeled with elements of Cat and the leaves are labeled with elements of Lex.

Let $T$ be a constituent structure tree and $F$ be a set of formulas 