Using forcing to prove completeness of resolution and paramodulation

DOI10.1016/S0747-7171(08)80130-7MaRDI QIDQ757093zbMATH OpenOpenAlexFDO

Authors 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

resolutioncompletenessforcingparamodulationfirst-order logic with equality

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Proof normalization for resolution and paramodulation
• Proving refutational completeness of theorem-proving strategies
• Completeness of resolution revisited
• Theorem-proving with resolution and superposition
• Completeness by forcing

Cites work

• scientific article; zbMATH DE number 3888510 (Why is no real title available?)
• scientific article; zbMATH DE number 3869258 (Why is no real title available?)
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 4053061 (Why is no real title available?)
• scientific article; zbMATH DE number 3784831 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 3286895 (Why is no real title available?)
• scientific article; zbMATH DE number 3289430 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3335896 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• scientific article; zbMATH DE number 3198011 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Completing theories by forcing
• Orderings for term-rewriting systems
• Proof normalization for resolution and paramodulation
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• Proving termination with multiset orderings
• Set theory. An introduction to independence proofs. 2nd print
• Termination of rewriting
• Theorem-proving with resolution and superposition
• Ultraproducts of finite sets

Cited in

(8)

• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• On the termination of clause graph resolution
• Local simplification
• Completeness by forcing
• Automated deduction with associative-commutative operators
• scientific article; zbMATH DE number 4049135 (Why is no real title available?)
• Redundancy criteria for constrained completion
• Redundancy criteria for constrained completion

This page was built for publication: Using forcing to prove completeness of resolution and paramodulation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q757093)