Termination of rewriting systems by polynomial interpretations and its implementation

DOI10.1016/0167-6423(87)90030-XzbMath0625.68036MaRDI QIDQ579930

Ahlem Ben Cherifa, Pierre Lescanne

Publication date: 1987

Published in: Science of Computer Programming (Search for Journal in Brave)

zbMATH Keywords

inequalities between polynomialsrewrite rule laboratory REVEtermination of rewriting systems

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Theory of software (68N99) Theory of computing (68Q99)

Related Items

Termination of term rewriting by interpretation, Path orderings for termination of associative-commutative rewriting, Automated deduction with associative-commutative operators, A path ordering for proving termination of AC rewrite systems, Weights for total division orderings on strings, Termination proofs and the length of derivations, Incremental termination proofs and the length of derivations, Open problems in rewriting, Topics in termination, A precedence-based total AC-compatible ordering, Extension of the associative path ordering to a chain of associative commutative symbols, Linear interpretations by counting patterns, More problems in rewriting, Generating polynomial orderings for termination proofs, Termination of constructor systems, Termination of string rewriting proved automatically, Mechanically proving termination using polynomial interpretations, Modular and incremental proofs of AC-termination, Polynomials over the reals in proofs of termination : from theory to practice, SAT solving for termination proofs with recursive path orders and dependency pairs, Total termination of term rewriting, Size-based termination of higher-order rewriting, AC-Termination of rewrite systems: A modified Knuth-Bendix ordering, AC-KBO revisited, Analyzing Innermost Runtime Complexity Through Tuple Interpretations, A fully syntactic AC-RPO., Proving termination by dependency pairs and inductive theorem proving, Chain properties of rule closures, The order types of termination orderings on monadic terms, strings and multisets, Termination of term rewriting using dependency pairs, Natural termination, A total AC-compatible ordering based on RPO, Automatic Proofs of Termination With Elementary Interpretations, Unnamed Item, On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting, Any ground associative-commutative theory has a finite canonical system, Preuves de terminaison de systèmes de réécriture fondées sur les interprétations polynomiales. Une méthode basée sur le théorème de Sturm, AC Completion with Termination Tools, Total termination of term rewriting, Termination of rewrite systems by elementary interpretations, Conditional narrowing modulo a set of equations, Completion for rewriting modulo a congruence, Schematization of infinite sets of rewrite rules generated by divergent completion processes, Automating the Knuth Bendix ordering, Automatic Termination, Termination by completion, REVE, Termination Modulo Combinations of Equational Theories, Invariants, patterns and weights for ordering terms, Cancellative Abelian monoids and related structures in refutational theorem proving. I, Generating polynomial orderings, A complete superposition calculus for primal grammars, Proving termination of (conditional) rewrite systems. A semantic approach