3.4.3 Proof Tactics

Tactics provide an easier way to construct and manage proof search and manipulation. They provide calls to the underlying reasoners or other tactics to modify proofs.

\includegraphics[width=7mm]{img/info_64.png}

A list of all proof tactics is maintained in the Rodin Wiki.1 This list is very comprehensive — be sure to check it out!

Tactics can be applied as follows:

Automatic

Rodin can automatically apply a number of tactics after each manual proof step.

Proof tree

Pruning the proof tree is a tactic that can be applied from the proof tree through the context menu. Other tactics may be available there.

In sequents

Some sequents have elements that are highlighted in red. Clicking on these elements brings up a menu with all applicable tactics so that they can be applied manually.

It may be useful to consider the following categories of tactics:

3.4.3.1 Basic Tactics

Basic tactics are tactics that change the proof tree only at the point of application.

3.4.3.2 Tactical Tactics

Tactical tactics are constructed from existing tactics. They indicate different strategic or heuristic decisions.

More complex proof strategy can be constructed by combining the above tactical tactics.

Footnotes

  1. http://wiki.event-b.org/index.php/Rodin_Proof_Tactics