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