Decision procedures: An algorithmic point of view, by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008

Clark Barrett

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish (US)
Pages (from-to)453-456
Number of pages4
JournalJournal of Automated Reasoning
Volume51
Issue number4
DOIs
StatePublished - Dec 1 2013

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Decision procedures: An algorithmic point of view, by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008'. Together they form a unique fingerprint.

  • Cite this