Towards a foundation of completion procedures as semidecision procedures
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 4016226 (Why is no real title available?)
- scientific article; zbMATH DE number 4191131 (Why is no real title available?)
- scientific article; zbMATH DE number 3871322 (Why is no real title available?)
- scientific article; zbMATH DE number 3829296 (Why is no real title available?)
- scientific article; zbMATH DE number 4047063 (Why is no real title available?)
- scientific article; zbMATH DE number 4049135 (Why is no real title available?)
- scientific article; zbMATH DE number 4053061 (Why is no real title available?)
- scientific article; zbMATH DE number 3684925 (Why is no real title available?)
- scientific article; zbMATH DE number 8327 (Why is no real title available?)
- scientific article; zbMATH DE number 176740 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- A Unification Algorithm for Associative-Commutative Functions
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A maximal-literal unit strategy for horn clauses
- A strong restriction of the inductive completion procedure
- Automated proofs of the Moufang identities in alternative rings
- Automatic proofs by induction in theories without constructors
- Complete Sets of Reductions for Some Equational Theories
- Completion for rewriting modulo a congruence
- Completion of a Set of Rules Modulo a Set of Equations
- Completion of first-order clauses with equality by strict superposition
- Computing with rewrite systems
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Critical pair criteria for completion
- Equational inference, canonical proofs, and proof orderings
- How to avoid the derivation of redundant clauses in reasoning systems
- On restrictions of ordered paramodulation with simplification
- On rewrite programs: Semantics and relationship with prolog
- On word problems in Horn theories
- Orderings for term-rewriting systems
- Proof by consistency
- Proofs by induction in equational theories with constructors
- Proving refutational completeness of theorem-proving strategies
- Proving termination with multiset orderings
- Refutational theorem proving using term-rewriting systems
- Resolution of equations in algebraic structures. Volume II: Rewriting techniques
- Rewrite method for theorem proving in first order theory with equality
- Semantic confluence tests and completion methods
- Termination of rewriting
- Theorem-proving with resolution and superposition
Cited in
(18)- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Canonical Inference for Implicational Systems
- On deciding satisfiability by theorem proving with speculative inferences
- Completion-time optimization of rewrite-time goal solving
- Structures for abstract rewriting
- Semi-initial completions
- On First-Order Model-Based Reasoning
- Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01).
- Canonicity!
- Abstract canonical presentations
- Canonical ground Horn theories
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Completion procedures as semidecision procedures
- A rewriting approach to satisfiability procedures.
- On using ground joinable equations in equational theorem proving
- Goal-directed completion using SOUR graphs
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)
