Proof Manager: Difference between revisions
imported>Son mNo edit summary |
imported>Son No edit summary |
||
| Line 10: | Line 10: | ||
By applying the generated proof rules by different reasoner, the Proof Manager builds a (partial) proof for an proof obligation by constructing ''[[Proof Trees]]''. | By applying the generated proof rules by different reasoner, the Proof Manager builds a (partial) proof for an proof obligation by constructing ''[[Proof Trees]]''. | ||
In order to encapsulate frequently used proof construction and manipulation steps, the Proof Manager provides the concept of ''[[Tactics]]''. They provides high-level strategic proof manipulation. Adding a new tactic is the second possibility for extending the Proof Manager. | |||
* [[Sequents]] | * [[Sequents]] | ||
| Line 18: | Line 20: | ||
* [[Proof Trees]] | * [[Proof Trees]] | ||
* [[Tactics]] | |||
[[Category:Developer Documentation]] | [[Category:Developer Documentation]] | ||
[[Category:Rodin Platform]] | [[Category:Rodin Platform]] | ||
Revision as of 15:25, 10 September 2008
The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.
Proof obligations are generated by the proof obligation generator and have the form of Sequents.
Sequents are proved using Proof Rules.
The Proof Manager architecture is separated into two parts: extensible part and static part. The extensible part is responsible for generating individual proof rules. The static part is responsible for putting proof rules together to construct and manage proofs. We call components that generate valid proof rules Reasoners.
The basic reasoning capabilities of the Proof Manager can be extended by adding new reasoners. A reasoner may implement a decision procedure for automated proof, or a derived rule schema for interactive proof.
By applying the generated proof rules by different reasoner, the Proof Manager builds a (partial) proof for an proof obligation by constructing Proof Trees.
In order to encapsulate frequently used proof construction and manipulation steps, the Proof Manager provides the concept of Tactics. They provides high-level strategic proof manipulation. Adding a new tactic is the second possibility for extending the Proof Manager.
