Content: Efficient Decision Procedures

• Basic Concepts
  • Motivation
  • First-Order Logic
  • First-Order Theories
  • Decision Procedures
• Propositional Logic
  • Introduction
  • CNF Conversion
  • Polynomial Subclasses
  • The DPLL Procedure
  • The Stålmarck Procedure
  • Binary Decision Diagrams
• Equality Logic
  • Introduction
  • Congruence Closure
  • Uninterpreted Functions
  • The Sparse Method
  • Domain Allocation
• Linear Arithmetic
  • Introduction
  • The Simplex Method
  • Branch and Bound
  • Fourier-Motzkin
  • The Omega Test
  • Difference Logic
• Bit-Vector Arithmetic
  • Introduction
  • Bit Blasting
  • Incremental Bit Blasting
  • Fixed-Point Arithmetic
  • Linear Modulo-Arithmetic
• Array Logic
  • Introduction
  • Array Properties
  • Quantifier Elimination
• Pointer Logic
  • Introduction
  • Semantic Translation
  • Dynamic Data Structures
  • Separation Logic
• Combined Theories
  • Introduction
  • The Nelson-Oppen Procedure
  • SAT Modulo Theories