Tjark Weber

Abstract:

We provide an overview of working integrations of SAT, QBF and SMT
solvers with interactive theorem provers Isabelle and HOL4.  Our
integrations do not need to be trusted: the external solvers generate
certificates that are checked by the ITPs' kernels.  Evaluation on large
benchmark collections shows that LCF-style certificate checking is
feasible even for proofs with millions of inferences.


Suggested topics/questions for discussion:

* Usability, maintainability, performance -- what are the main
  requirements that users and system developers have for external tool
  integrations?

* From proof formats to proof standards -- what should proof
  certificates look like, and how do we establish tool-independent
  standards?