The following pages link to REVE (Q40621):
Displaying 50 items.
- Multi-completion with termination tools (Q352956) (← links)
- Proving termination by dependency pairs and inductive theorem proving (Q438537) (← links)
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- Natural termination (Q673622) (← links)
- A total AC-compatible ordering based on RPO (Q673623) (← links)
- Categorical ML -- category-theoretic modular programming (Q684395) (← links)
- Automating the Knuth Bendix ordering (Q751830) (← links)
- Termination by completion (Q757069) (← links)
- Refutational theorem proving using term-rewriting systems (Q802317) (← links)
- Termination of string rewriting proved automatically (Q850497) (← links)
- Mechanically proving termination using polynomial interpretations (Q851142) (← links)
- Term rewriting and beyond -- theorem proving in Isabelle (Q909488) (← links)
- Equational completion in order-sorted algebras (Q912606) (← links)
- On the recursive decomposition ordering with lexicographical status and other related orderings (Q912609) (← links)
- A rewriting strategy to verify observational congruence (Q915472) (← links)
- Chain properties of rule closures (Q916402) (← links)
- Termination orderings for associative-commutative rewriting systems (Q1072371) (← links)
- A finite Thue system with decidable word problem and without equivalent finite canonical system (Q1073016) (← links)
- On recursive path ordering (Q1082075) (← links)
- Rewriting with a nondeterministic choice operator (Q1096383) (← links)
- Termination of rewriting (Q1098624) (← links)
- Unification in combinations of collapse-free regular theories (Q1099652) (← links)
- Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study (Q1100879) (← links)
- Simplifying conditional term rewriting systems: Unification, termination and confluence (Q1100891) (← links)
- History and basic features of the critical-pair/completion procedure (Q1103414) (← links)
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure (Q1106657) (← links)
- Combining matching algorithms: The regular case (Q1186723) (← links)
- Termination and completion modulo associativity, commutativity and identity (Q1199927) (← links)
- Well rewrite orderings and well quasi-orderings (Q1209622) (← links)
- Conditional narrowing modulo a set of equations (Q1261194) (← links)
- Completion for rewriting modulo a congruence (Q1262752) (← links)
- Schematization of infinite sets of rewrite rules generated by divergent completion processes (Q1262755) (← links)
- Generating polynomial orderings (Q1318775) (← links)
- Contextual rewriting as a sound and complete proof method for conditional LOG-specifications (Q1323311) (← links)
- Proving termination of (conditional) rewrite systems. A semantic approach (Q1323317) (← links)
- Automated deduction with associative-commutative operators (Q1340508) (← links)
- Buchberger's algorithm: The term rewriter's point of view (Q1350495) (← links)
- A fully syntactic AC-RPO. (Q1400715) (← links)
- Invariants, patterns and weights for ordering terms (Q1581131) (← links)
- Termination of rewrite systems by elementary interpretations (Q1805401) (← links)
- Proof of termination of the rewriting system SUBSET on CCL (Q1822494) (← links)
- Boolean unification - the story so far (Q1824411) (← links)
- Cancellative Abelian monoids and related structures in refutational theorem proving. I (Q1864898) (← links)
- A path ordering for proving termination of AC rewrite systems (Q1891259) (← links)
- Total termination of term rewriting (Q1912706) (← links)
- Termination of term rewriting using dependency pairs (Q1978641) (← links)
- A complete superposition calculus for primal grammars (Q2352496) (← links)
- SAT solving for termination proofs with recursive path orders and dependency pairs (Q2392415) (← links)
- On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting (Q2502172) (← links)
- Modular and incremental proofs of AC-termination (Q2643544) (← links)
