Abstract
Let F be a CNF formula. We will describe a method of transforming F into a formula equivalent to F and richer in clauses. This method then decides whether F is unsatisfiable, and whenever F is satisfiable it finds an assignment that satisfies F.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Italia
About this chapter
Cite this chapter
Mundici, D. (2012). The Resolution Method. In: Logic: A Brief Course. UNITEXT(). Springer, Milano. https://doi.org/10.1007/978-88-470-2361-1_3
Download citation
DOI: https://doi.org/10.1007/978-88-470-2361-1_3
Publisher Name: Springer, Milano
Print ISBN: 978-88-470-2360-4
Online ISBN: 978-88-470-2361-1
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)