Theorem-proving with resolution and superposition
From MaRDI portal
Publication:757094
DOI10.1016/S0747-7171(08)80131-9zbMath0723.68094MaRDI QIDQ757094
Publication date: 1991
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (19)
On subsumption in distributed derivations ⋮ Reasoning with conditional axioms ⋮ On First-Order Model-Based Reasoning ⋮ A rewriting approach to satisfiability procedures. ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01). ⋮ Abstract canonical presentations ⋮ Associative-commutative deduction with constraints ⋮ Using forcing to prove completeness of resolution and paramodulation ⋮ On word problems in Horn theories ⋮ 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 ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II ⋮ Observational proofs by rewriting.
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- On word problems in Horn theories
- A superposition oriented theorem prover
- Termination of rewriting
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Problem corner: Reasoning about equality
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Unit Refutations and Horn Sets
- Proving refutational completeness of theorem-proving strategies
- A Machine-Oriented Logic Based on the Resolution Principle
- The Concept of Demodulation in Theorem Proving
This page was built for publication: Theorem-proving with resolution and superposition
