On the termination of clause graph resolution
type: Item
instance of: scholarly article
title: On the termination of clause graph resolution
zbMATH Open document ID: 0819.68112
DOI: 10.1007/BF00881913
author: V. Pereyra
published in: Journal of Automated Reasoning
publication date: 1995-02-22T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 724147
zbMATH Keywords: extended clause graph resolution
zbMATH Keywords: Kowalski's clause graph resolution
MaRDI profile type: Publication
cites work: Resolution With Merging
cites work: Refutations by Matings
cites work: Theorem Proving via General Matings
cites work: Q3917511
cites work: On Matrices with Connections
cites work: Termination of rewriting
cites work: Properties of substitutions and unifications
cites work: Q3783625
cites work: Linear resolution with selection function
cites work: A Proof Procedure Using Connection Graphs
cites work: Q3862380
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q5636315
cites work: Q3880321
cites work: Using forcing to prove completeness of resolution and paramodulation
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Refutation graphs
cites work: Q3881540
cites work: Q3965577
full work available at URL: https://doi.org/10.1007/bf00881913
OpenAlex ID: W1992809260
description: scientific article; zbMATH DE number 724147