scientific article

zbMath0642.68036MaRDI QIDQ3783521

Leo Bachmair, Nachum Dershowitz

Publication date: 1986

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

transformationterminationcommutationassociative-commutative rewrite systems

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items (36)

Implementing term rewriting by graph reduction: Termination of combined systems ⋮ Some results on the confluence property of combined term rewriting systems ⋮ Strategies for combining decision procedures ⋮ A path ordering for proving termination of AC rewrite systems ⋮ Incremental termination proofs and the length of derivations ⋮ Extension of the associative path ordering to a chain of associative commutative symbols ⋮ Automatic termination proofs with transformation orderings ⋮ A complete characterization of termination of 0p 1q→1r 0s ⋮ Termination of constructor systems ⋮ Algebraic simulations ⋮ Modular proofs for completeness of hierarchical term rewriting systems ⋮ Termination of rewriting ⋮ Counterexamples to termination for the direct sum of term rewriting systems ⋮ Tyrolean termination tool: techniques and features ⋮ On modularity in term rewriting and narrowing ⋮ Buchberger's algorithm: A constraint-based completion procedure ⋮ Finding small counterexamples for abstract rewriting properties ⋮ Modularity in term rewriting revisited ⋮ Jumping and escaping: modular termination and the abstract path ordering ⋮ A calculational approach to mathematical induction ⋮ Termination modulo equations by abstract commutation with an application to iteration ⋮ Modular Termination of Basic Narrowing ⋮ Termination of term rewriting using dependency pairs ⋮ Modular termination of \(r\)-consistent and left-linear term rewriting systems ⋮ Modal Tools for Separation and Refinement ⋮ Transforming termination by self-labelling ⋮ Associative-commutative reduction orderings ⋮ Modularity of simple termination of term rewriting systems with shared constructors ⋮ Remarks on Isomorphisms of Simple Inductive Types ⋮ On finite complete rewriting systems, finite derivation type, and automaticity for homogeneous monoids ⋮ Any ground associative-commutative theory has a finite canonical system ⋮ Unnamed Item ⋮ Termination by completion ⋮ Termination orderings for associative-commutative rewriting systems ⋮ Proving termination of (conditional) rewrite systems. A semantic approach ⋮ Abstract abstract reduction

This page was built for publication: