Soundly proving B method formulæ using typed sequent calculus

DOI10.1007/978-3-319-46750-4_12MaRDI QIDQ3179401zbMATH OpenOpenAlexFDO

Authors 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

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)

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

Cites work

• scientific article; zbMATH DE number 2080009 (Why is no real title available?)
• Encoding monomorphic and polymorphic types
• The B-Book
• Theorem proving modulo
• Verifying B proof rules using deep embedding and automated theorem proving
• Why Would You Trust B?
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

Cited in

(4)

• scientific article; zbMATH DE number 1615249 (Why is no real title available?)
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Verifying B proof rules using deep embedding and automated theorem proving
• Why Would You Trust B?

Describes a project that uses

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)