Soundly proving B method formulæ using typed sequent calculus

DOI10.1007/978-3-319-46750-4_12zbMATH Open1482.68270OpenAlexW2522872546MaRDI QIDQ3179401FDOQ3179401

Pierre Halmagrand

Publication date: 21 December 2016

Published in: Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-46750-4_12

Recommendations

• scientific article; zbMATH DE number 1615249
• scientific article; zbMATH DE number 2172802
• Verifying B proof rules using deep embedding and automated theorem proving
• Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover
• An Automation-Friendly Set Theory for the B Method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• The B-Book
• Encoding Monomorphic and Polymorphic Types
• Theorem proving modulo
• Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving
• Why Would You Trust B?
• Title not available (Why is that?)

Cited In (3)

• Why Would You Trust B?
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Title not available (Why is that?)

Uses Software

• PVS
• Why3
• Zenon
• Atelier B
• BWare
• dedukti

This page was built for publication: Soundly proving B method formulæ using typed sequent calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179401)