Using forcing to prove completeness of resolution and paramodulation

DOI10.1016/S0747-7171(08)80130-7zbMATH Open0723.68093OpenAlexW2072984710MaRDI QIDQ757093FDOQ757093

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

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

zbMATH Keywords

resolutioncompletenessforcingparamodulationfirst-order logic with equality

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Proving termination with multiset orderings
• Orderings for term-rewriting systems
• A Machine-Oriented Logic Based on the Resolution Principle
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination of rewriting
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proving refutational completeness of theorem-proving strategies
• Title not available (Why is that?)
• Set theory. An introduction to independence proofs. 2nd print
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem-proving with resolution and superposition
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Title not available (Why is that?)
• Proving Theorems with the Modification Method
• Title not available (Why is that?)
• Proof normalization for resolution and paramodulation
• Ultraproducts of finite sets
• Completing theories by forcing

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
• Title not available (Why is that?)
• 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)