Using forcing to prove completeness of resolution and paramodulation
type: Item
instance of: scholarly article
title: Using forcing to prove completeness of resolution and paramodulation
zbMATH Open document ID: 0723.68093
DOI: 10.1016/S0747-7171(08)80130-7
author: John Pais
author: Gerald E. Peterson
published in: Journal of Symbolic Computation
publication date: 1991-01-01T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 4193156
zbMATH Keywords: resolution
zbMATH Keywords: paramodulation
zbMATH Keywords: completeness
zbMATH Keywords: first-order logic with equality
zbMATH Keywords: forcing
MaRDI profile type: Publication
cites work: Proof normalization for resolution and paramodulation
cites work: Completing theories by forcing
cites work: Q5570212
cites work: Proving Theorems with the Modification Method
cites work: Q5679729
cites work: Q5573370
cites work: Orderings for term-rewriting systems
cites work: Termination of rewriting
cites work: Proving termination with multiset orderings
cites work: Q3743300
cites work: Proving refutational completeness of theorem-proving strategies
cites work: Ultraproducts of finite sets
cites work: Q5581665
cites work: Set theory. An introduction to independence proofs. 2nd print
cites work: Q3337413
cites work: Q4139711
cites work: Q3962956
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Q5734410
cites work: Q5613180
cites work: Q5624683
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Theorem-proving with resolution and superposition
cites work: Q3221027
cites work: Q3789100
full work available at URL: s0747-7171(08)80130-7
OpenAlex ID: W2072984710
description: scientific article; zbMATH DE number 4193156