Proof Manager: Difference between revisions
imported>Son No edit summary |
imported>Son No edit summary |
||
| Line 3: | Line 3: | ||
Proof obligations are generated by the proof obligation generator and have the form of ''[[Sequents]]''. | 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 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. | 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. | ||
| Line 16: | Line 16: | ||
== Proof Trees == | == Proof Trees == | ||
Revision as of 13:58, 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.
Proof Trees
Proof Trees are recursive structure based on Proof Tree Nodes. Each node has three components:
1. sequent A sequent.
2. rule A proof rule (possibly null)
3. children A list of proof tree nodes (possibly null or empty).
A proof tree is a proof tree node where its sequent corresponding to the proof obligation.
A proof tree node has different statuses:
a. Pending No rule applied to this node, i.e. rule is null. In this case, children must be null.
b. Not pending Has a rule applied to this node. In this case, children contains the list of child proof tree nodes.
