Satisfiability Modulo Theories Conclusions

Tjark Weber

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

Sujets

• École polytechnique
• Automated proof checking

Informations

• Publié par: chaeh
• Nombre de lectures: 12
• Langue: English

Extrait

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