Towards a foundation of completion procedures as semidecision procedures
From MaRDI portal
Publication:673134
DOI10.1016/0304-3975(94)00187-NzbMATH Open0873.68107OpenAlexW2044301710MaRDI QIDQ673134FDOQ673134
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
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proving termination with multiset orderings
- Orderings for term-rewriting systems
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Termination of rewriting
- A Unification Algorithm for Associative-Commutative Functions
- Complete Sets of Reductions for Some Equational Theories
- Proving refutational completeness of theorem-proving strategies
- Automated proofs of the Moufang identities in alternative rings
- Critical pair criteria for completion
- Equational inference, canonical proofs, and proof orderings
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Proofs by induction in equational theories with constructors
- Refutational theorem proving using term-rewriting systems
- Proof by consistency
- Theorem-proving with resolution and superposition
- On word problems in Horn theories
- Rewrite method for theorem proving in first order theory with equality
- Completion of a Set of Rules Modulo a Set of Equations
- A maximal-literal unit strategy for horn clauses
- Automatic proofs by induction in theories without constructors
- Semantic confluence tests and completion methods
- A strong restriction of the inductive completion procedure
- Completion for rewriting modulo a congruence
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Computing with rewrite systems
- On rewrite programs: Semantics and relationship with prolog
- Completion of first-order clauses with equality by strict superposition
- On restrictions of ordered paramodulation with simplification
- How to avoid the derivation of redundant clauses in reasoning systems
Cited In (15)
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Semi-initial completions
- On using ground joinable equations in equational theorem proving
- On deciding satisfiability by theorem proving with speculative inferences
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Structures for abstract rewriting
- A rewriting approach to satisfiability procedures.
- On First-Order Model-Based Reasoning
- Canonical Inference for Implicational Systems
- Canonical Ground Horn Theories
- Canonicity!
- Abstract canonical presentations
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01).
Uses Software
This page was built for publication: Towards a foundation of completion procedures as semidecision procedures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q673134)
