## Rodin HandbookThis 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 |
## 3.4.3 Proof TacticsTactics 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.
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 TacticsBasic tactics are tactics that change the proof tree only at the point of application. Prune - This tactic is a direct application of the pruning facility providing by the proof tree. The tactic is successful if the input node is not pending. Rule Application Tactics - Tactics of this class provide a wrapper around a proof rule (3.4.2). The tactic is successful if the proof rule is successfully applied to the input node. Reasoner Application Tactics - Tactics of this class provide a wrapper around a reasoner (3.4.6). The tactic is successful if the reasoner is successfully applied to the input node.
## 3.4.3.2 Tactical TacticsTactical tactics are constructed from existing tactics. They indicate different strategic or heuristic decisions. Apply on All Pending - A tactic to apply a specific sub-tactic to all pending nodes at the point of application. The tactic is successful if the sub-tactic is successful on one of the pending nodes. Repeating - A tactic that repeats a specific sub-tactic at the point of application until it fails. The tactic is successful if a sub-tactic is successful at least once. Composing Sequential - A tactic to compose a list of sub-tactics that can be applied to the point of application. The tactic is successful if one of the sub-tactics is successful.
More complex proof strategy can be constructed by combining the above tactical tactics. |