Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. In Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 1425, Warsaw,Poland, June 1997. IEEE Comp. Soc. Press.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....is proved in [CD94] More general sort constraints involving some second order terms are studied in [Com98b] with applications to a sort constrained equational logic [Com98a] 3. 6 Bibliographic Notes 109 Sort constraints are also applied to speci cations and automated inductive proofs in [BJ97] where tree automata are used to represent some normal forms sets. They are used in logic programming and automated reasoning [FSVY91, GMW97] in order to get more e cient procedures for fragments which fall into the scope of tree automata techniques. They are also used in automated deduction in ....

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings, 12 in Computer Science [IEE97].

.... 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] which are also fundamental, e.g. in temporal and program logics [14] Two way automata, a.k.a. pushdown ....

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In LICS'97, 1997.

....There is, as mentioned in section 3.5, a third camp, using the initial ideas of implicit induction to produce test set induction techniques. Adel Bouhoula and his team are continuing to develop SPIKE, a theorem prover utilising this technique and also a new automata based one proposed in [BJ97]. They point out that it not only performs well but also, our method seems to yield very natural proofs . When [KZ] is published, it may open up another area of development using their method of quantified induction hypotheses, implemented using cover sets. So we conclude that implicit ....

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings of the 12th IEEE Symposium on Logic in Computer Science - LICS'97, June-July 1997.

.... 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] which are also fundamental, e.g. in temporal and program logics [13] Two way automata, a.k.a. pushdown ....

A. Bouhoula and J.-P. Jouannaud. Automatadriven automated induction. In LICS'97, 1997.

....and its predecessors, and indeed, can be considered extensions of OBJ3. There is also exciting new work in term rewriting [11] which is the basis for implementing systems like OBJ3, Maude and CafeOBJ) for example in France around Prof. Jean Pierre Jouannoud, on induction and termination proofs [5], including the spike [4] and CiME systems. The issues discussed in this paper seem to be of increasing importance for computer science, and I think we can look forward to continuing progress. ....

Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. In Proceedings, 12th Symposium on Logic in Computer Science, pages 14--25. IEEE, 1997.

.... in SPIKE [Bouhoula and Rusinowitch 1995] and cover sets are the basis of the mechanization of induction in (a part of) RRL [Kapur and Zhang 1995] Ground normal form languages and their recognizers play a role in specification analysis in ReDuX and in the design of new induction techniques [Jouannaud and Bouhoula 1997]. The decidability of ground reducibility was shown originally by D. Plaisted [Plaisted 1985] and several other algorithms have been proposed since. We sketch here two of them: one is based ond tree automata with constraints along the lines of [Caron et al. 1993] The second one is based on test ....

Jouannaud J.-P. and Bouhoula A. [1997], Automata-driven automated induction, in `Twelfth Annual IEEE Symposium on Logic in Computer Science', IEEE Comp. Soc. Press, Warsaw, Poland.

....at least doubly exponential. When we stick to the decision problem, it is EXPTIME complete [Comon and Jacquemard 1997] Finally, ground reducibility tests can also be used directly in the transformation of the original set of axioms yielding more powerful (resp. efficient) techniques [Comon 1989, Bouhoula and Jouannaud 1996]. All these techniques have been actually developed in the framework of equational theories. They carry over to clauses with equality, with the provision that, in general, there is no known axiomatization A for which the consistency of e [A can be decided for every equation e. Nevertheless, it is ....

Bouhoula A. and Jouannaud J.-P. [1996], Automata-driven automated induction, Technical report, SRI-CSL. http://www.loria.fr/ bouhoula.html, //www.lri.fr/people/jouannau.html.

....to that of OBJ, and indeed can be considered versions of OBJ. There is also exciting new work in term rewriting [16] which is the basis for implementing systems like OBJ3, Maude and CafeOBJ) for example in France around Jean Pierre Jouannoud and Adel Bouhoula, on induction and termination proofs [9], including the spike and CiME systems [8] and some new work on proving behavioral properties with a similar technology [3] The issues discussed in this paper seem to be of increasing importance for computer science, and I think we can look forward to continuing progress. ....

Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. In Proceedings, 12th Symposium on Logic in Computer Science, pages 14--25. IEEE, 1997.

No context found.

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. Information and Computation, 169(1):1--22, 2001.

No context found.

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. Information and Computation, 169(1):1--22, 2001. 14

No context found.

Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. In Proc. 12th IEEE Symp. LICS, Warsaw, 1997.

....methods can hardly be guided, hence they rarely terminate. The other methods need a lot of user interaction and usually require that A preliminary version of the results has been presented at the 12th IEEE Symposium on Logic in Computer Science, Warsaw (Poland) IEEE Comp. Soc. Press, 1997 [5]. This work was done while the authors were on leave at SRI International. constructors are free and functions are completely defined. SPIKE improves over the others by computing particular induction schemas tailored to the problem at hand in order to trigger the induction proof, while ....

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings 12th IEEE Symposium on Logic in Computer Science, Warsaw (Poland), pages 14--25, June-July 1997.

....practice. A familiar example is provided by the specification of integers with the non free constructors s, for successor, and p, for predecessor. Such specifications can be transformed automatically by computing the types on which the constructors become free [11] This technique is exploited in [8] to automate inductive proofs. We use it here to compute the recursor on integers, via the recursors operating on the subtypes Zero, Pos and Neg. These types can be seen as states of a bottom up tree automaton, the subtype relationship defining empty transitions in this automaton, and the ....

....omitted. The resulting recursor must satisfy the schema, since the rules corresponding to the subtype definitions are not recursive. A more complex solution to the problem of non free constructors is given in [1] Our method can also cope with associative commutative constructors as discussed in [8]. 5.4 Mutually Recursive Definitions The specification of ordinals given in section 3 is not quite satisfactory, since the ordinals below are not identified with the natural numbers. We now remedy to this situation by using Nat as a subtype of Ord. The resulting specification makes use of ....

Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. Technical report, SRI-CSL, 1996. http://www.loria.fr/ bouhoula.html, //www.lri.fr/people/jouannau.html.

.... a detailed model theoretic study of the logic and the semantic connections with order sorted and partial equational logics [21] an original study of the tree automata based inductive theorem proving techniques that are further developped here within the framework of membership equational logic [2]. We describe our Horn clause language in section 3. Functional computations with these Horn clauses is described in section 4, where are introduced confluence, type decreasingness, and regularity, which are further investigated in section 5. Relationships with tree automata are investigated in ....

....is a set of membership rules whose head contains a defined symbol and which are inductive consequences of R, then (C [D;R[M 0 ) is also ground confluent. Operational completeness becomes undecidable in presence of conditional rewrite rules. A complete test is based on the notion of a pattern [2]: Definition 33 A pattern is an order sorted term (f(T ) fx : sg) such that f 2 D and T i 2 T (C; Var(T ) for each T i 2 T . 3 Our test computes pattern trees for the defined symbols. A pattern tree for f 2 D K K at sort s 2 K is a tree whose nodes are labeled by patterns, whose root is ....

[Article contains additional citation context not shown here]

Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. submitted, 1996.

No context found.

Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. In Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 1425, Warsaw,Poland, June 1997. IEEE Comp. Soc. Press.

No context found.

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings, 12 in Computer Science [IEE97].

No context found.

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings, 12 in Computer Science [IEE97].

No context found.

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings, 12 in Computer Science [IEE97].

No context found.

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings, 12 in Computer Science [IEE97].

No context found.

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings, 12 in Computer Science [IEE97].

No context found.

A. Bouhoula and J.-P. Jouannaud. Automata-driven automated induction. In Proceedings, 12 in Computer Science [IEE97].

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.