Difference between revisions of "Extending the Proof Manager"

From Event-B
Jump to navigationJump to search
imported>Son
(New page: The Proof Manager is to ...)
 
imported>Son
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