
Feature Trees over Arbitrary Structures
Ralf Treinen?
Programming Systems Lab
German Research Center for Artificial Intelligence (DFKI)
Stuhlsatzenhausweg 3, D66123 Saarbrucken, Germany
treinen@dfki.unisb.de
Abstract
This paper presents a family of first order feature tree theories, indexed by the theory of the feature labels used to build the trees. A given feature label theory, which is required to carry an appropriate notion of sets, is conservatively extended to a theory of feature trees with the predicates x[t]y (feature t leads from the root of tree x to the tree y), where we have to require t to be a ground term, and xt# (feature t is defined at the root of tree x). In the latter case, t might be a variable. Together with the notion of sets provided by the feature label theory, this yields a firstclass status of arities.
We present a quantifier elimination procedure to reduce any sentence of the feature tree theory to an equivalent sentence of the feature label theory. Hence, if the feature label theory is decidable, the feature tree theory is too.
If the feature label theory is the theory of infinitely many constants and finite sets over infinitely many constants, we obtain an extension of the feature theory CFT, giving firstclass status to arities. As an another application, we obtain decidability of the theory of feature trees, where the feature labels are words, and where the language includes the successor function on words, lexical comparison of words and firstclass status of arities.
1 Introduction
Feature trees have been introduced as recordlike data structures in constraint (logic) programming [4], [28], and as models of feature descriptions in computational linguistics [7], [6]. The use of recordlike structures in logic programming languages, in the form of socalled terms [1], was pioneered by the languages LOGIN [2] and LIFE [3]. More recently, Oz [17, 26] uses a feature constraint system, the semantics of which is directly based on feature trees. In computational linguistics, feature structures have a long history in the field of unification grammars (as described in [25]).
?On leave to: L.R.I., B^at. 490, Universit?e Paris Sud, F91405 Orsay cedex, France, treinen@lri.fr
To appear in: Patrick Blackburn and Maarten de Rijke, eds., Logic, Structures and Syntax, Studies in Logic, Language and Information, 1995
In both areas, first order predicate logic has been recognized as a powerful description language for feature trees. For the first area, this is immediate by the role of constraints in constraint logic programming [19] and in concurrent constrainedbased languages [26], while in the second area different approaches have been proposed. [24, 27, 20, 25] have advocated the use of predicate logic as feature description languages. [6] argues that predicate logic is the right language to express phenomena in both fields, and that feature trees constitute the canonical semantical model.
Feature trees [4] are possibly infinite, finitely branching trees, where the edges carry labels
taken from some given set of feature symbols. Features are functional, i.e., all edges departing
from the same node have different labels. In contrast to the usual definition from
the literature, we will omit
of nodes by socalled sort
der languages have been
sic class of predicate symany
first order feature lanrelation
symbols x[f ]y for
the standard model of feaof
this predicate is y is
der edge f". The feature
???
@
@
@
???
@
@
@
???
???
@
@
@
???
@
@
@
a c d c d
d c a
a b
Figure 1: A Feature Tree
in this paper the labeling
symbols. Different first orstudied.
The most babols,
which is contained in
guage, consists of binary
every feature symbol f . In
ture trees, the denotation
the direct subtree of x untheory
FT [4] is an axiomatization
of feature trees based exactly on this language (besides equality and sort predicates).
The feature theory CFT [28] uses a much more expressive language which extends
FT by socalled arity constraints xff1; : : : ; fng. The denotation of such a constraint in
the standard model is x has exactly edges labeled by f1; : : : ; fn departing from its root".
Furthermore, regular path expressions (which contain an implicit existential quantification
over feature paths, [7]), and subsumption ordering constraints [15, 14] have been considered.
Finally, the language F [31] contains a ternary feature predicate x[y]z. Using quantification
over features, all other feature theories can be embedded in the theory F [31, 6].
With the establishment of first order logic as feature description language, concrete problems concerning logical theories of feature trees have been attacked. After fixing an appropriate predicate logic language, these problems can be phrased as decision problems of certain, syntactically characterized fragments of the theory of feature trees. Satisfiability of existentially quantified conjunctions of atomic constraints (socalled basic constraints) and entailment between basic constraints is efficiently decidable for the languages FT [4] and CFT [28], and satisfiability of regular path constraints [7] and weak subsumption constraints [14] is decidable, while it is undecidable for subsumption constraints [13]. These considerations lead to the more general question whether the full first order theories of these languages is decidable. An affirmative answer was given for the case of FT [9] and CFT [10, 8]. Not surprisingly, the full first order theory of feature trees over F is undecidable, although the existential fragment of the theory is NPcomplete even with arity constraints as additional primitive notions [31].
The reason for the undecidability of F is the fact that it allows one to quantify over the direct subtrees of a tree. Taking x OE y (x is a direct subtree of y") as abbreviation of
9f y[f ]x, we can define for trees x with only finitely many different subtrees (rational trees) the predicate x is a subtree of y" by
8z
?
y OE z ^ 8y1; y2 (y1 OE y2 OE z ! y1 OE z) ! x OE z
?
Here, the idea is to abuse" feature trees as sets, taking the direct subtrees of a tree as the elements of a set. Note that z fulfills the hypothesis in the above formula exactly if the set" z contains y and is transitive, and that hence the transitive closure of y is the smallest z which satisfies the hypothesis.
Thus, we can easily show (e.g., with the method of [30]) the undecidability of the theory of feature trees in the language of F. Consequently, in order to get a decidable subtheory of F, we have to restrict the use of quantification over features.
The first contribution of this paper is the formulation of a decidable theory of feature trees which lies between CFT and F. The idea is to allow quantification over features only in order to state which features are defined, but not to quantify over the direct subtrees of a tree. More precisely, we will define the restricted theory of feature trees as the set of formulae where t in x[t]y is always a ground term, but where still atomic constraints xf# (f is defined on x"), where f may be a variable, are allowed. This situation is similar to Process Logic, where unrestricted quantification over path and state variables lead immediately to an undecidable validity problem, while a syntactic restriction leads to decidable sublogic [22].
This restricted theory still is an essential extension of the theory of CFT. It extends CFT, since we can encode an arity constraint xff1; : : : ; fng as 8f (xf# $ Wni=1 f ?= fi). Beyond the expressivity of CFT, we can make statements about the arities of trees, for instance we can say that the arity of x is contained in the arity of y by
8f (xf# ! yf#)
As another example, the following formula expresses that x has exactly 3 features:
9f1; f2; f3
?
f1 ?6 = f2 ^ f2 ?6 = f3 ^ f1 ?6 = f3 ^ 8g (xg# $ [g ?= f1 _ g ?= f2 _ g ?= f3])
?
From these examples, one gets the idea that the theory of sets of feature symbols is hidden in our restricted theory of feature trees. This leads to the second contribution of our approach, which we now explain in three steps.
The first step is to realize that, in order to decide the validity of first order sentences over feature trees, we can save some work if we employ an existing decision algorithm for the theory of finite sets over infinitely many constants. Since this theory is easily encoded in the theory WS1S, the weak second order monadic theory of one successor function, the existence of such an algorithm follows immediately from Buchis result on the decidability of WS1S [11]1.
1The reader shouldn't be confused by the fact that we are apparently mixing first and second order structures. A second order structure can always be considered as a twosorted first order structure, with one sort for the elements, and another sort for the sets. Only in the context of classes of structures makes it really sense to distinguish first order from second order structures.
The following examples give an idea why logical statements involving feature trees can be
reduced to logical statements on sets of features. Let x; y; z denote variables ranging over
feature trees, f; g; h range over features and F; G; H range over sets of features. First, the
formula
9x; y
?
8f (xf# ! yf#) ^ :8g (yg# ! xg#)
?
does not involve any tree construction. This formula is just about the sets of features defined at the roots of x and y, and hence can be translated to:
9F; G
?
8f (f ?2 F ! f ?2 G) ^ :8g (g ?2 G ! g ?2 F )
?
Formulae like the above subformula (8f (xf# : : :), where the feature tree x is only used as a set of features, will be called primitive formulae.
The formula
9x (x[a]x ^ x[b]y ^ :xh#) (1)
where a and b are two different constants, is clearly satisfiable if we can find a set which contains a and b, but not h. Hence, (1) can be reduced to
9F (a ?2 F ^ b ?2 F ^ :h ?2 F ) (2)
In the setting we have defined so far, this is equivalent to a ?6 = h ^ b ?6 = h.
The next step is to generalize this idea to the situation where we have some structure of feature symbols and finite sets of feature symbols given, and to build the feature trees with the feature labels we find in the given feature label structure. Hence, we now obtain a family of feature tree structures, indexed by the feature label structures. This is a wellknown situation, for instance in constraint domains for programming languages [26], where feature constraints are not isolated but come in combination with other constraint domains like numbers and words.
Hence, our decision procedure now decides the validity of a sentence of the feature tree theory relative to the theory of the feature labels. As a consequence, our feature tree theory is decidable if the feature label theory is. There is only little to do in order to adopt the reduction procedure to this more general case. The only problem is now that two different ground terms, like the constants a and b in example (1) above, not necessarily denote semantically different elements. Hence we have to consider the two cases a ?= b and a ?6 = b. In the first case, a ?= b and the functionality of features yield x ?= y. Hence, we can eliminate x, and obtain for the first case
a ?= b ^ y[a]y ^ y[b]y ^ :yh#
In the second case, we get the same reduction as before:
a ?6 = b ^ 9F (a ?2 F ^ b ?2 F ^ :h ?2 F )
The feature label structure may be equipped with operations and predicate symbols of their own, which of course can be used in the feature tree structure as well. We could for instance
take as feature label structure WS2S, that is the structure of words over the alphabet fa; bg, finite sets of words, and successor functions for every symbol of the alphabet. Since the membership predicate in any regular language is definable in the theory of this structure, we can express in this feature tree theory for any regular language L that the arity of some x is contained in L.
So far, feature trees have been finitely branching trees, that is we took as possible arities all finite sets of features. The third step is to generalize this to an arbitrary notion of arities. That is, we assume that the feature label structure comes with a notion of sets, where we only require that there are at least two different sets. From this, we construct the feature trees such that the arities of the trees are always sets of the given feature label structure. For instance, we get as before the finitely branching feature trees if the feature label structure contains all the finite sets of feature trees. If we take as feature label structure natural numbers and all the initial segments of the natural numbers, that is sets of the form f1; : : : ; ng, we get a structure of feature trees where at every node the edges are consecutively numbered. In example (1) above, this has the consequence that we cannot reduce (2) to a ?6 = h ^ b ?6 = h. Instead, the satisfiability of (3) depends on the theory of the feature label structure.
As another example, consider
9x; y (x[f ]x ^ y[f ]y ^ x ?6 = y) (3)
Here, we will make a case distinction: Either both x and y have the arity ffg, that is f is the only feature defined, or at least one of them has a greater arity. In the first case both variables are called tight, in the second case a variable with arity greater than ffg is called sloppy. Intuitively, a sloppy variable has features for which there are no constraints. For the case that both variables are tight, the formula can not be satisfied. This is a consequence of the fact that the formula x[f ]x ^ arity(x; ffg), a socalled determinant [28], has a unique solution. In the other case, the formula is clearly satisfied, since we can use the unconstrained features of x, resp. y, to make both values different. Hence, we can translate (3) to the formula which states that this other case is indeed possible:
9F; g (f ?2 F ^ :g ?2 F ) (4)
Up to now, we have been talking about the feature tree structures defined upon some feature label structure. The quantifier elimination procedure we are going to present will be based on an axiomatization FX only, no other properties of the structures will be used for the justification of the procedure. The axiomatization is not subject to the syntactic restriction we imposed on the input formulae to the procedure, that is the axioms may contain subformulae x[t]y where t is nonground.
The quantifier elimination procedure proposed in this paper takes another road than the quantifier eliminations which have been given for the feature theories FT [9] and CFT [8]. We believe that, in the case of FT and CFT, our procedure is simpler than the existing ones for these theories. The difference lies in the way how the procedure deals with the fact
that these feature theories themselves do not have the property of quantifier elimination. A theory T is defined to have the property of quantifier elimination [18], if for every variable x and atomic formulae OE1; : : : ; OEn there is a quantifierfree formula such that T j= 9x (OE1 ^ : : : ^ OEn) $ . An effective procedure to compute this yields immediately a decision procedure for T , provided does not contain new free variables, and provided True and False are the only quantifierfree formulae. A simple counterexample, showing that for instance FT does not have the property of quantifier elimination, is
9x (y[l]x ^ xk#) (5)
We can not simply eliminate x, since we need it to express an important property of the free variable y, which we must not drop.
The classical way to solve this problem is to extend the language, such that nonreducible formulae like (5) become atomic formulae in the extended language. In our example, this means that we have to add socalled pathconstraints like y(lk)# to the language. This solution was chosen in [9] and [8].
We will use another idea: We exploit the functionality of features to trade in the above situation an existential quantifier for a universal quantifier, and transform (5) into:
yl# ^ 8x (y[l]x ! xk#)
We can benefit from this quantifierswitching if we consider the elimination of blocks of quantifiers of the same kind. This idea has already been used, for instance, in [21, 12]: We consider formulae in prenex normal form, for instance
9 ? ? ? 98 ? ? ? 89 ? ? ? 9OE
where OE is quantifierfree. If we can transform 9 ? ? ? 9OE into a formula of the form 8 ? ? ? 8 for some quantifierfree , then we have reduced the number of quantifier alternations from 2 to 1, although the total number of quantifiers might have increased.
The rest of the paper is organized as follows: Section 2 fixes the necessary notions from predicate logic. In Section 3, we define by an axiom the class of feature label structures, which will be called admissible parameter structures in the rest of the paper. In Section 4 we construct the standard model of feature trees over some arbitrary admissible parameter structure, present the axiomatization FX and show that the feature tree structure is a model of FX. Some basic properties of the axiomatization FX are stated in Section 5. The overall structure of the quantifier elimination procedure is presented in Section 6, the details are given in Section 7.
2 Preliminaries
We consider manysorted predicate logic with equality.
We use the standard shortcuts from predicate logic: ~8 OE is the universal closure of OE. We write 9?x OE, where ?x = (x1; : : : ; xn) is a list of variables, as abbreviation for 9x1 : : : 9xn OE (8?x OE is defined accordingly.) We also use sometimes the notation 9X OE, where X is a finite set of variables, for 9?x OE where ?x is some linear arrangement of X . Instead of writing the sort with every quantified variable, as in 8x 2 S : : :", we will introduce naming conventions which allow us to directly read off the sort of a variable. As usual, variables may be decorated with suband superscripts. Lists of variables will be denoted with an overstrike as in ?x.
The junctors ^; _ take precedence over (bind tighter than) $;!. Negation : and quantors bind tightest. It is understood that conjunction is commutative and associative. Consequently, we identify a conjunction of formulae with the multiset of its conjuncts. We use notions like 2 OE or ? OE, where OE is a conjunction, accordingly.
We write the negation of x ?= y as x ?6 = y. We consider equality as symmetrical, that is we identify x ?= y with y ?= x (and hence, x ?6 = y with y ?6 = x). The reader should be aware, that x ?= y and x ?6 = y are formulae of our object logic, while x = y, resp. x <> y, is a mathematical statement, expressing that the two variables x, y are syntactically identical, resp. distinct.
fr(OE) is the set of free variables of OE, OE[y=x] denotes the formula that is obtained from OE by replacing every occurrence of x by y, after possibly renaming bound variables to avoid capture.
An assignment is a Xupdate of an assignment , where X is a set of variables, if (x) =
(x) for all variables x 62 X . We write [x1 7! a1; : : : ; xn 7! an] for the fx1; : : : ; xngupdate
of which assigns ai to xi, respectively.
3 Admissible Parameter Structures
In this section, we specify the class of parameter structures which we want to allow as a basis for the construction of feature trees.
Definition 3.1 (Admissible parameter signature) The signature ? = hS?; F?; R?i is an admissible parameter signature, if S? contains at least the two sorts Feat and Set, and R? contains at least the relational symbol Feat ?2 Set, that is the binary infix relation symbol ?2 of profile Feat; Set.
The sort Feat is intended to denote the features, and the sort Set is intended to denote the sets of features. In this sense, ?2 can be thought of as the usual elementship relation.
Small letters from the middle of the alphabet f; g; h; : : : are variables of sort Feat, and capital letters from the middle of the alphabet F; G; H; : : : are variables of sort Set.
The only requirement on the class of admissible parameter structures is, that they contain at least two (observationally) different sets:
(S2) 9F; G; f (f ?2 F ^ :f ?2 G)
Definition 3.2 (Admissible Parameter Structure) Let ? be an admissible parameter signature. We call a ?structure B an admissible parameter structure, if B j= (S2).
This is in two respects weaker than what is usually stated by axioms systems of second order logic [5]. First, we don't require extensionality, that is two different sets may have the same elements. Second, axiom (S2) is much weaker than the usual comprehension axiom of second order logic which states that every formula denotes a set. Note that, as a consequence of (S2), every admissible parameter structure contains at least one element of sort Feat.
Examples of admissible parameter signatures and algebras are
1. The signature ?C consists of an infinite set C of Featconstants and the ?2 predicate symbol. The algebra BC assigns C to Feat, every constant of C to itself, the powerset over C to Set, and the elementship relation to ?2.
2. ?F and BF are defined as above with the only difference that Set is interpreted as the class of finite sets over C.
3. The signature ?N contains the constant of sort Feat, the unary function symbol succ
of profile Feat ! Feat, and ?2. The algebra BN assigns the set of natural numbers to
Feat, the number to the constant and the successor function to succ. Set denotes
the class of initial segments of natural numbers (that is, sets of the form f1; : : : ; ng),
and ?2 denotes elementship.
4. The signature ?S contains the constant ffl of sort Feat, finitely many function symbols succi, 1 <= i <= n, of profile Feat ! Feat, two predicate symbols <=pre and <=lex, and ?2. The algebra BS assigns the set f1; : : : ; ng? to Feat, the empty word to ffl, the function >=x:xn to succn, the prefix (resp. lexical) ordering to <=pre, resp. <=lex, the powerset of f1; : : : ; ng? to Set, and elementship to ?2.
4 Feature Tree Structures
In this section we give the definition of a standard model of features trees over some given admissible parameter structure. We also present a set of axioms for feature trees. We will prove, along the presentation of the axioms, that the standard model of feature trees is indeed a model of this axiomatization. No other properties of the feature tree model than the axiomatization will be used for the justification of the quantifier elimination procedure to be presented in the next sections.
Definition 4.1 (Tree signature) For a given admissible parameter signature ?, we define the tree signature ?y = hS?y ; F?y ; R?yi by
S?y = S? +[ fTreeg
F?y = F?
R?y = R? +[ fTree[Feat]Tree; Tree Feat#g
In the standard model to be defined below, the sort symbol Tree denotes a set of trees. Small letters at the end of the alphabet (x; y; z : : :) denote Treevariables. Note that the only Treeterms are the Treevariables, and that any ?yformula without Treevariables is in fact a ?formula. We write the negation of xt# as xt".
Definition 4.2 (Tree) For a set M , a set o ? M? of finite Mwords is called a tree over M if it is prefixclosed, that is if vw 2 o implies v 2 o for all v; w 2 M?. T (M) denotes the set of trees over M .
Note that every tree contains the empty word ffl and hence is nonempty, and that a tree may be infinite. This is of course the usual definition of treesthe tree in Figure 1, for instance, is fffl; a; b; ad; bc; ba; ada; adc; add; bac; badg.
Definition 4.3 (Admissible Tree) For an admissible parameter structure B, an admissible tree over FeatB is a tree o 2 T (FeatB), such that
for all v 2 o exists M 2 SetB with: ?2 BM , v 2 o
AT (FeatB) denotes the set of admissible trees over FeatB.
Intuitively, this means that the set of features defined at some node of an admissible tree must be licensed by the denotation of Set in the admissible parameter structure B. If we take, e.g., an admissible structure B where SetB is the class of finite subsets of FeatB, then AT (FeatB) contains exactly the finitely branching trees over FeatB.
Definition 4.4 (Feature tree structure) For any admissible ?structure B, we define the ?ystructure By by
1. By j? = B,
2. TreeBy = AT (FeatB),
3. o [ ]By oe iff oe = fv j v 2 og,
4. o #By iff 2 o .
Hence, By is a conservative extension of B.
The first axiom gives an explicit definition for the ? ? # predicate:
(#) 8x; f (xf# $ 9y x[f ]y)
The next axiom scheme expresses that every feature is functional:
(F) 8x; y; z (x[t]y ^ x[t]z ! y ?= z) where t is ground.
Syntactic Convention arity(x; F ) := 8f (xf# $ f ?2 F )
If ?x = (x1; : : : ; xn) and ?F = (F1; : : : ; Fn), we write arity(?x; ?F ) for Vni=1 arity(xi; Fi).
The next axiom states that every tree has an arity, and hence reflects the fact that we consider admissible trees only.
(A) 8x 9F arity(x; F )
By construction, we get immediately:
Proposition 4.5 For any admissible ?structure B, we have By j= (#); (F ); (A).
Next next axiom scheme expresses that certain formulae indeed have a solution in the domain of feature trees.
Definition 4.6 (Graph, Constrained variable) A conjunction of formulae of the form x[t]y is a called a graph. For a graph , let co( ) := fx j x[t]y 2 for some t and yg be the set of variables constrained by .
Syntactic Convention For a graph and variable x, we define
Fx := ft j x[t]y 2 for some variable yg
? := ft ?6 = s j t <> s and t; s 2 Fx for some xg
For instance,
:= x[a(f )]y ^ x[b(g; a(f ))]z ^ y[a(a(f ))]x ^ y[a(a(f ))]y
is a graph with co( ) = fx; yg, Fx = fa(f); b(g; a(f))g, F y = fa(a(f))g, F z = ;, and ? = a(f) ?6 = b(g; a(f )).
(E) ~8
2
64
B@? ^
n^
i=1
^
a2Fxi
a ?2 Fi
1
CA ! 9x1; : : : ; xn ^
n^
i=1
arity(xi; Fi)
!3
75
where is a graph with co( ) = fx1; : : : ; xng.
An example of axiom scheme (E) is
8z; f1; f2; g; F; G (f1 ?6 = f2 ^ f1 ?2 F ^ f2 ?2 F ^ g ?2 G
! 9x1; x2 (x1[f1]x2 ^ x1[f2]z ^ x2[g]x1^
arity(x1; F ) ^ arity(x2; G)))
(6)
Proposition 4.7 T (M) with the subset relation is a cpo.
(see, e.g., [16] for definition and basic properties of cpos). Note, that in general AT (M) does not constitute a subcpo of T (M ). Obviously, the set of compact elements of T (M) are exactly the finite sets in T (M ), and T (M) is an algebraic cpo.
Lemma 4.8 For any admissible ?structure B, we have By j= (E).
Proof: (Sketch) Let be a graph, co( ) = fx1; : : : ; xng, and By; j= ? ^Vni=1
V
a2Fxi a ?2
Fi. We construct o1; : : : ; on 2 AT (FeatB), such that
By; [x1 7! o1; : : : ; xn 7! on] j= ^
n^
i=1
^arity(xi; Fi) (7)
We define the operator ?: (T (FeatB))n ! (T (FeatB))n by its n components pri ffi ?. For given i, let fxi[t1]z1; : : : ; xi[tm]zmg be the set of atoms in which constrain xi.
pri ffi ?(?1; : : : ; ?n) = ffflg [ 1oe1 [ : : : [ moem [ f 2 FeatB j ?2 B (Fi)g
where j is the evaluation of tj in B; , and where we define oej := ?k if zj = xk for some 1 <= k <= n, and otherwise oej := (zj). As usual j oej is an abbreviation for f jv j v 2 oej g.
? is obviously continuous, hence we can define (o1; : : : ; on) as the least fixed point of ?. By construction, oi 2 AT (FeatB) for all i. Since By; j= ? , all j for given i are different. Hence, (7) holds. 2
As an example of this construction, consider the formula (6). Let (z) = fffl; e; eeg, (f1) = a, (f2) = b, (g) = c, (F ) = fa; bg and (G) = fc; dg. In this case, we define ? by
pr1 ffi ?(?1; ?2) = ffflg [ a?2 [ bfffl; e; eeg [ fa; bg
= fffl; b; be; beeg [ a?2
pr2 ffi ?(?1; ?2) = ffflg [ c?1 [ fc; dg
= fffl; dg [ c?1
The least fixed point of ? is (L1; L2), where L1 is the prefixclosure of (ac)?(bee [ ad), and L2 is the prefixclosure of (ca)?(d [ cbee).
Syntactic Convention Let M be a finite set of Featterms.
arity(x; M) := 8f (xf# $ _
a2M
f ?= a)
As above, this notion generalizes to arity(?x; ?M ).
Definition 4.9 A determinant ffi is a formula
^ ^
x2co( )
arity(x; Fx)
where is a graph and has only free variables of sort Tree.
In other words, for every constraint x[t]y in a determinant, the term t must be ground.
For instance, from the following three formulae
x[a(c)]y ^ x[b(d)]z ^ y[a(a(c))]x ^ arity(x; fa(c); b(d)g)^ arity(y; fa(a(c))g)
x[a(f )]y ^ arity(x; fa(f)g)
x[a(c)]y ^ x[b(d; a(c))]z ^ arity(x; fa(c)g)
only the first one is a determinant (since f denotes a variable).
The last axiom scheme expresses that determinants have at most one solution in the constrained variables.
Syntactic Convention 9<=1?x OE is an abbreviation for
8?x; ?y (OE(?x) ^ OE(?y) ! ?x ?= ?y)
where ?y is some list of distinct variables as long as ?x, and disjoint to fr(OE).
9<=1 ?x OE reads here is at most one tuple ?x, such that OE".
(U) ~8 (? ! 9<=1co(ffi) ffi ) where ffi is a determinant.
An example of (U) is
8z (a1 ?6 = a2 ! 9<=1x; y (x[a1]y ^ x[a2]z ^ y[b]x ^ arity(x; fa1; a2g) ^ arity(y; fbg)))
Note, that (U) does not state that a determinant always has a solution. In the above example, it might be the case that, e.g., the set" fbg does not exist, that is that 9F 8x(x ?2 F $ x ?= b) does not hold in the parameter structure. In this case, the determinant does not have a solution due to axiom (A).
Lemma 4.10 For any admissible ?structure B, we have By j= (U).
Proof: (Sketch) We split the determinant ffi into ^ ae, where is a graph and ae is a conjunction of arities. As in the proof of Lemma 4.8, let By; j= ?ffi, and let ? be the operator defined by . By the construction given in the proof of Lemma 4.8, By; [x1 7! o1; : : : ; xn 7! on] j= ffi iff (o1; : : : ; on) is a fixed point of ?.
We show, that ? has only one fixed point. Let (o1; : : : ; on); (oe1; : : : ; oen) be two fixed points of ?. Define o ji := fv 2 oi j length(v) = jg for any j >= 0, and analogously for oeji . One
shows easily by induction on j that o ji = oeji for all i; j. Taking the limits of the two chains, the claim follows immediately. 2
Definition 4.11 The axiom system FX consists of the axioms (S2), (#), (F), (A), (E) and (U)
Corollary 4.12 For every admissible parameter structure B, we have that By j= FX.
5 Some Properties of FX
5.1 Determinants
As an immediate consequence of (U) and the definition of 9<=1 , we get
Proposition 5.1 For every formula and determinant ffi , we have
FX j= ~8 (?ffi ^ 9co(ffi) (ffi ^ ) ! 8co(ffi) (ffi ! ))
This prominent role of determinants is the heart of the entailment check for the feature theory CFT [28].
5.2 Primitive Formulae
Definition 5.2 The set of primitive formulae is defined by the grammar
p ::= oe j xt# j p ^ p j p _ p j :p j 8O p j 9O p
where oe denotes an arbitrary ?formula, and where O denotes a variable not of sort Tree.
In other words, a primitive formula is a ?yformula that does not contain a Treequantifier, and does not contain an atom of the form x ?= y or x[t]y. A primitive formula without free Treevariables is in fact a ?formula. Intuitively, in a primitive formula, the sort Tree is only used to express statements that could be as well expressed using sets. The following definition makes this intuition formal:
Definition 5.3 We define inductively OE[F ==x], the replacement of a Treevariable x by a Setvariable F in a primitive formula OE.
xt#[F==x] = t ?2 F
a[F==x] = a if a is an atomic formula different from xt# for all t
(:OE)[F ==x] = :(OE[F ==x])
(OE1 ^ OE2)[F ==x] = OE1[F ==x] ^ OE2[F ==x]
(9O OE)[F ==x] = 9O (OE[F ==x]) if F <> O
(9F OE)[F ==x] = 9G ((OE[G=F ])[F ==x]) if G 62 fr(OE)
Intuitively, OE[F ==x] abstracts the feature tree x in OE to a set F . This operation is an
abstraction since it drops"all the subtrees of a feature tree and just keeps the information
about the features defined at the root. Again, this notation generalizes to simultaneous
replacement [ ?F ==?x]. For instance, OE := xa(f)# ^ 8g (xa(g)# ! xb(g)#) is a primitive
formula, and
OE[F ==x] = a(f) ?2 F ^ 8g(a(g) ?2 F ! b(g) ?2 F )
The following lemma expresses that the definition of OE[F ==x] meets the intuition of replacing a Treevariable x by a Setvariable F .
Proposition 5.4 Let OE be a primitive formula. Then j= ~8
?
arity(?x; ?F ) ! (OE $ OE[ ?F ==?x])
?
.
It would be possible to extend the definition of a primitive formula and of OE[F ==x] to allow also for Treequantifiers. The definition given here is sufficient for the quantifier elimination as described below.
6 The Main Theorem
We first define the class of restricted formulae, which is the class of input formulae for our quantifier elimination procedure.
Definition 6.1 (Restricted formula) A ?yformula is called a restricted formula, if in every subformula x[t]y the term t is ground.
In the following, we will also speak of restricted sentences, the restricted theory of a ?ystructure, and so on.
Theorem 6.2 (Main Theorem) There is an algorithm which computes for every restricted ?ysentence oe a ?sentence with FX j= oe $ .
Before we can discuss the toplevel structure of the proof, we need some additional concepts which describe the intermediate results we get during the quantifier elimination.
Definition 6.3 (Molecule) The set of molecules is defined by the following grammar:
m ::= x ?= y j x ?6 = y j x[t]y j :x[t]y j p
where p is a primitive formula, and where t is a ground term.
Hence, any molecule without free Treevariables is in fact a primitive formula without free Treevariables, and hence a ?formula.
Definition 6.4 (Basic Formula) A basic formula is a ?yformula of the form
9?x (m1 ^ : : : ^ mn)
where m1; : : : ; mn are molecules. A variable is local to a basic formula 9?x OE if it occurs in ?x, and global otherwise.
Let 9?x OE be a basic formula, and let be the greatest graph contained in OE, that is is the set of all molecules of the form x[t]y contained in OE. Then we define FxOE = Fx.
Theorem 6.2 follows from the following lemma:
Lemma 6.5 (Main Lemma) There is an algorithm which computes for every basic formula OE an universally quantified Boolean combination of molecules, such that
1. FX j= ~8 (OE $ )
2. fr( ) ? fr(OE)
3. if fr(OE) = ;, then is a boolean combination of molecules.
We borrow the technique of proving Theorem 6.2 from Lemma 6.5 from [21], [12].
Proof of Theorem 6.2: It is sufficient to consider only sentences oe in a weak prenex normal form, where the matrix is just required to be boolean combination of molecules (instead of a boolean combination of atoms). We proceed by induction on the number n of quantifier blocks in the quantifier prefix.
If n = 0, then since oe is a sentence, it does not contain any Treevariables and hence is a ?sentence.
Let n >= 1 and oe = Q9?x OE, where Q is a (possibly empty) string of quantifiers, not ending with 9, and OE is a Boolean combination of molecules. We transform OE into disjunctive normal form and obtain an equivalent formula
Q9?x (OE1 _ : : : _ OEn)
where every OE is a conjunction of molecules. This is equivalent to
Q(9?x OE1 _ : : : _ 9?x OEn)
where every 9?x OEi is a basic formula. Using (1) of Lemma 6.5, we can transform this
equivalently into
Q(8?y1 1 _ : : : _ 8?yn n)
where every i is a Boolean combination of molecules, and where all ?yi are empty if Q is the empty string (because of (3) in Lemma 6.5). After possibly renaming bound variables, this can be transformed into the sentence Q8?z , where is Boolean combination of molecules. By condition (2) of Lemma 6.5, Q8?z is again a sentence. Since the number of quantifier alternations in Q8?x is n ? 1, we can now apply the induction hypothesis.
If the innermost block of quantifiers consists of universal quantifiers, we consider the negation :oe of the sentence (which now has an existential innermost block of quantifiers) and transform it into a restricted sentence . Consequently, FX j= oe $ : . 2
Corollary 6.6 If B is an admissible ?structure, then the restricted theory of By is decidable relative to the theory of B.
Note that all four admissible parameter structures introduced at the end of Section 3 have a decidable firstorder theory.
1. We can interpret the theory of BC in S1S, the monadic second order theory of natural numbers with successor. The decidability of the theory of BC follows from Buchis result [11] on the decidability of S1S.
2. Analogously, the decidability of the theory of BF follows from the decidability of WS1S, the weak monadic second order theory of the natural numbers with successor. The decidability of WS1S is an easy corollary of [11], since the finite sets are definable in S1S.
3. Decidability of the theory of BN follows again from [11], since the initial fragments of natural numbers are definable in S1S.
4. Definability of the theory of BS follows from Rabins celebrated result [23] on the decidability of S2S, the monadic second order theory of two successor functions. Note that the prefix relation and the lexical ordering can be defined in S2S [29].
Corollary 6.7 The restricted theory of By, where B is one of BC, BF , BN , BS, is decidable.
7 The Reduction
We now prove Lemma 6.5. Our goal is to eliminate, by equivalence transformations w.r.t. FX , all the quantifiers of sort Tree, taking care of the fact that we don't introduce new variables. This will be achieved by transformation rules which transform basic formulae into combinations of basic formulae. To make this formal, we introduce the class of complex formulae (see Figure 7 for an overview of the different syntactic classes of formulae):
?f. 
^; _; :
8; 9; xt#
x ?= y, x ?6 = y,
x[t]y, :x[t]y XXXXXXXz
primitive ????
molecule 
9; ^ basic 
8; ^; _ complex
Figure 2: Classes of formulae
Definition 7.1 (Complex formula) The set of complex formulae is defined by the following grammar:
F ::= 8x F j F ^ F j F _ F j hbasic formulai
Note that this fragment, by closure of the set of molecules under negation, also contains constructions like
molecule1 ^ : : : ^ moleculen ! basic formula
The transformation rules always have a basic formula in the hypothesis. Such a rule can be applied to any maximal basic formula occurring in a complex formula. The maximality condition means here, that we have to use the complete existential quantifier prefix. If a complex formula does not contain any basic formula, it can be easily transformed into a universal quantified boolean combination of molecules by moving universal quantifiers outside.
Definition 7.2 (Quasisolved from) A basic formula 9?x is a quasisolved form, if
1. does not contain a molecule x ?= y or :x[t]y,
2. if x ?6 = y 2 , then x <> y, and x 2 ?x or y 2 ?x.
3. if x[t]y 2 , then x 2 ?x,
4. if x[t]y ^ x[t]z ? , then y = z.
5. if the ground Featterms t, s occur in and t <> s, then t ?6 = s 2 .
6. if x 2 ?x, then arity(x; FxOE ) 2 or :arity(x; FxOE ) 2 .
7.1 Transformation into Quasisolved Form
The goal of the rules in Figure 3 is to have only basic formulae which are quasisolved forms.
Proposition 7.3 The rules described by (SC), (E1), (E2), (IE1), (FI) are equivalence transformations in every structure.
(Sc) 9?x (m ^ OE)
m ^ 9?x OE fr(m) ?x = ;; m is not a primitive formula
(E1) 9?x; x (x ?= y ^ OE)
9?x OE[y=x] y <> x
(E2) 9?x (x ?= x ^ OE)
9?x OE
(IE1) 9?x (x ?6 = x ^ OE)
?
(UD) 9?x (:x[t]y ^ OE)
9?x (xt" ^ OE)
_ 9?x; z (x[t]z ^ z ?6 = y ^ OE)
z new
(FD) 9?x (x[t]y ^ x[t]z ^ OE)
9?x (x[t]y ^ y ?= z ^ OE)
(FI) 9?x OE
s ?= t ^ 9?x OE[t=s]
_ 9?x (s ?6 = t ^ OE)
the ground terms s, t occur in OE, s <> t
(FQ) 9?x; x (y[t]x ^ OE)
yt# ^ 8z (y[t]z ! 9?x OE[z=x]) y 62 ?x; z new
Figure 3: The rule set (QSF) for quasisolved forms.
Lemma 7.4 (UD) describes an equivalence transformation in every model of the axioms schemes ("), (F).
Proof: Axiom scheme (F) is equivalent to
8x; y (x[t]y $ 9z x[t]z ^ 8z (x[t]z ! z ?= y))
which can be transformed equivalently, using axiom (#), into
8x; y (:x[t]y $ xt" _ 9z (x[t]z ^ z ?6 = y))
As a consequence, we have for every formula OE with z 62 fr(OE):
("); (F ) j= ~8 (:x[t]y ^ OE $ (xt" ^ OE) _ 9z (x[t]z ^ z ?6 = y ^ OE))
and hence
("); (F ) j= ~8 (9?x (:x[t]y ^ OE) $ 9?x (xt" ^ OE) _ 9?x; z (x[t]z ^ z ?6 = y ^ OE)) 2
Lemma 7.5 (FD) describes an equivalence transformation in every model of the axiom scheme (F).
Lemma 7.6 (FQ) describes an equivalence transformation in every model of the axiom scheme (F).
Proof: We have for any formula with z 62 fr( )
(F ) j= ~8
?
9x (y[t]x ^ ) $ yt# ^ 8z (y[t]z ! [z=x])
?
Now we choose to be the formula 9?xOE. Since y 62 ?x the antecedent of the rule is equivalent to 9x (y[t]x ^ 9?x OE), and the claim follows immediately. 2
For this rule it is essential that t is ground.
Lemma 7.7 The rule system (QSF) is terminating.
Proof: We define a measure on basic formulae and show, that for every rule application the measure of every single basic formula generated is smaller than the measure of the basic formula being replaced. Termination then follows by a standard multiset argument. We assign a basic formula the tuple ( 1; 2; 3; 4), where
1. 1 is the number of :x[t]y molecules in ,
2. 2 is the number of x[t]y molecules in ,
3. 3 is the number of pairs (t; s) of Featground terms, where both t and s occur in , but t ?6 = s does not occur in ,
4. 4 is the total length of .
It is now easily checked that the lexicographic ordering on these measures is strictly decreased by every application of a rule. The side condition of rule (Sc) guarantees that no formula of the form t ?6 = s, arity(x; FxOE ) or :arity(x; FxOE ) is moved out of a basic formula. 2
Corollary 7.8 There is an algorithm, which transforms any basic formula into an FX equivalent complex formula, in which all basic formulae are quasisolved forms.
Proof: We compute a normalfrom wrt. the ruleset (QSF), and from this compute a normal form wrt. the following rule:
(ST) 9?x; x OE
9?x; x (OE ^ arity(x; FxOE ))
_ 9?x; x (OE ^ :arity(x; FxOE ))
arity(x; FxOE ); :arity(x; FxOE ) 62 OE
2
7.2 Eliminating quasisolved forms with sloppy inequations
In this section, we show how to eliminate quasisolved forms with only benign inequations, in a sense to be explained soon. In the next subsection, we will explain how to get rid of nasty inequations.
Definition 7.9 (Sloppy and Tight variables) Let 9?x be a basic formula. We call a local variable x 2 ?x tight (in 9?x ) if arity(x; Fx) 2 , and otherwise sloppy.
By the definition of a quasisolved form, :arity(x; FxOE ) 2 for every sloppy variable x.
Definition 7.10 (Closure) For a graph , we define for every feature path ss of Featterms the relation ;ss as the smallest relation on fr( ) with
x ;ffl x if x 2 fr( )
if x ;ss y and y[t]z 2 ; then x ;sst z
We write x ; y if x ;ss y for some ss.
For a graph and variables x; y, we define the closure of (x; y)
hx; yi := f(u; v) 2 fr( )2 j x ;ss u and y ;ss v for some ssg
In [8], the variable y with x ;ss y has been called the value j xss j of the rooted path xss in . Obviously, hx; yi can be computed in finitely many steps.
Proposition 7.11 For every graph ,variables x; y and (u; v) 2 hx; yi we have
(F ) j= ( ^ u ?6 = v ! x ?6 = y)
Definition 7.12 (Sloppy and Tight inequations) Let 9?x be a basic formula. We call an inequation x ?6 = y sloppy (in 9?x ), if there is a (u; v) 2 hx; yi with x <> y, where at least one of u and v is sloppy. Otherwise, the inequation is called tight.
The benign inequations handled in this section are the sloppy ones. The idea is that for sloppy variables, we have enough freedom to make them all different.
In the following, we assume a partition of a quasisolved form as 9?x ( ^ ? ^ ae), where denotes a graph, ? denotes a conjunction of inequations between Treevariables, and ae denotes a primitive formula. Note that in this case, by the definition of quasisolved forms, co( ) ? ?x, ? ? ae, and ? contains only nontrivial inequations which use at least one local variable. For a graph , we denote by ~ the formula obtained by replacing every atom x[t]y by xt#.
Lemma 7.13 Let 9?x ( ^ ae) be a quasi solved form without inequations. Then
FX j= ~8
?
9?x ( ^ ae) ! 9 ?F ((~ ^ ae)[ ?F ==?x])
?
where ?F is disjoint with fr(ae).
Proof: Let A j= FX and be a valuation with A; j= 9?x ( ^ ae). Since j= ! ~, we get A; j= 9?x (~ ^ ae). Together with axiom (A), this means since ?F is disjoint with fr(ae), that A; j= 9?x; ?F (arity(?x; ?F ) ^ ~ ^ ae). With Proposition 5.4, we get
A; j= 9 ?F ((~ ^ ae)[ ?F ==?x])
since ?x is disjoint with fr((~ ^ ae)[ ?F ==?x]). 2
Lemma 7.14 Let 9?x ( ^ ? ^ ae) be a quasi solved form, where ?F is disjoint with fr(ae) and ? consists of sloppy inequations only. Then
FX j= ~8
?
9 ?F ((~ ^ ae)[ ?F ==?x]) ! 9?x ( ^ ? ^ ae)
?
Proof: Let A j= FX and be a valuation with A; j= 9 ?F (~ ^ ae)[ ?F ==?x]. Let be an ?F  update of , such that A; j= (~ ^ ae)[ ?F ==?x]. Let Sl be the set of sloppy variables of ^ ae. Let f; F be new variables, and for every x 2 Sl, let nx >= 0, and fx; x0; : : : ; xnx be variables
not occurring in ^ ae. Let Slf = ffx j x 2 Slg, and Slx = fxi j x 2 Sl; <= i <= nxg. We
define an extension ? of by
? := ^ ^
x2Sl
(x[fx]x0 ^ x0[f ]x1 ^ : : : xnx?1[f ]xnx ^ arity(xnx ; F ))
Hence, j= ? ! . By axiom (S2), there are a 2 FeatA and A; B 2 SetA with a ?2A A and a 6 ?2A B. We denote by ??x the extension of ?x by Slx, and by ??F an according extension of ?F . Hence, by definition of sloppyness, there is a Slf [ Slx [ ff; Fgupdate of such that
A; j= ?? ^ (~? ^ ae)[ ??F ==??x]
Especially, (f) = a, (F i) = A if F corresponds to some xi with i <= nx, and (F i) = B
if F corresponds to some xnx . Note, that ?? extends ? ? ae just by stating that fx
is assigned a value different from all (ground) terms in Fx. By construction, A; j=
Vni=1
V
a2Fxi? a 2 Fi. Hence, by axiom (E), there is an ??xupdate 00 of , such that
A; 00 j= ? ^ arity(??x; ??F )
Let (x) = 00(x) if x 2 ?x, and (x) = (x) otherwise. Hence, A; j= . By Proposition
5.4 and since ?F is disjoint with fr(ae), A; j= ae.
Since there are infinitely many choices of nx for every x 2 Sl, we can easily find values nx such that 00(x) <> 00(y) for every variable y 2 fr( ^ ? ^ ae) with y <> x. Hence, by Proposition 7.11, A; j= ?. 2
We are now ready to give the elimination rule for quasisolved forms with benign inequations:
(IE2) 9?x ( ^ ? ^ ae)
9 ?F ((~ ^ ae)[ ?F ==?x]) if ? contains only sloppy inequations, ?F fr(ae) = ;
As an example of rule (IE2), consider
9x; y; u (x[s]y ^ u[s]v ^ y[t]y ^ x ?6 = u ^ arity(x; fsg) ^ arity(u; fsg) ^ :arity(y; ftg))
9F; G; H ( s ?2 F ^ s ?2 G ^ t ?2 H^
8? (? ?2 F $ ? ?= s) ^ 8? (? ?2 G $ ? ?= s) ^ :8? (? ?2 F $ ? ?= s))
Here, x ?6 = u is a sloppy inequation since y is a sloppy variable.
From Lemma 7.14 and Lemma 7.13, we get immediately
Lemma 7.15 (IE2) describes an equivalence transformation in every model of FX.
Corollary 7.16 There is an algorithm, which transforms any complex formula, in which all basic formulae are quasisolved forms containing only sloppy inequations, into an FX equivalent universally quantified boolean combination of molecules.
7.3 Eliminating tight inequations
In the closure of tight inequations, there are only inequations of type tight <> tight or tight <> global. We first show how to transform the quasisolved form such that the only tight inequations are of type tight <> global. Then, we show how to get rid of the tight <> global inequations.
(IE3) 9?x ( ^ ? ^ x ?6 = y ^ ae)
9?x ( ^ ? ^ ae)
there are tight variables u; v with (u; v) 2 hx; yi
and Fu <> F v
From Proposition 7.11, we get
Proposition 7.17 (IE3) describes an equivalence transformation on quasisolved forms in every model of FX.
Proof: This is a consequence of condition (5) in the definition of a quasisolved form. 2
We say that the set ? of equations is closed under a graph , if whenever x ?= y 2 and (u; v) 2 hx; yi , then u ?= v 2 .
Proposition 7.18 Let ffi be a determinant and ? a set of equations which is closed under ffi . If fr(?) ? co(ffi) and Fxffi = F yffi for every equation x ?= y 2 ?, then
FX j= ~8 (?ffi ! (ffi ! ?))
Proof: Let A; j= ?ffi. By Proposition 5.1, we have to show that
A; j= 9co(ffi)(ffi ^ ?)) (8)
Let ? be an idempotent substitution equivalent to ?. Then
(8) , A; j= 9co(ffi)(ffi ^ ?)
, A; j= 9co(ffi)(?ffi ^ ?)
, A; j= 9co(ffi)(?ffi) since fr(?) ? co(ffi) (9)
By construction, ?ffi is again a determinant, with co(?) ? co(ffi), and ??ffi = ?ffi. Hence, (9) follows from axiom (E). 2
A similar lemma, in the context of CFT, was presented in [28].
Proposition 7.19 Let ffi be a determinant and ?; ?0 be sets of equations such that ? ^ ?0 is closed under ffi . If fr(?) ? co(ffi) and Fxffi = F yffi for every equation x ?= y 2 ?, then
FX j= ?ffi ! ~8 (ffi ! (?0 $ ? ^ ?0))
Proof: We have to show that
FX j= ~8 (?ffi ^ ffi ^ ?0 ! ?) (10)
Let ?0 be an idempotent substitution equivalent to ?0. Then (10) is equivalent to
FX j= ~8 (?ffi ^ ?0 ffi ! ?0?) (11)
since ?0?ffi = ?ffi. Observe, that ?ffi = ??0 ffi , fr(?0?) ? co(?0 ffi ), ?0? is closed under ?0 ffi , and that Fx?0 ffi = F y?0 ffi for every equation x ?= y 2 . Hence, (11) follows from Proposition 7.18. 2
We can now give the rule which reduces the tight <> tight inequations to tight <> global inequations:
(IE4) 9?x ( ^ ? ^ x ?6 = y ^ ae)
_
(u;v)2I
9?x ( ^ ? ^ u ?6 = v ^ ae)
x ?6 = y tight, rule (IE3) does not apply,
I = f(u; v) 2 hx; yi j fu; vg 6? ?xg
As an example of rule (IE4), consider
9x; y; v ( x[s]v ^ x[t]v0 ^ y[s]w ^ y[t]w0 ^ s ?6 = t^
arity(x; fs; tg) ^ arity(y; fs; tg) ^ arity(v; fg) ^ x ?6 = y)
9x; y; v ( x[s]v ^ x[t]v0 ^ y[s]w ^ y[t]w0 ^ s ?6 = t^
arity(x; fs; tg) ^ arity(y; fs; tg) ^ arity(v; fg) ^ v ?6 = w)
_ 9x; y; v ( x[s]v ^ x[t]v0 ^ y[s]w ^ y[t]w0 ^ s ?6 = t^
arity(x; fs; tg) ^ arity(y; fs; tg) ^ arity(v; fg) ^ v0 ?6 = w0)
Lemma 7.20 (IE4) describes an equivalence transformation in every model of FX.
Proof: This follows immediately from Proposition 7.19. 2
Finally, we give the rule to eliminate tight <> global inequations.
Definition 7.21 (Generated subformula) For a conjunction OE of molecules and variable x, the subformula OEx of OE generated by x is defined as
OEx := fu[t]v; arity(u; M) 2 OE j x ;OE ug
Note that, if x ?6 = y is tight in the quasisolved form 9?x OE, then OEx is a determinant.
(IE5) 9?x; x (OE ^ x ?6 = y)
9?x; x OE ^ 8co(OEx) (OEx ! x ?6 = y) y 62 ?x; y ?6 = x; x tight
As an example of rule (IE5), consider
9x; x0 (x[s]x ^ x[t]y ^ x0[t]x0 ^ s ?6 = t ^ arity(x; ffg) ^ x ?6 = y)
9x; x0 (x[s]x ^ x[t]y ^ x0[t]x0 ^ s ?6 = t ^ arity(x; ffg))^
8x (x[s]x ^ x[t]y ^ arity(x; ffg) ! x ?6 = y)
Lemma 7.22 (IE5) describes an equivalence transformation in every model of FX.
Proof: First note that co(OEx) ? ?x [ fxg. Since j= OE ! OEx, the conclusion implies the hypothesis.
The hypothesis obviously implies the first part of the conclusion. By Proposition 5.1, it also implies the second part (note that ?OEx ? OE, since OE is a quasisolved form). 2
Corollary 7.23 There is an algorithm, which transform any complex formula in which all basic formulae are quasisolved forms, into an FXequivalent complex formula, in which all basic formulae are quasisolved forms containing only sloppy inequations.
Hence, we obtain the proof of Lemma 6.5 by composing the Corollaries 7.8, 7.16 and 7.23.
Acknowledgments. David Israel pointed out the analogy to the situation in process logic. Rolf Backofen, Andreas Podelski and Gert Smolka provided helpful criticism and remarks.
This work has been supported by the Bundesminister fur Bildung, Wissenschaft, Forschung und Technologie (Hydra, ITW 9105), the Esprit Basic Research Project ACCLAIM (EP 7195) and the Esprit Working Group CCL (EP 6028).
References
[1] Hassan A?tKaci. An algebraic semantics approach to the effective resolution of type equations. Theoretical Computer Science, 45:293{351, 1986.
[2] Hassan A?tKaci and Roger Nasr. LOGIN: A logic programming language with builtin inheritance. Journal of Logic Programming, 3:185{215, 1986.
[3] Hassan A?tKaci and Andreas Podelski. Towards a meaning of LIFE. In Jan Maluszy?nski and Martin Wirsing, editors, 3rd International Symposium on Programming Language Implementation and Logic Programming, Lecture Notes in Computer Science, vol. 528, pages 255{274. SpringerVerlag, August 1991.
[4] Hassan A?tKaci, Andreas Podelski, and Gert Smolka. A featurebased constraint system for logic programming with entailment. Theoretical Computer Science, 122(1{2):263{283, January 1994.
[5] Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Computer Science and Applied Mathematics. Academic Press, 1986.
[6] Rolf Backofen. Expressivity and Decidability of FirstOrder Theories over Feature Trees. PhD thesis, Technische Fakultat der Universitat des Saarlandes, Saarbrucken, Germany, 1994.
[7] Rolf Backofen. Regular path expressions in feature logic. Journal of Symbolic Computation, 17:421{455, 1994.
[8] Rolf Backofen. A complete axiomatization of a theory with feature and arity constraints. Journal of Logic Programming, 1995. To appear.
[9] Rolf Backofen and Gert Smolka. A complete and recursive feature theory. Theoretical Computer Science. To appear.
[10] Rolf Backofen and Ralf Treinen. How to win a game with features. In JeanPierre Jouannaud, editor, 1st International Conference on Constraints in Computational Logics, Lecture Notes in Computer Science, vol. 845, Munchen, Germany, September 1994. SpringerVerlag.
[11] J. R. Buchi. On a decision method in restricted second order arithmetic. In E. Nagel et. al., editor, International Congr. on Logic, Methodology and Philosophy of Science, pages 1{11. Stanford University Press, 1960.
[12] Hubert Comon and Pierre Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7(3,4):371{425, 1989.
[13] Jochen Dorre. FeatureLogik und Semiunfikation. PhD thesis, Philosophische Fakultat der Universitat Stuttgart, July 1993. In German.
[14] Jochen Dorre. Featurelogic with weak subsumption constraints. In M. A. Rosner C. J. Rupp and R. L. Johnson, editors, Constraints, Language and Computation, chapter 7, pages 187{203. Academic Press, 1994.
[15] Jochen Dorre and WilliamC. Rounds. On subsumption and semiunification in feature algebras. Journal of Symbolic Computation, 13(4):441{461, April 1992.
[16] C. A. Gunter and D. S. Scott. Semantic domains. In van Leeuwen [32], chapter 12, pages 633{674.
[17] Martin Henz, Gert Smolka, and Jorg Wurtz. Objectoriented concurrent constraint programming in Oz. In V. Saraswat and P. Van Hentenryck, editors, Principles and Practice of Constraint Programming, chapter 2, pages 27{48. MIT Press, Cambridge, MA, 1995. To appear.
[18] Wilfrid Hodges. Model Theory. Encyclopedia of Mathematics and its Applications 42. Cambridge University Press, 1993.
[19] Joxan Jaffar and JeanLouis Lassez. Constraint logic programming. In Proceedings of the 14th ACM Conference on Principles of Programming Languages, pages 111{119, Munich, Germany, January 1987. ACM.
[20] Mark Johnson. AttributeValue Logic and the Theory of Grammar. CSLI Lecture Notes 16. Center for the Study of Language and Information, Stanford University, CA, 1988.
[21] Anatoli?? Ivanovi<=c Malc'ev. Axiomatizable classes of locally free algebras of various type. In III Benjamin Franklin Wells, editor, The Metamathematics of Algebraic Systems: Collected Papers 1936{1967, chapter 23, pages 262{281. North Holland, 1971.
[22] Rohit Parikh. A decidability result for a second order process logic. In 19th Annual Symposion on Foundations of Computer Science, pages 177{183, Ann Arbor, Michigan, October 1978. IEEE.
[23] Michael O. Rabin. Decidability of secondorder theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1{35, 1969.
[24] William C. Rounds and Robert Kasper. A complete logical calculus for record structures representing linguistic information. In Proceedings of the First Symposium on Logic in Computer Science, pages 38{43, Cambridge, MA, June 1986. IEEE Computer Society.
[25] Gert Smolka. Feature constraint logics for unification grammars. Journal of Logic Programming, 12:51{87, 1992.
[26] Gert Smolka. The definition of Kernel Oz. In Andreas Podelski, editor, Constraints: Basics and Trends, Lecture Notes in Computer Science, vol. 910, pages 251{292. SpringerVerlag, March 1995.
[27] Gert Smolka and Hassan A?tKaci. Inheritance hierarchies: Semantics and unification. Journal of Symbolic Computation, 7:343{370, 1989.
[28] Gert Smolka and Ralf Treinen. Records for logic programming. Journal of Logic Programming, 18(3):229{258, April 1994.
[29] Wolfgang Thomas. Automata on infinite objects. In van Leeuwen [32], chapter 4, pages 133{191.
[30] Ralf Treinen. A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14(5):437{457, November 1992.
[31] Ralf Treinen. Feature constraints with firstclass features. In Andrzej M. Borzyszkowski and Stefan Soko lowski, editors, Mathematical Foundations of Computer Science 1993, Lecture Notes in Computer Science, vol. 711, pages 734{743. SpringerVerlag, 30 August{3 September 1993.
[32] Jan van Leeuwen, editor. Handbook of Theoretical Computer Science, volume B  Formal Models and Semantics. Elsevier Science Publishers and The MIT Press, 1990.