J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1-33, 1989.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....as complete. It must be the case that for any ground substitution g of variables in f(x 1 ; xn ) some rule f(s i 1 ; s i n ) r i if cond i from the de nition of f must be applicable on g (f(x 1 ; xn ) Below we review a generalization of the methods discussed in [7, 11] so that de nitions given using linear terms can also be checked for completeness using PA. Checking for completeness amounts to constructing a formula that is a disjunction of conditions under which each rule covers the arguments of f . Assuming that x 1 ; xn are new variables not ....

....arithmetic, the existential quanti ers can be eliminated, and the above formula simpli es to: u = 0) v = 0) v u u 0) u v v 0) a valid formula in Presburger arithmetic. The cover set generated from the de nition of gcd is, thus, complete. Methods discussed in [7, 11] cannot be used to prove the completeness of gcd since they depend upon the use of completion procedures; the completion procedure would not terminate on the de nition of gcd. If a formula generated for checking completeness is not valid, then the de nition of f may or may not be complete ....

J.-P. Jouannaud and E. Kounalis, \Automatic proofs by induction in theories without constructors," Information and Computation 82, 1-33, 1989.

.... proof method to other theorem proving methods, such as, i) methods based on the Clark completion [6, 18] ii) methods based on resolution augmented by the negation as ( nite or in nite) failure rule [1, 22] iii) methods based on induction, and (iv) the proof by consistency method [14, 15, 19]. 2 Preliminaries In presenting our proof method we consider locally strati ed logic programs. Let us begin by recalling some basic de nitions. For notions not de ned here the reader may refer to [1, 18, 22] The formulas and programs we consider are constructed by using a xed rst order ....

.... these methods we would like to mention the following ones: i) the method based on the Clark completion [6, 18] ii) the methods based on resolution augmented by the negation as ( nite or in nite) failure rule [1, 22] iii) the methods based on induction, and (iv) the proof by consistency method [14, 15, 19]. i) The method based on the Clark completion amounts to prove that M(P ) j= by showing that comp(P) where comp(P) denotes the Clark completion of program P . Equivalently, since the Lloyd Topor transformation from f to F (f; preserves the completion semantics, one may show that ....

[Article contains additional citation context not shown here]

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):133, 1989.

....we can exhibit a witness of probable inconsistency. Such a witness can typically be a critical pair of the form true = false (a la Musser [28] or a relation between constructors 0 = s(x) a la HuetHullot [22] or more generally the failure of a ground reducibility test (a la Jouannaud Kounalis [23]) Therefore we change our mind and instead of trying to prove the proposition Q, we are going to disprove it, that is to prove its negation: T h; Th u : 8x ( x 2 ) Q(x) which is equivalent to: T h; Th u ; 8x ( x 2 ) Q(x) which could be internalized as before but without the ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1-33, 1989.

....reducibility decision. 1 Introduction Ground reducibility of a term t w.r.t. a term rewriting system R expresses that all ground instances (instances without variables) of t are reducible by R. This property is fundamental in automating inductive proofs in equational theories without constructors [9]. It is also related to sufficient completeness in algebraic specifications (see e.g. 11] Roughly, it expresses that all cases have been covered by R and that t will be reducible for any inputs. Many papers have been devoted to decision of ground reducibility. Let us report a brief history of ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.

.... proof method to other theorem proving methods, such as, i) methods based on the Clark completion [34, 103] ii) methods based on resolution augmented by the negation as ( nite or in nite) failure rule [4, 127] iii) methods based on induction, and (iv) the proof by consistency method [86, 89, 109]. 5.3.1 Translating First Order Formulas into Logic Programs In this section we present a method that given a locally strati ed program P and a closed rst order formula in L, introduces a new predicate f and constructs a locally strati ed program P F (f; such that M(P ) j= i M(P F ....

.... ones: i) the method based on the Clark completion [34, 103] ii) the methods based on resolution augmented by the negation as ( nite or in nite) failure rule [4, 127] iii) the method based on partial evaluation [21] iv) the methods based on induction, and (v) the proof by consistency method [37, 86, 89, 109]. i) The method based on the Clark completion amounts to prove that M(P ) j= by showing that comp(P) where comp(P) denotes the Clark completion of program P . Equivalently, since the Lloyd Topor transformation from f to F (f; preserves the completion semantics, one may show that ....

[Article contains additional citation context not shown here]

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):133, 1989.

....let us skip problem P3 for a moment and turn to problem P4 which has now a more than ten years history. The problem, known under the name of ground reducibility problem, has attracted a lot of attention in the area of term rewriting [DJ90] because of its application to automated inductive proofs [JK89]. The problem consists of testing if all instances of a given tree pattern p have a subtree matched by one of the patterns of a given set S. Once again, non linear variables in patterns of S make the problem much more dicult. In the middle and late 80 s, several authors observed that the problem ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1-33, 1989.

.... proof method to other theorem proving methods, such as, i) methods based on the Clark completion [7, 19] ii) methods based on resolution augmented by the negation as ( nite or in nite) failure rule [1, 23] iii) methods based on induction, and (iv) the proof by consistency method [15, 16, 20]. 3 2 Preliminaries In this section we recall some basic de nitions concerning locally strati ed logic programs and perfect models. For notions not de ned here the reader may refer to [1, 19, 23] The formulas and programs we consider are constructed by using a xed rst order language L. ....

.... ones: i) the method based on the Clark completion [7, 19] ii) the methods based on resolution augmented by the negation as ( nite or in nite) failure rule [1, 23] iii) the method based on partial evaluation [4] iv) the methods based on induction, and (v) the proof by consistency method [8, 15, 16, 20]. 16 (i) The method based on the Clark completion amounts to prove that M(P ) j= by showing that comp(P) where comp(P) denotes the Clark completion of program P . Equivalently, since the Lloyd Topor transformation from f to F (f; preserves the completion semantics, one may show ....

[Article contains additional citation context not shown here]

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):133, 1989.

....induction relation is explicitly given (e.g. by the recursions of a function) and using this relation base and step formulas are constructed. But there has also been a lot of work based on the implicit induction principle (also called proof by consistency or inductionless induction ) cf. e.g. [2, 4, 35, 37, 38, 40, 65]. However, these approaches are also restricted to terminating functions (i.e. the specification has to be given by a terminating term rewriting system) Then the rewrite ordering of this system is implicitly used for induction proofs. 9. Conclusion Partial functions are important in many ....

Jouannaud, J.-P. and Kounalis, E., `Automatic Proofs by Induction in Theories Without Constructors', Information and Computation 82, 1-33 (1989).

....data structure under consideration. As proved earlier, an induction scheme generated using a complete cover set is sound. This is ensured if the terminating rewrite rules defining a function whose left sides are used as the basis for constructing the cover set, completely define the function. In [5, 8], algorithms for checking completeness of constructor based definitions expressed as terminating rewrite rules arithjar.tex; 14 06 1995; 17:08; no v. p.30 30 Deepak Kapur and M. Subramaniam are discussed; for background information on this topic, an interested reader may also consult [6] For ....

J.-P. Jouannaud and E. Kounalis, "Automatic proofs by induction in theories without constructors, " Information and Computation 82, 1-33, 1989.

....a normal form is a ground term which not only is not an instance of a term from a given set S, but also does not contain a subterm which is such an instance. There exists an extensive literature devoted to ground reducibility, the set of normal forms and related issues (some sample references are [KNZ86, JK89, BK89, Com91, HH94]) Related complexity questions have also been studied (see [Pla85, KT95, KNRZ91, KR95a, KR95b, CJ97] However, to the best of our knowledge, no work has been done on analyzing complexity problems related to complement representation. The only result, trivially implied by the Lassez and Marriot s ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1{ 33, 1989.

....and the image is recognizable. It is conjectured true when the image is recognizable [8] The result can also be used to decide properties of term rewrite systems. When a rewrite system R has good properties (same occurrences of a variable are brothers : it includes the case of shallow systems [11]) it gives a procedure to test recognizability of the set of normal forms of R which is much easier than the general one and it allows testing whether the set of direct descendants R(L) is recognizable for a recognizable language L: testing these properties can be useful e.g for computing ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1--33, July 1989.

...., both equations are SP 0 convergent and thus SP 0 joinable (Definition 10.33) i.e. u Gamma SP 0 v Gamma SP 0 t Gamma SP 0 v 0 Gamma SP 0 u 0 for some v; v 0 . Since SP 0 is confluent, v and v 0 and thus u and u 0 are SP 0 joinable. ut 23 This generalizes [JK89] Theorem 1, to conditional axioms. Peter Padawitz Secondly, we modify the definition of subjoinability (Definition 10.41) Definition 10.53 (SP 0 subjoinability) Given a subspecification SP 0 of SP and a binary relation on goals, a Horn clause p ( H is SP 0 subjoinable below a ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1--33, 1989.

....In this framework, the system Nqthm was developed, which was for many years the only significant automated theorem proving system for induction. However, Nqthm often requires interaction with the user. The second approach involves a proof by consistency: this is the inductionless induction method [706, 509, 550, 540, 520, 355, 598, 46, 427, 802]. However, both methods have many limitations on the theorems that can be proved and on the underlying theory. Indeed, guiding a proof by explicit induction requires some skill in finding the right axioms or hypotheses to apply. On the other hand, the proof by consistency technique does not ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1--33, 1989. \Phi.

....theories of interest include AC operators, which are hard to handle since they cause divergence or generate complex proofs. To overcome this problem, we propose to have the AC axioms built in the inference mechanism of SPIKE. The advantage of our approach over other implicit induction techniques [5, 9], is that it does not use AC unification (which is doubly exponential) during the proof process, but only AC matching. In this paper, we propose methods for automatically selecting the induction variables of a conjecture to be proved, and for constructing test sets in the case of an AC conditional ....

....defined AC operators, nb pos ind( 1 and nb pos ind( 1, we can choose fx; wg or fy; wg or fz; wg as induction variables. Thus, we obtain only 4 lemmas to prove. 5 Computing test sets The computation of test sets according to definition 3. 4 relies on the inductive reducibility property [9], which is unfortunately undecidable in AC theories [10] However we can use a semi decision procedure that has proved to be quite useful for practical applications [11] For the more restricted case where the rewrite system is left linear and sufficiently complete, and the relations between ....

[Article contains additional citation context not shown here]

J.-P. Jouannaud, E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1--33, 1989.

....theorem proving system that supports a cover set method which is closely related to Boyer and Moore s approach. Within the last decade, the proof by consistency approach, which is based on rewriting and completion techniques, has been developed in [30] and has been re ned in several ways in [23,22,24,20,29,3,38]. However, both approaches have limitations. Guiding a proof by explicit induction requires some skill in nding the right axioms or hypotheses to apply. On the other hand, a proof using consistency techniques does not require guidance from the user since the generation of lemmas is performed ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:133, 1989.

....theories of interest include AC operators, which are hard to handle since they cause divergence or generate complex proofs. To overcome this problem, we propose to have the AC axioms built in the inference mechanism of SPIKE. The advantage of our approach over other implicit induction techniques [BK89, JK89], is that it does not use AC unification (which is doubly exponential [KN92] during the proof process, but only AC matching. In this paper, we propose methods for automatically selecting the induction variables of a conjecture to be proved, and for constructing test sets in the case of an AC ....

....n) exp(y; n) fg, read var(exp(x; n) exp(y; n) fg We select the first scheme since it does not change any read variable. The proof of C succeeds in this case. 5 Computing test sets The computation of test sets according to definition 3. 4 relies on the inductive reducibility property [JK89], which is unfortunately undecidable in AC theories [KNRZ91] However we can use a semi decision procedure that has proved to be quite useful for practical applications. For the more restricted case where the rewrite system is left linear and sufficiently complete, and the relations between ....

[Article contains additional citation context not shown here]

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1--33, 1989.

....algorithm, which leads to more effective decision procedures. Introduction Ground reducibility of a term t with respect to a term rewriting system R is the property that all ground instances of t are reducible by R. This property is used in automatic proof by induction in equational theories [10, 1], in proving properties of equational specifications [11] and in constraint solving in quotient algebras [9] Ground reducibility has been shown decidable in the general case by D. Plaisted [15] D. Kapur et al. 11] E. Kounalis [12] Recently, some of us proved a more general result : the first ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1--33, July 1989.

....For example, D. Musser [22] assumes that E contains an equational axiomatization of equality, and A is the set ftrue 6= falseg. G. Huet and J. M. Hullot [15] assume a constructor theory and A expresses that two pure constructor terms are distinct (see also [21] J. P. Jouannaud and E. Kounalis [16] and L. Bachmair [1] assume that E is given by a ground convergent rewrite system (see also [17] then A expresses that two equal terms should be ground reducible. This last notion plays a central role in further developments of inductionless induction, as will be explained later. Now, the second ....

....the deduction system consists in some restrictions of the Knuth Bendix completion procedure, as explained in [2, 13] This corresponds actually to apply an (implicit) induction scheme. Besides the proof methods, several works have been devoted to the decision of ground reducibility (e.g. [16, 23, 19, 18], 20, 5, 8] For arbitrary rewrite systems, the problem has been shown decidable by D. Plaisted [23] However, the complexity of the decision algorithm is so high (a tower of 7 exponentials) that several other methods have been proposed afterwards. In the general case, the problem, including the ....

[Article contains additional citation context not shown here]

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.

....was a method for proving inductive theorems proposed in [23] which does not require the underlying system to be conAEuent, not even on ground terms. Therefore this step may be skipped when using the just mentioned method. 3. prove in R 2 by consistency [27, 32] or by inductive reducibility [31, 33], with a possible involvement of Fribourg s method [16] or even the more general Bachmair s one [2] an inductive theorem, derived from the structure of the generated in nite family of rules, and add it as a rule to the existing system R 2 , producing R 0 2 , 4. add the rules removed in step 1 ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1 33, 1989.

....all the axioms of NAT, i.e. A # Alg(NAT) In order to check the fact that I(NAT) # A, one can observe that the enrichment of NAT by a constant c : Nat and these equations forms a terminating rewrite system this just makes it possible to prove its consistency wrt. NAT by methods suggested in [JK89, Kir92]. To complete the proof, we suggest the following interpretation of div on A that satisfies (1) div A (n, 0) div A (c, n) c; div A (n,c) 0; div A (c,c) 1; div A (n, n # ) k for all n, n # # N, n # 0 where k # N is the quotient of integer division n on n # . Note that ....

Jouannaud J.-P., Kounalis E. Automatic proofs by induction in theories without constructors. Information and Computation, 82, 1:1-33 1989.

....ground reducibility. 1 Introduction Ground reducibility of a term t w.r.t. a term rewriting system R expresses that all ground instances (instances without variables) of t are reducible by R. This property is fundamental in automating inductive proofs in equational theories without constructors [10]. It is also related to sufficient completeness in algebraic specifications (see e.g. 12] Roughly, it expresses that all cases have been covered by R and that t will be reducible for any inputs. Many papers have been devoted to decision of ground reducibility. Let us report a brief history of ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.

.... proof by induction have been developed for non parameterized speci cations: The rst type applies explicit induction arguments on the term structure [ Aubin, 1979; Boyer and Moore, 1988; Bundy et al. 1993 ] The second type involves a proof by consistency [ Musser, 1980; Huet and Hullot, 1982; Jouannaud and Kounalis, 1989; Fribourg, 1989; K#chlin, 1989; Bachmair, 1988; Gramlich, 1989 ] More recently, new methods were developed that do not rely on the completion framework [ Kounalis and Rusinowitch, 1990; Reddy, 1990; Bouhoula et al. 1995; Bouhoula and Rusinowitch, 1995 ] The inductive theory of a ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:133, 1989.

....A that can be found in the Literature . 23 5.1 Musser s approach [Musser 1980] 23 5.2 Huet and Hullot s method [Huet and Hullot 1982] 26 5. 3 Jouannaud and Kounalis approach [Jouannaud and Kounalis 1989] . 28 5.4 Bachmair s approach [Bachmair 1988] 31 5.5 Further examples of normal axiomatizations . 32 6 Ground Reducibility . ....

....restrictions of the Knuth Bendix completion procedure, as explained in [Bachmair 1991, Fribourg 1989] This corresponds actually to apply an (implicit) induction scheme, for purely equational specifications. Besides the proof methods, several works have been devoted to ground reducibility (e.g. [Jouannaud and Kounalis 1989, Plaisted 1985, Kapur, Narendran and Zhang 1987, Kapur, Narendran, Rosenkrantz and Zhang 1991] Kounalis 1992, Caron, Coquid e and Dauchet 1993, Comon and Jacquemard 1994] For arbitrary rewrite systems, the problem has been shown decidable by D. Plaisted 6 Hubert Comon [Plaisted 1985] ....

[Article contains additional citation context not shown here]

Jouannaud J.-P. and Kounalis E. [1989], `Automatic proofs by induction in theories without constructors', Information and Computation 82(1).

.... test sets [BR93] are developed which, combined with a reduction ordering, allow for inductive proofs. In many cases the test or cover sets can be computed from the specification. No partiality is allowed here. For unconditional specifications the method proof by consistency is known [HH82] [JK89], KM87] Bac88] Red90] Again, no partiality is allowed, the rewrite system induced by the specification has to be terminating. For unconditional partial specifications we refer to [KM86] We have already commented on that. This paper gives a unifying presentation on the work carried out in ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1--33, 1989.

....without variables) of t are reducible by R. This property, which is also known as quasi reducibility and inductive reducibility , has been used by several authors for proving properties of algebraic specifications (the sufficient completeness) as well as in inductive theorem proving (see [3, 6, 9 15] among others) Ground reducibility has been shown to be decidable for an arbitrary rewrite system by D. Plaisted [15] Further decidability proofs where given by Kapur, Narendran and Zhang [11] and Kounalis [13] These three proofs are based on a test set method: they show that there is a bound ....

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.

No context found.

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1-33, 1989.

No context found.

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1-33, 1989.

....to the general agreement that provers should be interactive and free the user from routine tasks, including simple inductive proofs, the problem investigated in this paper. Four main solutions have been explored for semi automating induction: the generalization of KnuthBendix completion techniques [22]; the integration of cooperating decision procedures, among which advanced model checking methods, as done in PVS [29] the use of sophisticated heuristics for guiding the search, as in NQTHM or RRL [8,30] the definition of powerful simplification rules allowing for mutual induction, available in ....

....specifications, completeness of definitions. The idea is that any term should return a result built upon constructor symbols, together with its sort when evaluated. Algorithms found in the literature assume either that constructors are free [3] or that rules for defined symbols are unconditional [22]. We assume instead a complete specification coming in two parts: a complete specification of constructor symbols C, and a complete specification of defined symbols D, which we proceed to define. 4.1 Complete Specifications of Constructors Throughout this section, we assume given a specification ....

[Article contains additional citation context not shown here]

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.

....the general agreement that provers should be interactive and free the user from routine tasks, including simple inductive proofs, the problem investigated in this paper. Four main solutions have been explored for semi automating induction: the generalization of Knuth Bendix completion techniques [12]; the integration of cooperating decision procedures, among which advanced model checking methods, as done in PVS [15] the use of sophisticated heuristics for This work was done while the authors were on leave at SRI International, and has been partially supported by the Information Technology ....

....specifications, completeness of definitions. The idea is that any term should return a result built upon constructor symbols, together with its sort when evaluated. Algorithms found in the literature assume either that constructors are free [1] or that rules for defined symbols are unconditional [12]. We assume instead a complete specification coming in two parts: a complete specification of constructor symbols C, and a complete specification of defined symbols D, which we proceed to define. 4.1 Complete Specifications of Constructor Symbols Constructor symbols may be free for some sorts, ....

[Article contains additional citation context not shown here]

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), 1989.

No context found.

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1-33, 1989.

No context found.

J. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1--33, 1989.

No context found.

J. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1--33, 1989.

No context found.

J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:133, 1989.

No context found.

JK89 J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1--33, 1989.

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.