Rodin Handbook


3.4 Proving

In Section 3.2.7, we learned what proof obligations are generated by Rodin from an Event-B model. We validate the model by discharging proof obligations. This is what we call proving.


In this chapter we will:

  • Explain proof rules

  • Explain tactics

  • Explain and describe provers

  • Explain reasoners

  • Describe how to perform automatic and manual proving

  • Purge proofs for maintenance

  • Simplify proofs for maintenability and storage