On the termination of clause graph resolution

DOI10.1007/BF00881913MaRDI QIDQ1344889zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

extended clause graph resolutionKowalski's clause graph resolution

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 4047183
• scientific article; zbMATH DE number 3986668
• Some techniques for proving termination of the hyperresolution calculus
• scientific article; zbMATH DE number 3990906
• Link inheritance in abstract clause graphs

Cites work

• scientific article; zbMATH DE number 4047183 (Why is no real title available?)
• scientific article; zbMATH DE number 3664336 (Why is no real title available?)
• scientific article; zbMATH DE number 3684933 (Why is no real title available?)
• scientific article; zbMATH DE number 3686368 (Why is no real title available?)
• scientific article; zbMATH DE number 3729473 (Why is no real title available?)
• scientific article; zbMATH DE number 3788022 (Why is no real title available?)
• scientific article; zbMATH DE number 3362981 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Proof Procedure Using Connection Graphs
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Linear resolution with selection function
• On Matrices with Connections
• On the termination of clause graph resolution
• Properties of substitutions and unifications
• Refutation graphs
• Refutations by Matings
• Resolution With Merging
• Termination of rewriting
• Theorem Proving via General Matings
• Using forcing to prove completeness of resolution and paramodulation

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
• scientific article; zbMATH DE number 3986668 (Why is no real title available?)
• scientific article; zbMATH DE number 3990906 (Why is no real title available?)
• scientific article; zbMATH DE number 4047183 (Why is no real title available?)
• scientific article; zbMATH DE number 1926639 (Why is no real title available?)
• scientific article; zbMATH DE number 3858461 (Why is no real title available?)

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)