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 2013

Fingerprint

Binary decision diagrams

ASJC Scopus subject areas

  • Artificial Intelligence
  • Software
  • Computational Theory and Mathematics

Cite this

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

In: Journal of Automated Reasoning, Vol. 51, No. 4, 12.2013, p. 453-456.

Research output: Contribution to journalArticle

@article{0c8b1a1010e34ef3a24f71b05fc1de06,
title = "Decision procedures: An algorithmic point of view, by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008",
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.",
author = "Clark Barrett",
year = "2013",
month = "12",
doi = "10.1007/s10817-013-9295-4",
language = "English (US)",
volume = "51",
pages = "453--456",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "4",

}

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

VL - 51

SP - 453

EP - 456

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 4

ER -