Satisfiability Modulo Theories Conclusions

-

English
63 Pages
Read an excerpt
Gain access to the library to view online
Learn more

Description

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


Subjects

Informations

Published by
Reads 12
Language English
Report a problem
Introduction SAT Solvers Satisfiability Modulo Theories Conclusions
Integrating SAT with Interactive
Tjark
and SMT Theorem
Weber
TypiCal Seminar Laboratoire d’Informatique ´ Ecole Polytechnique
10 September 2009
Tjark Weber
Solvers Provers
Integrating SAT and SMT Solvers with ITPs
Motivation
1
Introduction SAT Solvers Satisfiability Modulo Theories Conclusions
Motivation LCF-Style Proof Checking
Interactive theorem proving needsautomation. Use SAT solvers to decide formulas of propositional logic. Use SMT solvers to decide SMT formulas. Can we do this without increasing the trusted code base?
Tjark Weber
Integrating SAT and SMT Solvers with ITPs
Motivation
1
2
Introduction SAT Solvers Satisfiability Modulo Theories Conclusions
Motivation LCF-Style Proof Checking
Interactive theorem proving needsautomation. Use SAT solvers to decide formulas of propositional logic. Use SMT solvers to decide SMT formulas. Can we do this without increasing the trusted code base?
SAT and SMT solvers frequently contain bugs. How can we verifytheir results? Proofs (of unsatisfiability) can be checked independently. Can we keep the proof checker small?
Tjark Weber
Integrating SAT and SMT Solvers with ITPs
Introduction SAT Solvers Satisfiability Modulo Theories Conclusions
LCF-Style Proof Checking
Motivation LCF-Style Proof Checking
Theorems are implemented as anabstract data type. They can be constructed only through a fixed set of functions provided by this data type.
Each constructor function implements an axiom or inference rule of the logic.
Advanced proof procedures must (ultimately) employ combinations of primitive inferences.
Tjark Weber
Integrating SAT and SMT Solvers with ITPs
Introduction SAT Solvers Satisfiability Modulo Theories Conclusions
An
LCF-Style
Propositional Logic, Resolution System Overview Proof Reconstruction Representation of SAT Problems Performance
Integration
Proof-Producing
Tjark Weber
SAT
of
Solvers
Integrating SAT and SMT Solvers with ITPs
Introduction SAT Solvers Satisfiability Modulo Theories Conclusions
Propositional Logic
Propositional Logic, Resolution System Overview Proof Reconstruction Representation of SAT Problems Performance
Propositional logic: Boolean variables:p,q, . . . Formulas:ϕ::=p|¬ϕ|ϕϕ|ϕϕ
Tjark Weber
Integrating SAT and SMT Solvers with ITPs