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.
ASJC Scopus subject areas
- Computational Theory and Mathematics
- Artificial Intelligence