LARA Exercise 14 Slides: 1.pptx, 1.pdf 2.pptx, 2.pdf 3.pptx, 3.pdf 4.pptx, 4.pdf Combining FOL Models Summary: SAT + theories lazy approach and eager approach small models and Ackerman encoding quantifier instantiation Deciding Quantifier-Free FOL 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 Deciding Quantifier-Free FOL over Ground Terms Arithmetic and Eager Encoding Eager SAT Encoding Quantifier Instantiation Local Theories References 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