Proof Manager: Difference between revisions
imported>Son No edit summary |
imported>Son No edit summary |
||
| Line 1: | Line 1: | ||
The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations. | 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 ''[[ | Proof obligations are generated by the proof obligation generator and have the form of ''[[sequents]]''. | ||
Sequents are proved using ''[[ | 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 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]]''. | ||
Revision as of 14:28, 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.
