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 auto-tactic. If the auto-tactic runs out of memory, remove PP.

• If the model is small, add PP after lasso and P1 to the auto-tactic.

• Whenever you think that the current proof obligation should be discharged automatically, invoke the auto-tactic ( ) 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.

  • 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 auto-tactic because they have a longer timeout.

  • The configurations that act on more than the selected hypotheses (unrestricted P1, PP and ML) become useless when the model grows.

• 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).