On the termination of clause graph resolution
From MaRDI portal
Publication:1344889
DOI10.1007/BF00881913zbMATH Open0819.68112OpenAlexW1992809260MaRDI QIDQ1344889FDOQ1344889
Authors: 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
Recommendations
Cites Work
- A Proof Procedure Using Connection Graphs
- Title not available (Why is that?)
- A Machine-Oriented Logic Based on the Resolution Principle
- Properties of substitutions and unifications
- Termination of rewriting
- Linear resolution with selection function
- Resolution With Merging
- Theorem Proving via General Matings
- On Matrices with Connections
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Using forcing to prove completeness of resolution and paramodulation
- On the termination of clause graph resolution
- Title not available (Why is that?)
- Refutation graphs
- Refutations by Matings
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (9)
- Recognizing unnecessary clauses in resolution based systems
- Link inheritance in abstract clause graphs
- On the termination of clause graph resolution
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
This page was built for publication: On the termination of clause graph resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1344889)
