Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants

Pascal Fontaine 1 Jean-Yves Marion 2 Stephan Merz 1 Leonor Prensa Nieto 1 Alwen Tiu 2
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Formal system development needs expressive specification languages, but also calls for highly automated tools. These two goals are not easy to reconcile, especially if one also aims at high assurances for correctness. In this paper, we describe a combination of Isabelle/HOL with a proof-producing SMT (Satisfiability Modulo Theories) solver that contains a SAT engine and a decision procedure for quantifier-free first-order logic with equality. As a result, a user benefits from the expressiveness of Isabelle/HOL when modeling a system, but obtains much better automation for those fragments of the proofs that fall within the scope of the (automatic) SMT solver. Soundness is not compromised because all proofs are submitted to the trusted kernel of Isabelle for certification. This architecture is straightforward to extend for other interactive proof assistants and proof-producing reasoners.
Keywords : theorem proving decision procedures tool integration proof certification SMT solver
Type de document :
Communication dans un congrès
Holger Hermanns and Jens Palsberg. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'06, Mar 2006, Vienna/Austria, Springer, 3920, pp.167-181, 2006, Lecture Notes in Computer Science. 〈10.1007/11691372_11〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00001088
Contributeur : Stephan Merz <>
Soumis le : jeudi 2 février 2006 - 17:06:57
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Tiu. Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. Holger Hermanns and Jens Palsberg. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'06, Mar 2006, Vienna/Austria, Springer, 3920, pp.167-181, 2006, Lecture Notes in Computer Science. 〈10.1007/11691372_11〉. 〈inria-00001088〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

258

Contact


archive-ouverte@inria.fr