In Section 3.2.6, 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