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)

zbMATH Keywords

resolutionrefutationsuperpositionBoolean ringsCompletion

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

• 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?)
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• On Cores and Prime Implicants of Truth Functions
• Refutational theorem proving using term-rewriting systems

Cited in

(4)

• 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)