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.