Towards a foundation of completion procedures as semidecision procedures
From MaRDI portal
Publication:673134
DOI10.1016/0304-3975(94)00187-NzbMath0873.68107OpenAlexW2044301710MaRDI QIDQ673134
Maria Paola Bonacina, Jieh Hsiang
Publication date: 28 February 1997
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(94)00187-n
Related Items
Structures for abstract rewriting, On First-Order Model-Based Reasoning, A rewriting approach to satisfiability procedures., On using ground joinable equations in equational theorem proving, On deciding satisfiability by theorem proving with speculative inferences, Canonicity!, Canonical Inference for Implicational Systems, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, Canonical Ground Horn Theories, Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01)., Abstract canonical presentations, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- How to avoid the derivation of redundant clauses in reasoning systems
- Theorem-proving with resolution and superposition
- On word problems in Horn theories
- Proofs by induction in equational theories with constructors
- Refutational theorem proving using term-rewriting systems
- Automated proofs of the Moufang identities in alternative rings
- Proof by consistency
- Termination of rewriting
- Rewrite method for theorem proving in first order theory with equality
- Critical pair criteria for completion
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Completion for rewriting modulo a congruence
- A strong restriction of the inductive completion procedure
- Automatic proofs by induction in theories without constructors
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Computing with rewrite systems
- Semantic confluence tests and completion methods
- Completion of a Set of Rules Modulo a Set of Equations
- Proving termination with multiset orderings
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- A Unification Algorithm for Associative-Commutative Functions
- Complete Sets of Reductions for Some Equational Theories
- On rewrite programs: Semantics and relationship with prolog
- Equational inference, canonical proofs, and proof orderings
- Proving refutational completeness of theorem-proving strategies
- A maximal-literal unit strategy for horn clauses
- Completion of first-order clauses with equality by strict superposition
