On the termination of clause graph resolution

DOI10.1007/BF00881913zbMath0819.68112OpenAlexW1992809260MaRDI QIDQ1344889

V. Pereyra

Publication date: 22 February 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00881913

zbMATH Keywords

extended clause graph resolutionKowalski's clause graph resolution

Mathematics Subject Classification ID

Related Items

On the termination of clause graph resolution

Cites Work

• Using forcing to prove completeness of resolution and paramodulation
• Properties of substitutions and unifications
• Termination of rewriting
• Refutation graphs
• On the termination of clause graph resolution
• Linear resolution with selection function
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Theorem Proving via General Matings
• On Matrices with Connections
• Refutations by Matings
• A Proof Procedure Using Connection Graphs
• A Machine-Oriented Logic Based on the Resolution Principle
• Resolution With Merging
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item