Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo

Guillaume Bury; David Delahaye; Damien Doligez; Pierre Halmagrand; Olivier Hermant

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo

Guillaume Bury ¹ David Delahaye ¹ Damien Doligez ² Pierre Halmagrand ^{1, 3} Olivier Hermant ⁴

1 CEDRIC - Centre d'étude et de recherche en informatique et communications

2 GALLIUM - Programming languages, types, compilation and proofs

Inria Paris-Rocquencourt

3 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique

Inria Paris-Rocquencourt

4 CRI - Centre de Recherche en Informatique

Abstract : We introduce an encoding of the set theory of the B method using polymorphic types and deduction modulo, which is used for the automated verication of proof obligations in the framework of theBWare project. Deduction modulo is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We also present the associated automated theorem prover Zenon Modulo, an extension of Zenon to polymorphic types and deduction modulo, along with its backend to the Dedukti universal proof checker, which also relies on types and deduction modulo, and which allows us to verify the proofs produced by Zenon Modulo. Finally, we assess our approach over the proof obligation benchmark of BWare.

Keywords : Dedukti Zenon Modulo Deduction Modulo Typed Proof Search B Method Set Theory Automated Deduction

Type de document :

Communication dans un congrès

LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58

Domaine :

Informatique [cs] / Langage de programmation [cs.PL]

Liste complète des métadonnées

Littérature citée [22 références] Voir Masquer Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-01204701
Contributeur : Claire Medrala <>
Soumis le : mardi 15 décembre 2015 - 11:12:20
Dernière modification le : mardi 13 novembre 2018 - 17:10:03
Document(s) archivé(s) le : samedi 29 avril 2017 - 14:08:06

A-615-v2.pdf

Fichiers produits par l'(les) auteur(s)

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo

Fichier

Identifiants

Collections

Citation

Exporter

Métriques

418

161

Contact

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo

Fichier

Identifiants

Collections

Citation

Exporter

Partager

Métriques

418

161

Contact