Pages that link to "Item:Q1154801"
From MaRDI portal
The following pages link to A complete proof of correctness of the Knuth-Bendix completion algorithm (Q1154801):
Displayed 50 items.
- Effective codescent morphisms in the varieties determined by convergent term rewriting systems. (Q278228) (← links)
- Strong normalisation in the \(\pi\)-calculus (Q598201) (← links)
- Towards a foundation of completion procedures as semidecision procedures (Q673134) (← links)
- Theorem-proving with resolution and superposition (Q757094) (← links)
- A completion procedure for conditional equations (Q758211) (← links)
- Automating inductionless induction using test sets (Q758216) (← links)
- Refutational theorem proving using term-rewriting systems (Q802317) (← links)
- Equational completion in order-sorted algebras (Q912606) (← links)
- Chain properties of rule closures (Q916402) (← links)
- A superposition oriented theorem prover (Q1060857) (← links)
- Equational methods in first order predicate calculus (Q1065783) (← links)
- On merging software extensions (Q1082067) (← links)
- On solving the equality problem in theories defined by Horn clauses (Q1085152) (← links)
- Rewrite method for theorem proving in first order theory with equality (Q1098649) (← links)
- Analysis of Dehn's algorithm by critical pairs (Q1100558) (← links)
- History and basic features of the critical-pair/completion procedure (Q1103414) (← links)
- Critical pair criteria for completion (Q1106659) (← links)
- Completion for unification (Q1178701) (← links)
- Fuzzy term-rewriting system (Q1182011) (← links)
- Schematization of infinite sets of rewrite rules generated by divergent completion processes (Q1262755) (← links)
- Buchberger's algorithm: The term rewriter's point of view (Q1350495) (← links)
- A rewriting approach to satisfiability procedures. (Q1401930) (← links)
- Partial completion of equational theories (Q1592635) (← links)
- A strong restriction of the inductive completion procedure (Q1824381) (← links)
- Automatic proofs by induction in theories without constructors (Q1824382) (← links)
- About the rewriting systems produced by the Knuth-Bendix completion algorithm (Q1836978) (← links)
- Larry Wos: visions of automated reasoning (Q2102922) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Essential unifiers (Q2494722) (← links)
- Abstract canonical presentations (Q2500482) (← links)
- (Q2980972) (← links)
- Unnecessary inferences in associative-commutative completion procedures (Q3489486) (← links)
- Canonicity! (Q3541714) (← links)
- Rewriting Systems and Embedding of Monoids in Groups (Q3617419) (← links)
- (Q3667939) (← links)
- (Q3700828) (← links)
- Canonical Ground Horn Theories (Q4916071) (← links)
- (Q5013816) (← links)
- On how to move mountains ‘associatively and commutatively’ (Q5055722) (← links)
- On fairness of completion-based theorem proving strategies (Q5055773) (← links)
- On proving properties of completion strategies (Q5055777) (← links)
- Open problems in rewriting (Q5055780) (← links)
- Completion for multiple reduction orderings (Q5055819) (← links)
- Problems in rewriting III (Q5055847) (← links)
- Chain properties of rule closures (Q5096168) (← links)
- A categorical formulation for critical-pair/completion procedures (Q5881196) (← links)
- Meta-rule synthesis from crossed rewrite systems (Q5881274) (← links)
- Completion procedures as semidecision procedures (Q5881279) (← links)
- Linear completion (Q5881280) (← links)
- On interreduction of semi-complete term rewriting systems (Q5941203) (← links)