On the relation between resolution based and completion based theorem proving

DOI10.1016/S0747-7171(08)80135-6zbMATH Open0724.68081MaRDI QIDQ758218FDOQ758218

Authors: Ralf Socher 

Publication date: 1991

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

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

zbMATH Keywords

resolutionrefutationsuperpositionBoolean ringsCompletion

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Title not available (Why is that?)
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Title not available (Why is that?)
• On Cores and Prime Implicants of Truth Functions
• Refutational theorem proving using term-rewriting systems
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (4)

• Theorem proving by chain resolution
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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)