Loading presentation...

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers

Dagstuhl Seminar 13411: Deduction and Arithmetic
by

Tjark Weber

on 13 October 2013

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers

Integrating SAT, QBF and SMT Solvers
with Interactive Theorem Provers
Tjark Weber
Dagstuhl Seminar 13411: Deduction and Arithmetic
October 9, 2013
LCF-style Theorem Proving
Theorems are implemented as an abstract data type.
There is a fixed number of constructor functions - one for each axiom/inference rule of higher-order logic.
More complicated proof procedures must be implemented by composing these functions.
Selected HOL4 Inference Rules
Propositional Resolution
Z3 uses 34 different inference rules.
Satisfiability Modulo Theories
Proof Structure
Proofs are
directed acyclic graphs.
Each node corresponds to an inference step.
Children are premises of inferences. Leaves are axioms/input formulas.
A designated root note concludes .
Proofs can be checked by depth-first
post-order traversal
.
1. A single primitive inference/theorem instantiation.
2. Combinations of primitive inferences/theorem instantiations.
3. Automated proof procedures (e.g., for linear arithmetic).
4. Combinations of the above.
Avoiding Automated Proof Procedures
Combinations of primitive inferences
Instantiation of schematic theorems
Generalization wrt. background theories
Memoization
Speed-ups of up to 3 orders of magnitude!
Integrating SAT, QBF and SMT Solvers
with Interactive Theorem Provers

http://user.it.uu.se/~tjawe125/
... with special thanks to the people who made this work possible: Hasan Amjad, Nikolaj Bjørner, Jasmin Blanchette, Sascha Böhme, Leonardo de Moura, Anthony Fox, Ramana Kumar, Sharad Malik, Thomas Sewell, Christoph Wintersteiger, and many others
Conclusions
Proof validation is feasible for SAT, QBF and SMT. It scales to large formulas and proofs with millions of inferences.

Naive solutions are slow - efficient implementations based on sophisticated optimizations are crucial.

Our integrations provide a high degree of
automation
in interactive theorem provers, and
validation
for automated solvers.
LCF-style theorem provers are ...
generic
sound
powerful
e.g., based on higher-order logic
provided their kernel is correct
term rewriting, arithmetic, ...
System Overview
Interactive theorem proving is powerful, but time-consuming, and requires expert knowledge.
Automated theorem proving is easy to use, but (so far) limited in power.
Validation
Automation
Mutual Benefit!
Interactive Theorem Proving
Expressivity
Automation
SMT
Resolution, LCF-style
Proofs
... should be easy (and fast) to
generate
.
... should be easy (and fast) to
check
.
Proof Reconstruction for 'rewrite' and 'th-lemma-bv'
Schematic theorems
Theorem memoization
Strategy selection
rewrite
th-lemma-bv
Evaluation
SAT
QBF
SMT
#validated
#solved
validation time
solving time
100%
87%
18 : 1
100%
1 : 25
1 : 2
75%
19 : 1
invalid
valid
AUFLIA
AUFLIRA
QF_UFLIA
QF_UF
QF_UFLRA
Profiling
Q-resolution is propositional resolution followed by forall-reduction.
Q-Resolution
Q-Resolution, LCF-style
Example
Forall-Reduction, LCF-style
Valid QBF, LCF-style
Thank you!
Combinations of Primitive Inferences
Full transcript