Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297318, 1994.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....example of Section 3. Related Work. There is much literature on finite tree automata [9, 17] Apart from the already cited use in cryptographic protocol verification, applications include approximat2 ing reachability sets for rewrite systems [18] disunification and inductive reducibility [30], unification under constraints [26] ground reducibility [10] automated inductive theorem proving [5] fast tree matching [28] automated model building in first order logic [37] etc. These applications deal with automata on finite trees. We won t deal with automata on infinite trees [42] ....

D. Lugiez and J. L. Moysset. Tree automata help one to solve equational formulae in ACtheories. Journal of Symbolic Computation, 18(4):297--318, 1994.

....by the results of Section 4. Related Work. There is much literature on finite tree automata [9, 16] Apart from the already cited use in cryptographic protocol verification, applications include approximating reachability sets for rewrite systems [17] disunification and inductive reducibility [28], unification under constraints [24] ground reducibility [10] automated inductive theorem proving [5] fast tree matching [26] automated model building in first order logic [34] etc. These applications deal with automata on finite trees. We won t deal with automata on infinite trees [39] ....

D. Lugiez and J. L. Moysset. Tree automata help one to solve equational formulae in ACtheories. Journal of Symbolic Computation, 11, 1994.

....of the derivation tree. One main difficulty in compiling strategies is to handle search in non deterministic computations, which leads to use set choice points and jump operations. 2. 3 AC matching AC matching has already been extensively studied, for instance in [Hul80, BKN87, KL91, LTV93, LM94, Eke95] A term t is said to AC match another term s if there exists a substitution oe such that toe =AC s. For example, let us assume that f(x; f(g(a; y) z) is the pattern and f(a; f(g(a; b) c) is the subject. If none of the symbols is AC, there is a substitution fx 7 a; y 7 b; z 7 cg ....

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in AC-theories. Journal of Symbolic Computation, 18(4):297--318, 1994.

....could provide with the specification associated with the normal form automaton. Besides being non natural in many cases, this is not always possible. Data structures like graphs or bags are inherently non free, and require further developments of our technique based on a work by Lugiez and Moysset [25]. This is briefly sketched in Section 7. The main novelty of our method is the use of the normal form automaton associated with the subspecification of constructors in order to transform a conjecture clause into new clauses whose all terms inhabit free sorts. The computation of the automaton ....

....and can be encoded as Boolean functions. Another case is when the constructors satisfy equations among associativity (A) commutativity (C) identity (U) and idempotency (I) The conditions under which a constructor may satisfy such axioms express the existence of the associated kind of automaton [25]: i) A, U and I always come along with C, ii) these equations hold for a binary constructor c at a sort where c is free. This assumes that, in this case, the sorts on which the constructor c is free are given beforehand. iii) non linear variables may not appear in left hand sides immediately ....

[Article contains additional citation context not shown here]

D. Lugiez and J.-L. Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297--318, 1994.

....could provide with the specification associated with the normal form automaton. Besides being non natural in many cases, this is not always possible. Data structures like graphs or bags are inherently non free, and require further developments of our technique based on work by Lugiez and Moysset [14], which are briefly sketched in conclusion. The main novelty of our method is the use of the normal form automaton associated with the subspecification of constructors in order to transform a conjecture clause into new clauses whose all terms inhabit free sorts. The computation of the automaton ....

....constraints. Another important case is when the constructors satisfy equations among associativity (A) commutativity (C) identity (I) and idempotency (Z) The conditions under which a constructor may satisfy such axioms express the existence of the associated kind of automaton [14]: i) A, I and Z always come along with C, ii) these equations hold for a binary constructor c at a sort where c is free. This assumes that, in this case, the sorts on which the constructor c is free are given beforehand. iii) non linear variables may not appear in left hand sides immediately ....

D. Lugiez and J.-L. Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297--318, 1994.

....the application of this rule fails. Conditional rewriting requires AC matching problems to be solved in a particular way: the first solution has to be found as fast as possible, and the others have to be found on request . AC matching has already been extensively studied, for instance in [16,2,20,1,21,9]. Usually all terms in the same AC equivalence class are represented by their canonical form [16,9] Given a total ordering on the set of function symbols F and variables, the canonical form is obtained by flattening nested occurrences of the same AC function symbol, recursively computing the ....

D. Lugiez and J.-L. Moysset. Tree automata help one to solve equational formulae in AC-theories. Journal of Symbolic Computation, 18(4):297--318, 1994.

....conditions on the terms recognized so far at states in s before to apply the transition from s to s labelled by the function symbol f . It is also possible to express associativity, commutativity, identity and idempotency, by labelling the transitions with formulae of Presburger s arithmetic [19]. 7 Induction schemas In this section, we relate normal form automata and induction. Definition 22 Given a CRMS R, a term (T ; Gamma) is said to be ground reducible (resp. irreducible, sortable) if T fl is reducible (resp. irreducible, sortable) for each irreducible admissible ground ....

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297-- 318, 1994.

No context found.

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297318, 1994.

....decidable for nite S (see Plaisted [Pla85] Complement problems are also introduced in automated deduction. They are the subject of Exercises 14 and 15. The complement problem for linear terms was proved decidable by Lassez and Marriott [LM87] and the AC complement problem by Lugiez and Moysset [LM94] The reachability problem is de ned in Exercise 16. It is well known that this problem is undecidable in general. It is decidable for rewrite systems preserving recognizability, i.e. such that for every recognizable tree language L, the set of reductions of terms in L by S is recognizable. This ....

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297318, 1994.

No context found.

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297318, 1994.

No context found.

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297318, 1994.

No context found.

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297318, 1994.

No context found.

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297318, 1994.

No context found.

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297318, 1994.

....are still restricted to syntactical objects such as trees, which is a strong restriction for theorem proving application where we need to incorporate interpreted domains like multisets, integers, Little work has been done to see how tree automata could be extended in such cases. In [LM94] we introduced tree automata to deal with sets and multisets but this approach solves only cases of non linear definitions which seldom appear in automated deduction applications. In this area, we often write definition rules of the following kind, which combines syntactical symbols (div in this ....

....discussed a similar approach for defining recognizable sets of feature trees which are special trees which also have an unbounded width. Each of these work provide the reader with the corresponding notion of tree automata. Combining constraints and associative commutative symbols has been done in [LM94] but the non linearity treated is restricted inside multisets, contrary to the present paper. Currently, the complexity of our decision algorithm is very high. Unfortunately there is no hope to get low bounds since the problem of deciding if a non deterministic (usual) tree automaton accepts all ....

Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in AC-theories. Journal of Symbolic Computation, 18(4):297--318, 1994.

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.