Skip to Main content Skip to Navigation
Conference papers

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

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Claire Medrala Connect in order to contact the contributor
Submitted on : Tuesday, December 15, 2015 - 11:12:20 AM
Last modification on : Wednesday, September 28, 2022 - 5:58:33 AM
Long-term archiving on: : Saturday, April 29, 2017 - 2:08:06 PM


Files produced by the author(s)


  • HAL Id : hal-01204701, version 2


Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant. Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58. ⟨hal-01204701v2⟩



Record views


Files downloads