Theorem-proving with resolution and superposition

DOI10.1016/S0747-7171(08)80131-9zbMath0723.68094MaRDI QIDQ757094

Michaël Rusinowitch

Publication date: 1991

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

superpositionresolutionparamodulationcomplete simplification orderingrefutational completeness

Mathematics Subject Classification ID

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