Abstract
The method of resolution, invented by J.A. Robinson in 1965, is an efficient method for searching for a proof. In this section, we introduce resolution for the propositional logic, though its advantages will not become apparent until it is extended to first-order logic. It is important to become familiar with resolution, because it is widely used in automatic theorem provers and it is also the basis of logic programming (Chap. 11).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
M. Fitting. First-Order Logic and Automated Theorem Proving (Second Edition). Springer, 1996.
A. Nerode and R.A. Shore. Logic for Applications (Second Edition). Springer, 1997.
G.S. Tseitin. On the complexity of derivation in propositional calculus. In A.O. Slisenko, editor, Structures in Constructive Mathematics and Mathematical Logic, Part II, pages 115–125. Steklov Mathematical Institute, 1968.
A. Urquhart. Hard examples for resolution. Journal of the ACM, 34:209–219, 1987.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag London
About this chapter
Cite this chapter
Ben-Ari, M. (2012). Propositional Logic: Resolution. In: Mathematical Logic for Computer Science. Springer, London. https://doi.org/10.1007/978-1-4471-4129-7_4
Download citation
DOI: https://doi.org/10.1007/978-1-4471-4129-7_4
Publisher Name: Springer, London
Print ISBN: 978-1-4471-4128-0
Online ISBN: 978-1-4471-4129-7
eBook Packages: Computer ScienceComputer Science (R0)