Proof Manager: Difference between revisions
imported>Son No edit summary |
imported>Son No edit summary |
||
| Line 7: | Line 7: | ||
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. | 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''. | By applying the generated proof rules by different reasoner, the Proof Manager builds a (partial) proof for an proof obligation by constructing ''[[proof trees]]''. | ||
* [[Sequents]] | * [[Sequents]] | ||
| Line 14: | Line 14: | ||
* [[Proof Trees]] | * [[Proof Trees]] | ||
Revision as of 14:02, 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.
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.
