Cited in
(90)- Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
- AC completion with termination tools
- On the recursive decomposition ordering with lexicographical status and other related orderings
- A rewriting strategy to verify observational congruence
- Categorical ML -- category-theoretic modular programming
- Total termination of term rewriting
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Rewriting with a nondeterministic choice operator
- A decidable word problem without equivalent canonical term rewriting system
- Chain properties of rule closures
- A fully syntactic AC-RPO.
- Completion for rewriting modulo a congruence
- Invariants, patterns and weights for ordering terms
- Automatic Termination
- Term rewriting and beyond -- theorem proving in Isabelle
- Grez
- Conditional narrowing modulo a set of equations
- Schematization of infinite sets of rewrite rules generated by divergent completion processes
- On recursive path ordering
- Refutational theorem proving using term-rewriting systems
- A path ordering for proving termination of AC rewrite systems
- Buchberger's algorithm: The term rewriter's point of view
- On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
- Proving termination by dependency pairs and inductive theorem proving
- Polynomials over the reals in proofs of termination : from theory to practice
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- A complete superposition calculus for primal grammars
- Size-based termination of higher-order rewriting
- Mechanically proving termination using polynomial interpretations
- Proving termination of (conditional) rewrite systems. A semantic approach
- Unification in combinations of collapse-free regular theories
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Termination of rewriting
- Combining matching algorithms: The regular case
- AC-KBO revisited
- Termination orderings for associative-commutative rewriting systems
- LARCH
- SPIKE
- AProVE
- Tyrolean
- CiME
- CARIBOO
- mkbTT
- MU-TERM
- Slothrop
- SbReve2
- TORPA
- Tsukuba
- ORME
- KBCV
- A3PAT
- Nagoya Termination Tool
- TCAS
- term-rewriting
- AFFIRM
- RRL
- Polynomials
- Termination of term rewriting using dependency pairs
- CatLib
- Termination and completion modulo associativity, commutativity and identity
- Generating polynomial orderings
- scientific article; zbMATH DE number 3870584 (Why is no real title available?)
- Automating the Knuth Bendix ordering
- Termination by completion
- Contextual rewriting as a sound and complete proof method for conditional LOG-specifications
- Well rewrite orderings and well quasi-orderings
- A finite Thue system with decidable word problem and without equivalent finite canonical system
- Boolean unification - the story so far
- Equational completion in order-sorted algebras
- Multi-completion with termination tools
- scientific article; zbMATH DE number 3870642 (Why is no real title available?)
- NARROWER
- Termination Modulo Combinations of Equational Theories
- Automated deduction with associative-commutative operators
- Outermost ground termination
- History and basic features of the critical-pair/completion procedure
- Proof of termination of the rewriting system SUBSET on CCL
- 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
- scientific article; zbMATH DE number 3921947 (Why is no real title available?)
- NaTT
- Modular and incremental proofs of AC-termination
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Mechanically certifying formula-based Noetherian induction reasoning
- scientific article; zbMATH DE number 3926235 (Why is no real title available?)
- scientific article; zbMATH DE number 4047067 (Why is no real title available?)
- Termination of rewrite systems by elementary interpretations
- Termination of string rewriting proved automatically
- A total AC-compatible ordering based on RPO
- Natural termination
- Automatic proofs of termination with elementary interpretations
This page was built for software: REVE
