Using forcing to prove completeness of resolution and paramodulation

DOI10.1016/S0747-7171(08)80130-7zbMath0723.68093OpenAlexW2072984710MaRDI QIDQ757093

John Pais, Gerald E. Peterson

Publication date: 1991

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

Full work available at URL: https://doi.org/10.1016/s0747-7171(08)80130-7

zbMATH Keywords

completenessforcingresolutionparamodulationfirst-order logic with equality

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Automated deduction with associative-commutative operators, On the termination of clause graph resolution, Redundancy criteria for constrained completion, Redundancy criteria for constrained completion, Local simplification, Cancellative Abelian monoids and related structures in refutational theorem proving. I

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
• Orderings for term-rewriting systems
• Theorem-proving with resolution and superposition
• Set theory. An introduction to independence proofs. 2nd print
• Termination of rewriting
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Proving termination with multiset orderings
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• Proof normalization for resolution and paramodulation
• A Machine-Oriented Logic Based on the Resolution Principle
• Ultraproducts of finite sets
• Completing theories by forcing