swMATH28907MaRDI QIDQ40621FDOQ40621
Author name not available (Why is that?)
Official website: https://dl.acm.org/citation.cfm?id=567078
Cited In (89)
- Total termination of term rewriting
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- A fully syntactic AC-RPO.
- Automatic Termination
- Invariants, patterns and weights for ordering terms
- A path ordering for proving termination of AC rewrite systems
- CatLib
- NaTT
- 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
- A complete superposition calculus for primal grammars
- Size-based termination of higher-order rewriting
- SAT solving for termination proofs with recursive path orders and dependency pairs
- AC-KBO revisited
- Generating polynomial orderings
- Contextual rewriting as a sound and complete proof method for conditional LOG-specifications
- Automated deduction with associative-commutative operators
- Grez
- Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
- 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
- A decidable word problem without equivalent canonical term rewriting system
- Rewriting with a nondeterministic choice operator
- Chain properties of rule closures
- Completion for rewriting modulo a congruence
- Term rewriting and beyond -- theorem proving in Isabelle
- 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
- Polynomials over the reals in proofs of termination : from theory to practice
- Proving termination by dependency pairs and inductive theorem proving
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Mechanically proving termination using polynomial interpretations
- Proving termination of (conditional) rewrite systems. A semantic approach
- Unification in combinations of collapse-free regular theories
- Termination of rewriting
- Combining matching algorithms: The regular case
- Termination orderings for associative-commutative rewriting systems
- Termination of term rewriting using dependency pairs
- Termination and completion modulo associativity, commutativity and identity
- Title not available (Why is that?)
- SPIKE
- AProVE
- Tyrolean
- CiME
- CARIBOO
- mkbTT
- MU-TERM
- Slothrop
- SbReve2
- TORPA
- Tsukuba
- ORME
- Automating the Knuth Bendix ordering
- Termination by completion
- KBCV
- A3PAT
- Nagoya Termination Tool
- TCAS
- term-rewriting
- AFFIRM
- RRL
- Polynomials
- 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
- NARROWER
- Title not available (Why is that?)
- Termination Modulo Combinations of Equational Theories
- Equational completion in order-sorted algebras
- Multi-completion with termination tools
- 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
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Termination of rewrite systems by elementary interpretations
- Automatic proofs of termination with elementary interpretations
- Termination of string rewriting proved automatically
- A total AC-compatible ordering based on RPO
- Natural termination
- AC completion with termination tools
This page was built for software: REVE
