On the relation between resolution based and completion based theorem proving

DOI10.1016/S0747-7171(08)80135-6zbMath0724.68081MaRDI QIDQ758218

Rolf Socher-Ambrosius

Publication date: 1991

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

zbMATH Keywords

Boolean ringssuperpositionresolutionrefutationCompletion

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (1)

Theorem proving by chain resolution

Cites Work

• Refutational theorem proving using term-rewriting systems
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• On Cores and Prime Implicants of Truth Functions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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