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