TY - JOUR
T1 - Decision procedures
T2 - An algorithmic point of view, by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008
AU - Barrett, Clark
PY - 2013/12
Y1 - 2013/12
N2 - The topic of the Journal of Automated Reasoning is decision procedures for first-order theories, a research area referred to as Satisfiability Modulo Theories (SMT). The book is important for being one of the first to capture the essential concepts of SMT in a book. The book is structured in the form of a high-level introductory chapter and a chapter on propositional logic and Boolean satisfiability (SAT). The majority of the content deals with decision procedures for specific first-order theories, including equality with uninterpreted functions, linear arithmetic, bit vectors, arrays, and pointer logic. Chapter 1 is an introduction and begins with an important point about the book's perspective. Chapter 2 covers propositional logic with a focus on Boolean satisfiability (SAT) and binary decision diagrams (BDDs). Two classic methods are also discussed for removing function symbols in Ackermann's method and Bryant's method.
AB - The topic of the Journal of Automated Reasoning is decision procedures for first-order theories, a research area referred to as Satisfiability Modulo Theories (SMT). The book is important for being one of the first to capture the essential concepts of SMT in a book. The book is structured in the form of a high-level introductory chapter and a chapter on propositional logic and Boolean satisfiability (SAT). The majority of the content deals with decision procedures for specific first-order theories, including equality with uninterpreted functions, linear arithmetic, bit vectors, arrays, and pointer logic. Chapter 1 is an introduction and begins with an important point about the book's perspective. Chapter 2 covers propositional logic with a focus on Boolean satisfiability (SAT) and binary decision diagrams (BDDs). Two classic methods are also discussed for removing function symbols in Ackermann's method and Bryant's method.
UR - http://www.scopus.com/inward/record.url?scp=84891507268&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84891507268&partnerID=8YFLogxK
U2 - 10.1007/s10817-013-9295-4
DO - 10.1007/s10817-013-9295-4
M3 - Article
AN - SCOPUS:84891507268
SN - 0168-7433
VL - 51
SP - 453
EP - 456
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
IS - 4
ER -