Miki Hermann  @ NUS Home/Search
Context Related
| loria.fr/~hermann/pub...vademecum.ps.gz Cached: PS.gz PS PDF Image Update Help From: loria.fr/~hermann/publications (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: This paper presents two structural patterns to detect divergence of the completion procedure, followed by a detailed overview of dioeerent examples of divergent rewrite systems. Further it introduces five different empirical methods to avoid divergence, applicable during a session with a rewrite rule laboratory. (Update)
Context of citations to this paper: More
.... in an incremental fashion, since in this way divergence of completion, i.e. non termination of completion, may sometimes be avoided too [He88]. It will turn out that a lot of problems may arise, if it is allowed to change the ordering during completion, as mentioned above, even...
.... with the user, the completion process usually diverges, but based on the intended semantics, there are ways to avoid such a divergence (see [Her88]) Let us give some principles used in the case of calculus. ffl Generalize any rule of the form a[s] a[t] or (s) t) to...
Cited by: More
Unification of Terms With Exponents - Socher-Ambrosius (1993) (Correct)
On the Relation Between Primitive Recursion, Schematization, and.. - Hermann (Correct)
From λσ to λν - a Journey through Calculi .. - Lescanne (1994) (Correct)
Active bibliography (related documents): More All
1.4: Chain Properties of Rule Closures - Hermann (1990) (Correct)
1.2: Rewrite Systems - Dershowitz, Jouannaud (1990) (Correct)
0.6: Generating Polynomial Orderings for Termination Proofs - Giesl (1995) (Correct)
Similar documents based on text: More All
0.6: A decision procedure for the existential theory of term.. - Korovin, Voronkov (2000) (Correct)
0.2: On Proving Properties of Completion Strategies - Hermann (1990) (Correct)
0.1: The Complexity of Counting Problems in Equational Matching - Hermann, Kolaitis (1995) (Correct)
Related documents from co-citation: More All
2: Simple Word Problems in Universal Algebra (context) - Knuth, Bendix - 1970
BibTeX entry: (Update)
M. Hermann. Vademecum of divergent term rewriting systems. CRIN Report 88-R-082 (Centre de Recherche en Informatique de Nancy, 1988). http://citeseer.comp.nus.edu.sg/117618.html More
@misc{ hermann88vademecum,
author = "M. Hermann",
title = "Vademecum of divergent term rewriting systems",
text = "M. Hermann. Vademecum of divergent term rewriting systems. CRIN Report
88-R-082 (Centre de Recherche en Informatique de Nancy, 1988).",
year = "1988",
url = "citeseer.comp.nus.edu.sg/117618.html" }
Citations (may not include all citations):384 Simple word problems in universal algebras (context) - Knuth, Bendix - 1970
72 Completion without failure - Bachmair, Dershowitz et al. - 1989
68 Proofs by induction in equational theories with constructors (context) - Huet, Hullot - 1982
65 Automated theorem-proving for theories with simpliøers (context) - Slagle - 1974
65 the uniform halting problem for term rewriting systems (context) - Huet, Lankford - 1978
55 Completion of a set of rules modulo a set of equations (context) - Jouannaud, Kirchner - 1986
54 Tree-manipulating systems and Church-Rosser theorems (context) - Rosen - 1973
52 On word problems in equational theories (context) - Hsiang, Rusinowitch - 1987
51 Proof by consistency in equational theories (context) - Bachmair - 1988
49 Orderings for equational proofs (context) - Bachmair, Dershowitz et al. - 1986
45 Proof by consistency (context) - Kapur, Musser - 1987
40 A strong restriction of the inductive completion procedure (context) - Fribourg - 1989
34 Automatic proofs by induction in theories without constructo.. (context) - Jouannaud, Kounalis - 1989
33 Completion for rewriting modulo a congruence (context) - Bachmair, Dershowitz - 1989
22 Completion and its applications (context) - Dershowitz - 1989
19 Computer experiments with the Reve term rewriting system gen.. (context) - Lescanne - 1983
19 transformation and termination (context) - Bachmair, Dershowitz - 1986
19 the recursive decomposition ordering with lexicographical st.. (context) - Lescanne - 1990
16 Termination of rewriting systems by polynomial interpretatio.. (context) - BenCherifa, Lescanne - 1987
12 How to choose the weights in the Knuth-Bendix ordering (context) - Martin - 1987
12 On proving uniform termination and restricted termination of.. (context) - Guttag, Kapur et al. - 1983
9 and construction of rewrite systems (context) - Dershowitz, Marcus et al. - 1988
9 Transformation ordering (context) - Bellegarde, Lescanne - 1987
8 Bulletin of the European Association for Theoretical Compute.. (context) - Dershowitz, Jouannaud et al. - 1991
8 Completion procedures as transition rules + control (context) - Lescanne - 1989
7 Proving inductive theorems based on term rewriting systems (context) - Hofbauer, Kutsche - 1988
6 Special issue on Rewriting Techniques and Applications (context) - Dershowitz, rewriting et al. - 1987
6 On suOEcient completeness and related properties of term rew.. (context) - Kapur, Narendran et al. - 1987
5 Canonical forms and uniøcation (context) - Hullot - 1980
4 Path of subterms ordering and recursive decomposition orderi.. (context) - Rusinowitch - 1987
4 Chain properties of rule closures - Hermann - 1989
3 First-order uniøcation in an equational theory (context) - Fay - 1979
3 ConAEuent reductions: Abstract properties and applications t.. (context) - Huet - 1980
3 Centre de Recherche en Informatique de Nancy (context) - Hermann, rewriting et al. - 1989
3 Department of Mathematics and Computer Science (context) - Lankford, Research - 1975
3 Information Sciences Institute (context) - Lankford, Musser et al. - 1978
2 nite sets of rewrite rules generated by divergent completion.. (context) - Kirchner, ino - 1989
2 On nontermination of Knuth-Bendix algorithm (context) - Hermann, Pr - 1986
2 Data abstraction transformations (context) - Ardis - 1980
2 Rewriting systems on FP expressions to reduce the number of .. (context) - Bellegarde - 1986
2 Divergence of the Knuth-Bendix completion procedure and term.. (context) - Lescanne - 1986
1 Technical Report ATR (context) - Dershowitz, Marcus et al. - 1982
1 therian and conAEuent rewrite system for idempotent semigrou.. (context) - Siekmann, Szab - 1982
1 Divergence in the completion of rewriting systems (context) - Mong, Purdom - 1987
1 Detecting looping simpliøcations (context) - Purdom - 1987
1 Institute of SocioEconomic Information and Automation in Man.. (context) - Hermann, Pr et al. - 1985
1 Ground conAEuence (context) - bel - 1987
1 quations dans les alg#bres libres et les vari #t#s #quatione.. (context) - Kirchner, Kirchner et al. - 1982
Documents on the same site (http://www.loria.fr/~hermann/publications.html): More
On the Word, Subsumption, and Complement Problem for.. - Hermann, Salzer (Correct)
Unification Algorithms Cannot be Combined in Polynomial Time - Hermann, Kolaitis (1996) (Correct)
On the Complexity of Counting the Hilbert Basis of a.. - Hermann, Juban, Kolaitis (1999) (Correct)
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.