Rodin Proof Tactics

From Event-B
Revision as of 21:30, 6 March 2010 by imported>Son
Jump to navigationJump to search

This page contains descriptions of the available proof tactics within the RODIN Platform.

For each tactic, the descriptions is as follows:

  • ID: The unique ID for each tactic.
  • Description: A high-level description of the tactic
  • Display: How an application of the tactic is displayed in the proof tree, the auto-tactic preference or the post-tactic preference.
  • Auto-tactic: No: the tactic cannot be added as auto-tactic. Yes: the tactic can be added as auto-tactic. Default: the tactic is a default auto-tactic.