On the termination of clause graph resolution
From MaRDI portal
Publication:1344889
DOI10.1007/BF00881913zbMath0819.68112MaRDI QIDQ1344889
Publication date: 22 February 1995
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Related Items
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