H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, cycle-syntacticness, and shallow theories. Information and Computation, 111(1):154--191, 1994.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....: x ar(f) y are distinct variables. Hence, for con uent, suciently complete TRSs, the redundancy problem is reduced to the problem of checking validity of a particular class of inductive theorems. The problem of identifying the inductive theory of a TRS is in general undecidable, as shown by [11] even for a very restricted class of TRSs: nite, canonical, left and right linear, and right monadic (right hand sides have depth at most 1) CSs. However, several methods for (semi) automatically proving validity of inductive theorems have been developed, such as the cover set method [28] test ....

....and right monadic (right hand sides have depth at most 1) CSs. However, several methods for (semi) automatically proving validity of inductive theorems have been developed, such as the cover set method [28] test set method [9] rewriting induction method [25] and inductionless induction method [10, 11], which generalizes the former ones. Also, the abstract rewriting method of [8] can be used for proving inductive theorems. In the following, we show how, both the inductionless induction as well as abstract rewriting methods can be successfully applied for detecting redundancy of arguments, ....

[Article contains additional citation context not shown here]

H. Comon and R. Nieuwenhuis. Induction = I-Axiomatization + First-Order Consistency. Information and Computation, 159(1/2):151-186, 2000.

....r##criture terminant, conAEuent et complet. Mots cl# : Th#ories #quationnelles, preuve par induction, interpr#tation abstraite, r##criture 1 Introduction In the eld of automatic deduction, the proof of (positive) inductive theorems on equational specications has already been widely investigated [Red90, KZ95, BR95, Com94, CN98, GS92]. Starting from an equational specication E and from an equation s = t those techniques try to prove that s = t is true in the initial model of E and thus prove that s = t is true in every Herbrand model. This implies that s = t is an inductive theorem of E. As far as we know, the proof of ....

....of the two techniques in every cases. What should be also investigated is if proving negative properties of equational speci cation may ooeer a way to nd axiomatisation for the smallest Herbrand model of a theory. This would be useful in proof techniques like jinductionless inductionj [CN98]. ....

H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + rst-order consistency. Information and Computation, 1998.

....it is able to refute in finite time conjectures which are inconsistent with the set of hypotheses. When originally proposed, this technique was of limited applicability. Recently, Comon and Nieuwenhuis have drawn together and extended previous research to show how it may be more generally applied, [10]. They describe an experimental implementation of the inductive completion part of the system. However, the check for refutation or consistency was not implemented. This check is necessary in order to ensure a theorem is correct, and to automatically refute an incorrect conjecture. We have ....

....the infinite state problem, and assumes an arbitrary number of protocol participants, but proofs are tricky and require days or weeks of expert effort. If a proof breaks down, there are no automated facilities for the detection of an attack. 3 The Comon Nieuwenhuis Method Comon and Nieuwenhuis, [10], have shown that the previous techniques for proof by consistency can be generalised to the production of a first order axiomatisation A of the minimal Herbrand model such that A [ E [ C is consistent if and only if C is an inductive consequence of E. With A satisfying the properties they define ....

[Article contains additional citation context not shown here]

H. Comon and R. Nieuwenhuis. Induction = IAxiomatization + First-Order Consistency. Information and Computation, 159(1-2):151--186, May/June 2000.

....proof by implicit induction of the commutativity of gcd. This had been posed as a challenge problem to the technique in the past. 1 Overview of The System Comon and Nieuwenhuis described the operation of a refutation complete proving system based on an implicit induction strategy in their paper, [1], but their implementation was not complete. We have produced a complete implementation, described in figure 1. The input to the system is an inductive problem in Saturate format and an I Axiomatisation (as defined by Comon and Nieuwenhuis, see [1] The version of Saturate customised by ....

....on an implicit induction strategy in their paper, 1] but their implementation was not complete. We have produced a complete implementation, described in figure 1. The input to the system is an inductive problem in Saturate format and an I Axiomatisation (as defined by Comon and Nieuwenhuis, see [1]) The version of Saturate customised by Nieuwenhuis for implicit induction (the rightmost box in the diagram) gets the problem file only, and proceeds to pursue inductive completion. Every non redundant clause generated is passed via the server to the refutation control program (the leftmost ....

[Article contains additional citation context not shown here]

H. Comon and R. Nieuwenhuis. Induction = I-Axiomatization + First-Order Consistency. Information and Computation, 159(1-2):151--186, May/June 2000.

....by induction and the class of formulas that can be proved by the unfold fold proof method. iv) The unfold fold proof method is related to methods for proof by consistency (also called inductionless induction method) of equational formulas by using term rewriting systems (see [14, 15, 19] and [7] for a brief survey) This relationship is based on the ability of the unfold fold proof method of proving inductive properties without using an explicit induction schema. However, the proofs by consistency are refutational proofs, they work by nding minimal counterexamples, and they require ....

H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + rst-order consistency. Information and Computation, 1999. to appear.

.... of constrained functional dependencies in polynomial time [45] Examples of constraint systems with the independence property are: universal closures of the definite Horn clauses of a logic programming language [43] term equations over finite or infinite trees [20] or in shallow theories [22], linear equations over the real numbers [42] various constraint classes over feature trees [8, 7, 56] infinite Boolean algebras with positive constraints [36] and various simple subclasses of constraints (e.g. inequations over numberswhere each variable always appears on the same side of the ....

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, cycle-syntacticness, and shallow theories. Information and Computation, 111:154--191, May 1994.

.... 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 ....

....by induction and the class of formulas that can be proved by the unfold fold proof method. v) The unfold fold proof method is related to methods for proof by consistency (also called inductionless induction method) of equational formulas by using term rewriting systems (see [86, 89, 109] and [37] for a brief survey) This relationship is based on the ability of the unfold fold proof method of proving inductive properties without using an explicit induction schema. However, the proofs by consistency are refutational proofs, they work by nding minimal counterexamples, and they require ....

H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + rst-order consistency. Information and Computation, 1999. to appear.

....recursivity. In [8] J. Christian defines a new criterion : every rewrite rule lhs is flat (f(s 1 ; s n ) is flat if 8i 2 [1; n] s i is either a variable or a ground data term) and the rewrite rules are oriented by a well founded ordering. H. Comon, M. Haberstrau and J. P. Jouannaud in [9] show that decidability also holds for shallow rewrite systems (the sides of rewrite rules have variables occurring at depth at most one) R. Nieuwenhuis in [26] extends the shallow theories to standard theories that allow non shallow variables. The restriction of D. Kapur and P. Narendran in ....

....grammar. Example 8.4 Let R = f 0 x x; x 0 x; s(x) s(y) s(s(x y) s(x) p(y) x y; p(x) s(y) x y; p(x) p(y) p(p(x y) g that defines the addition in positive and negative integers. This rewrite system does not satisfy the restrictions given in the previous work [19, 23, 9, 26, 21, 8, 20, 14] but satisfies ours. Therefore we are able to solve linear equations modulo this theory. Example 8.5 Let ( r 1 : f(c(x; x 0 ) c(y; y 0 ) c(f(x; y 0 ) f(x 0 ; y) r 2 : f(0; 0) 0 This system provides an idea of the expressiveness of TTSG s because when solving the equation f(x; ....

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, Cycle-Syntacticness and Shallow Theories. Information and Computation, 111(1):154--191, 1994.

.... 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 ....

....by induction and the class of formulas that can be proved by the unfold fold proof method. 17 (v) The unfold fold proof method is related to methods for proof by consistency (also called inductionless induction method) of equational formulas by using term rewriting systems (see [15, 16, 20] and [8] for a brief survey) This relationship is based on the ability of the unfold fold proof method of proving inductive properties without using an explicit induction schema. However, the proofs by consistency are refutational proofs, they work by nding minimal counterexamples, and they require ....

H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + rst-order consistency. Information and Computation, 1999. to appear.

....rewriting system, a rule being ultra shallow if variables occurs at depth one. This undecidability result is surprising in the light of the decidability result for the first order theory of the quotient algebra T Gamma = E when Gamma is a finite signature and E a finite set of shallow equations [10]. Hence, for any shallow rewriting system, the theory of the symmetric transitive closure of the one step rewriting relation is decidable. Decidability of the positive existential fragment has been shown in [22] for any rewrite system. In [6] it is proved that the existential fragment of ....

Comon, H., Haberstrau, M., and Jouannaud, J.-P. Syntacticness, cyclesyntacticness and shallow theories. Information and Computation 111, 1 (May 1994), 154--191.

.... of results on decidability of E unification for particular classes of trs s, such as Peano s axioms without multiplication which can be expressed in Pressburger arithmetic [Pre27] monoids [Mak77] particular, restricted, confluent string rewriting systems [OND95] shallow theories [CHJ94], that is, particular trs s, in the rules of which variables may only occur at depth at most one. particular, restricted convergent (that is, terminating and confluent) trs s, as considered in [Hul80, KN87, Mit94] The reference which is most relevant and also closest related to our results, is ....

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, cycle-- syntacticness, and shallow theories. Information and Computation, 111:154-- 191, 1994.

....class are the equational shallow theories, the ones axiomatized by equations where all variables are shallow , i.e. they appear only at depth at most one in each side of the equation. This is a fundamental class with decidable word and unification problems and even a decidable first order theory [Comon et al. 1994]. These results on shallow theories subsume much earlier ones on classes like ground, permutative, compact or quasi free theories. They were obtained, following [Kirchner, 1986] by transforming shallow presentations into equivalent (cycle )syntactic ones, for which complete and terminating ....

.... flat equations: at depth one there are only variables and constants: otherwise, replace non constant ground arguments t everywhere with a new constant a and add a new shallow equation a t (iterate this if the arguments of t are again non constant) This process generates a conservative extension [Comon et al. 1994]. It only adds a linear number of new constants and equations. Now close E under paramodulation wrt. an RPO compatible with arities. This means that constants are small in the precedence, and hence all non topmost inferences are replacements of constants by constants. The language of flat ....

[Article contains additional citation context not shown here]

Comon, H., Haberstrau, M., and Jouannaud, J.-P. (1994). Syntacticness, Cycle-Syntacticness and Shallow Theories. Information and Computation, 111(1):154--191.

....rewrite rules, that gives the remainder of x Xi y. When using the first clause, a disequation has to be solved modulo a theory. Few authors have studied equational disunification. Decidability results have been established for quasi free theories and compact theories [3] and for shallow theories [4]. Other work gives algorithms that enumerate the solutions, as in syntactic theories [2] or modulo theories presented by a convergent set of rewrite rules [6] These enumerations do not terminate in general, therefore these works give semi decision procedures of existence of solutions. In this ....

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, CycleSyntacticness and Shallow Theories. Information and Computation, 111(1):154-- 191, 1994.

....are the equational Shallow theories, the ones axiomatized by equations where all variables are shallow , i.e. they appear only at depth at most one in each side of the equation. This is a fundamental class with decidable word and unification problems (and even a decidable first order theory) [CHJ94], subsuming much previous work on classes like ground, permutative, compact or quasi free theories. The results on shallow theories were obtained, following [Kir86] by transforming shallow presentations into equivalent (cycle )syntactic ones, for which complete and terminating unification rules ....

.... equations: at depth one there are only variables and constants: otherwise, replace non constant ground arguments t everywhere with a new constant a and add a new shallow equation a t (iterate this if the arguments of t are again non constant) This process generates a conservative extension [CHJ94]. It only adds a linear number of new constants and equations. Now close E under paramodulation wrt. an RPO compatible with arities. This means that constants are small in the precedence, and hence all nontopmost inferences are replacements of constants by constants. The language of flat ....

[Article contains additional citation context not shown here]

Hubert Comon, Marianne Haberstrau, and Jean-Pierre Jouannaud. Syntacticness, Cycle-Syntacticness and Shallow Theories. Information and Computation, 111(1):154--191, 1994.

....in Pressburger arithmetic [Pre27] monoids [Mak77] or particular, restricted, confluent string rewriting systems [OND95] More closely related to the classes of TRSs that we consider here are the following theories: 1. Standard theories [Nie96] which are an extension of shallow theories [CHJ94]. A shallow theory is induced by a TRS that is R restricted in the following way: in the right hand sides of the rules of R, variables may occur only at depth at most 1. 2. Particular, restricted convergent (that is, terminating and confluent) TRSs, as considered in [Hul80, KN87, Mit94] 3. ....

....un decidability of E unification in Section 5 and Section 6, respectively. 4.1 Related Decidability Results 4.1.1 Standard and Shallow Theories Shallow variables are variables occurring in a term at depth at most 1. Shallow theories are induced by TRSs in which only shallow variables occur. In [CHJ94] it is shown that E unification is decidable in shallow theories. In [Nie96] an extension of this result is presented, namely, decidability of E unification for an even larger class is shown. In this class, nonshallow variables may occur in specific cases. However, there is still a restriction ....

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, cycle-syntacticness, and shallow theories.<F4.826e+05> Information and Computation,<F5.35e+05> 111:154--191, 1994.

....synchronized grammar. Example 5.7 Let R = f0 x x; x 0 x; s(x) s(y) s(s(x y) s(x) p(y) x y; p(x) s(y) x y; p(x) p(y) p(p(x y) g that defines the addition in positive and negative integers. This rewrite system does not satisfy the restrictions given in the previous works [7, 11, 2, 12, 9, 1, 8, 4] but satisfies ours. Therefore we are able to solve linear equations modulo this theory. Example 5.8 Let r 1 f(c(x; x 0 ) c(y; y 0 ) c(f(x; y 0 ) f(x 0 ; y) r 2 f(0; 0) 0 This system provides an idea of the expressiveness of TTSG s because when solving the equation f(x; y) z, ....

....recursivity. In [1] J. Christian defines a new criterion : every rewrite rule lhs is flat (f(s 1 ; s n ) is flat if 8i 2 [1; n] s i is either a variable or a ground data term) and the rewrite rules are oriented by a well founded ordering. H. Comon, M. Haberstrau and J. P. Jouannaud in [2] show that decidability also holds for shallow rewrite systems (the sides of rewrite rules have variables occurring at depth at most one) R. Nieuwenhuis in [12] extends the shallow theories to standard theories that allow non shallow variables. The restriction of D. Kapur and P. Narendran in [9] ....

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, Cycle-Syntacticness and Shallow Theories. Information and Computation, 111(1):154--191, 1994.

....recursivity. In [1] J. Christian defines a new criterion : every rewrite rule lhs is flat (f(s 1 ; s n ) is flat if 8i 2 [1; n] s i is either a variable or a ground data term) and the rewrite rules are oriented by a well founded ordering. H. Comon, M. Haberstrau and J. P. Jouannaud in [2] show that decidability also holds for shallow rewrite systems (the sides of rewrite rules have variables occurring at depth at most one) R. Nieuwenhuis in [12] extends the shallow theories to standard theories that allow non shallow variables. The restriction of D. Kapur and P. Narendran in [9] ....

....grammar. Example 5.13 Let R = f0 x x; x 0 x; s(x) s(y) s(s(x y) s(x) p(y) x y; p(x) s(y) x y; p(x) p(y) p(p(x y) g that defines the addition in positive and negative integers. This rewrite system does not satisfy the restrictions given in the previous work [7, 11, 2, 12, 9, 1] but satisfies ours. Therefore we are able to solve linear equations modulo this theory. 6 Conclusion We have presented an original approach using Tree Tuple Synchronized Grammars (TTSG) to solve linear equations modulo theories given as rewrite systems satisfying some restrictions. This ....

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, Cycle-Syntacticness and Shallow Theories. Information and Computation, 111(1):154--191, 1994.

.... results that have been applied to state of the art theorem provers like Spass [Wei97] and Vampire [RV01] These techniques have also led to results on logic based complexity and decidability analysis [BG01,Nie98] on deduction with constrained clauses [KKR90,NR95] on inductive theorem proving [CN00], and on many other applications like symbolic constraint solving, or equational logic programming. In the handbook chapter [NR01] the fundamental techniques in this area are reviewed and presented in a uniform framework. However, in the last two years several interesting developments have taken ....

.... problems (winning in the corresponding category of several CADE ATP System Competitions) There is also a very close relationship between the finite computation of saturated sets and implicit inductive theorem proving, that is, where the user does not need to provide explicit induction schemes [CN00]. 2 Although for some E extended inference rules are needed (see, e.g. RV95] 4 3 Paramodulation with weak orderings Up to recently, all major known completeness results for Knuth Bendix completion and ordered paramodulation require the term ordering to be wellfounded, monotonic and total ....

H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + first-order consistency. Information and Computation, 2000. To appear.

....literature: even in very restricted and simple situations the problem remains undecidable. To our knowledge, the only decidability results are for complete theories, i.e. where (for infinite I) the inductive theory coincides with the equational theory, like the shallow equational theories of [CHJ94] or the Catalog Horn theories of [Nie96] However, under reasonable assumptions it is possible to obtain what we will call refutation complete procedures for inductive validity: procedures that provide in finite time a disproof for any conjecture that is false (in M) Then the situation is ....

....To our knowledge, the only (syntactically defined) classes of axiomatizations E with a decidable inductive validity problem are the w complete ones, i.e. for infinite I) the inductive theory coincides with the equational theory. This is the case for classes like the shallow equations of [CHJ94] or the Catalog Horn axiomatizations of [Nie96] It seems to be folk knowledge that it is difficult to go beyond. In this section we very briefly give some insight for the reason why: even for (syntactically) very restricted and simple E the problem remains undecidable. We slightly adapt two ....

Hubert Comon, Marianne Haberstrau, and Jean-Pierre Jouannaud. Syntacticness, Cycle-Syntacticness and Shallow Theories. Information and Computation, 111(1):154--191, 1994.

....even in very restricted and simple situations the problem remains undecidable. To our knowledge, the only decidability results are for complete theories, i.e. where (for infinite models) the inductive theory coincides with the equational theory, like the shallow equational theories of [CHJ94] or the Catalog Horn theories of [Nie96] However, under reasonable assumptions it is possible to obtain what we will call refutation complete procedures for inductive validity: procedures that provide in finite time a disproof for any conjecture that is false in M. Then the situation is exactly ....

....To our knowledge, the only (syntactically defined) classes of axiomatizations E with a decidable inductive validity problem are the w complete ones, i.e. for infinite I) where the inductive theory coincides with the equational theory. This is the case for classes like the shallow equations of [CHJ94] or the Catalog Horn axiomatizations of [Nie96] which are both based on presentations where variables do not occur at depth more than one. It seems to be folk knowledge that it is difficult to go beyond. In this section we very briefly give some insight for the reason why: even for ....

Hubert Comon, Marianne Haberstrau, and Jean-Pierre Jouannaud. Syntacticness, Cycle-Syntacticness and Shallow Theories. Information and Computation, 111(1):154--191, 1994.

....involving arithmetic is not computable. The third part is devoted to linear shallow theories. This includes such theories as commutativity or unity, but not associativity or idempotency. Shallow theories were investigated by H. Comon, M. Haberstrau and J. P. Jouannaud in their papers [14] and [15]. We show that the problem of consistency of systems of set constraints in such theories can be reduced to satisfiability of almost flat formulae and then solved using methods introduced in [11] Following the ideas of [31] we were able to use this result to prove that semantic order sorted ....

....apply techniques from [11] and obtain the decidability result for mixed set constraints. We apply this result to prove decidability of (elementary) order sorted unification in such theories. Shallow theories were investigated by H. Comon, M. Haberstrau and J. P. Jouannaud in their papers [14] and [15]. This is probably the largest class of equational theories for which all interesting problems (like word problem, unification and disunification, quantifier elimination) are decidable, and one of very few classes of theories that enjoy a uniform unification or disunification procedure. 3.1 Basic ....

[Article contains additional citation context not shown here]

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, cycle-syntacticness, and shallow theories. Information and Computation, 111:154--191, May 1994.

No context found.

H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, cycle-syntacticness, and shallow theories. Information and Computation, 111(1):154--191, 1994.

No context found.

Comon, H. 2000. Sequentiality, second order monadic logic, and tree automata. Information and Computation 157, 25--51.

No context found.

H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + first-order consistency. Information and Computation, 159(1/2):151-186, 2000.

No context found.

H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + first-order consistency. Information and Computation, 159(1/2):151-186, 2000.

First 50 documents

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.