This work is sponsored by the
Deploy Project
This work is sponsored by the
ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
How to Use the Provers Effectively
Rodin User’s Handbook v.2.8
 



Rodin User’s Handbook v.2.8 



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 PP restricted, P0, and ML to the autotactic. If the autotactic runs out of memory, remove PP. If the model is small, add PP after lasso and P1 to the autotactic. Whenever you think that the current proof obligation should be discharged automatically, invoke the autotactic (
) instead of some particular automatic prover. If the autotactic 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. Create a case distinction Instantiate quantifiers. Apply ae (abstract expression) to replace complicated expressions with fresh variables.
You can also apply one of the automatic provers. They may be more successful than the autotactic because they have a longer timeout. When everything fails, try to solve the proof obligation manually by clicking on the red symbols.
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 (4.2.9).
