On the relation between resolution based and completion based theorem proving

DOI10.1016/S0747-7171(08)80135-6MaRDI QIDQ758218zbMATH OpenFDO

Authors Ralf Socher

Publication date 1991

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0747-7171(08)80135-6

zbMATH Keywords

Boolean ringsCompletionrefutationresolutionsuperposition

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 3871320
• Completeness of resolution revisited
• Completion of first-order clauses with equality by strict superposition
• Theorem-proving with resolution and superposition
• Efficient deduction in equality Horn logic by Horn-completion

Cites work

• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• scientific article; zbMATH DE number 4022667 (Why is no real title available?)
• scientific article; zbMATH DE number 4047185 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• On Cores and Prime Implicants of Truth Functions
• Refutational theorem proving using term-rewriting systems

Cited in

(5)

• Well-behaved inference rules for first-order theorem proving
• Theorem proving by chain resolution
• scientific article; zbMATH DE number 3871320 (Why is no real title available?)
• scientific article; zbMATH DE number 1765670 (Why is no real title available?)
• Completeness of resolution revisited

This page was built for publication: On the relation between resolution based and completion based theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q758218)