Soundly Proving B Method Formulæ Using Typed Sequent Calculus

DOI10.1007/978-3-319-46750-4_12zbMath1482.68270OpenAlexW2522872546MaRDI QIDQ3179401

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

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

Related Items (1)

First-order automated reasoning with theories: when deduction modulo theory meets practice

Uses Software

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

Cites Work

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

This page was built for publication: Soundly Proving B Method Formulæ Using Typed Sequent Calculus