Decision Procedures: An Algorithmic Point of View
Daniel Kroening, Ofer Strichman · 2008
A decision procedure is an algorithm that, given a decision problem, terminates with a correct yes/no answer.Here, the authors focus on theories that are expressive enough to model real problems, but are still decidable.Specifically, the book concentrates on decision procedures for first-order theories that are commonly used in automated verification and reasoning, theorem-proving, compiler optimization and operations research.The techniques described in the book draw from fields such as graph theory and logic, and are routinely used in industry.