Satisfiability Modulo Theories Conclusions

Niveau: Supérieur
Introduction SAT Solvers Satisfiability Modulo Theories Conclusions Integrating SAT and SMT Solvers with Interactive Theorem Provers Tjark Weber TypiCal Seminar Laboratoire d'Informatique Ecole Polytechnique 10 September 2009 Tjark Weber Integrating SAT and SMT Solvers with ITPs

• motivation lcf-style


• overview proof


• advanced proof procedures


• proof checking


• proof-producing sat


• introduction sat


• use sat


• sat problems