Difference between revisions of "Proof Manager"

From Event-B
Jump to navigationJump to search
imported>Son
imported>Son
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]]
 
 
 
== 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.
 

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.