Combining FOL Models

Summary:

• SAT + theories
• lazy approach and eager approach
• small models and Ackerman encoding
• quantifier instantiation

Deciding Quantifier-Free FOL

Axioms for Equality

Notes on Congruences

Congruence Closure Algorithm and Correctness

Implementing Congruence Closure

Deciding Quantifier-Free FOL over Ground Terms

Eager SAT Encoding

Quantifier Instantiation

Local Theories

• Decision Procedures Based on Congruence Closure
• Greg Nelson: Techniques for Program Verification
• Calculus of Computation Textbook
• SAT and SMT Summer school at MIT 2011
• SAT and SMT Summer school in Trento 2012
• Slides Accompanying Decision Procedures textbook
• SRI Summer School 2004