Difference between revisions of "Proof Manager"
imported>Son (New page: The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations. For this, the Proof Manager architecture is separated into two ...) |
imported>Son |
||
| Line 7: | Line 7: | ||
== Reasoners == | == Reasoners == | ||
Reasoners are responsible for generating proof rules. The input of a reasoner is: | Reasoners are responsible for generating proof rules. The input of a reasoner is: | ||
| + | |||
1. A sequent. | 1. A sequent. | ||
| + | |||
2. Optional input (e.g. a predicate in the case of the Cut Rule). | 2. Optional input (e.g. a predicate in the case of the Cut Rule). | ||
| + | |||
The output of the reasoner (in case of successful) is a proof rule. This proof rule is ''trusted'' by the Proof Manager to built the proof. | The output of the reasoner (in case of successful) is a proof rule. This proof rule is ''trusted'' by the Proof Manager to built the proof. | ||
An important point about reasoners is that the internal workings of them are not visible to the other part of the Proof Manager. It is only required that they satisfy the following requirements: | An important point about reasoners is that the internal workings of them are not visible to the other part of the Proof Manager. It is only required that they satisfy the following requirements: | ||
| + | |||
a. '''Logically Valid''' A generated proof rule must be valid (i.e. can be derived) in the mathematical logic. | a. '''Logically Valid''' A generated proof rule must be valid (i.e. can be derived) in the mathematical logic. | ||
| + | |||
b. '''Replayable''' A reasoner must work ''deterministically'', i.e. given the same input, a reasoner must generate the same proof rule every time. | b. '''Replayable''' A reasoner must work ''deterministically'', i.e. given the same input, a reasoner must generate the same proof rule every time. | ||
== Maintaining Existing Proofs == | == Maintaining Existing Proofs == | ||
Revision as of 13:23, 10 September 2008
The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.
For this, 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.
Reasoners
Reasoners are responsible for generating proof rules. The input of a reasoner is:
1. A sequent.
2. Optional input (e.g. a predicate in the case of the Cut Rule).
The output of the reasoner (in case of successful) is a proof rule. This proof rule is trusted by the Proof Manager to built the proof.
An important point about reasoners is that the internal workings of them are not visible to the other part of the Proof Manager. It is only required that they satisfy the following requirements:
a. Logically Valid A generated proof rule must be valid (i.e. can be derived) in the mathematical logic.
b. Replayable A reasoner must work deterministically, i.e. given the same input, a reasoner must generate the same proof rule every time.
