Rodin Handbook
This work is sponsored by the Deploy Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
User Manual for Rodin v.2.3 |  |
 |
 |
3.4.5 How to Use the Provers Effectively
It is very hard, in general, to predict whether a certain automatic prover can or cannot discharge a given proof obligation within a given amount of time. (This is also the case for many other automatic first order theorem provers.) Therefore applying the 11 configurations in a trial and error fashion is often frustrating.
The following guidelines may be useful:
Add New PP restricted (PP restricted), P0 (Atelier B P0), and ML (Atelier B ML) to the auto-tactic. If the auto-tactic runs out of memory, remove New PP.
If the model is small, add New PP after lasso (PP after lasso) and P1 (Atelier B P1) to the auto-tactic.
Whenever you think that the current proof obligation should be discharged automatically, invoke the auto-tactic (
![\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}](images/img-0341.png)
) instead of some particular automatic prover. If the auto-tactic fails, it is usually best to simplify the proof obligation in some way. The most important ways of simplifying the proof obligation are:
Remove unnecessary hypotheses; add required hypotheses that have been missing.
Do some case splits.
Instantiate quantifiers.
Apply ae (abstract expression) to replace complicated expressions by fresh variables.
You can also apply one of the automatic provers. They may be more successful than the auto-tactic because they have a longer timeout.
Try New PP before PP or ML because New PP proofs can be better reused, if the model changes.
The configurations that act on more than the selected hypotheses (New PP after lasso and unrestricted P1, PP and ML) become useless when the model grows.
When everything fails, try to unfold the proof obligation manually, by clicking on the red links.
You may discover that some assumption was missing.
You may complete the proof.
If you observe that a valid proof obligation cannot be proved manually, please send a bug report. (Rodin Bug Tracker)
|
|
|
|
|
|