Extending the Proof Manager: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Son
New page: The Proof Manager is to ...
 
imported>Son
No edit summary
Line 1: Line 1:
The [[Proof Manager]] is to ...
The [[Proof Manager]] is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.
 
There are two ways for extending the Proof Manager:
 
# adding a new [[Reasoners|reasoner]].
 
# adding a new [[Tactics|tactic]].
 
== Adding a New Reasoner ==
 
 
== Adding a New Tactic ==

Revision as of 13:06, 11 September 2008

The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.

There are two ways for extending the Proof Manager:

  1. adding a new reasoner.
  1. adding a new tactic.

Adding a New Reasoner

Adding a New Tactic