Difference between pages "Proof Skeleton View" and "Proof Trees"
From Event-B
(Difference between pages)
Jump to navigationJump to searchimported>Mathieu m (→Showing the View: use menu template) |
imported>Mathieu m (Category:Proof) |
||
| Line 1: | Line 1: | ||
| − | + | ''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. '''Non-pending''' Has a rule applied to this node. In this case, ''children'' contains the list of child proof tree nodes. | |
| − | + | We now review the constraints on the proof trees, follows by different operations on the proof trees. | |
| − | + | == Constraints on Proof Trees == | |
| + | A proof tree is valid if all its proof tree nodes are valid. | ||
| + | A ''pending'' proof tree node is valid if its ''children'' is ''null'' | ||
| − | [[Category: | + | A ''non-pending'' proof tree node is valid if: |
| + | |||
| + | * It's ''children'' is not ''null''. | ||
| + | |||
| + | * ''rule'' (which is not ''null'') is applicable to the ''sequent''. | ||
| + | |||
| + | * ''children'' corresponding to the result of the application of ''rule'' to ''sequent''. | ||
| + | |||
| + | * Each of the ''children'' proof tree nodes is valid. | ||
| + | |||
| + | == Operations on Proof Trees == | ||
| + | |||
| + | * '''Construction''' Create an initial proof tree corresponding to an input sequent. The resulting proof tree containing a single root node. This root node is a pending node with corresponding to an input sequent. | ||
| + | |||
| + | * '''Rule application''' A proof tree ''grows'' when a rule applies to one of its pending node. The input rule is first check for applicability to the sequent corresponding to the pending node. If successful, the rule is attach to the node, then a new ''children'' nodes are attached according to the outcome of the application of the rule. | ||
| + | |||
| + | * '''Pruning''' A proof tree can be ''pruned'' at any of its proof tree nodes. The ''rule'' and the ''children'' associated with that node will be removed (reset to ''null''). | ||
| + | |||
| + | * '''Getting the list of pending nodes''' A list of pending nodes can be computed for any proof tree. | ||
| + | |||
| + | * '''Checking if the proof tree is complete''' A proof tree is complete if it does not contain any pending proof tree node. | ||
| + | |||
| + | == Example of Proof Trees == | ||
| + | {{TODO|}} | ||
| + | |||
| + | [[Category:Design]] | ||
| + | [[Category:Rodin Platform]] | ||
| + | [[Category:Proof]] | ||
Latest revision as of 12:52, 12 August 2009
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. Non-pending Has a rule applied to this node. In this case, children contains the list of child proof tree nodes.
We now review the constraints on the proof trees, follows by different operations on the proof trees.
Constraints on Proof Trees
A proof tree is valid if all its proof tree nodes are valid.
A pending proof tree node is valid if its children is null
A non-pending proof tree node is valid if:
- It's children is not null.
- rule (which is not null) is applicable to the sequent.
- children corresponding to the result of the application of rule to sequent.
- Each of the children proof tree nodes is valid.
Operations on Proof Trees
- Construction Create an initial proof tree corresponding to an input sequent. The resulting proof tree containing a single root node. This root node is a pending node with corresponding to an input sequent.
- Rule application A proof tree grows when a rule applies to one of its pending node. The input rule is first check for applicability to the sequent corresponding to the pending node. If successful, the rule is attach to the node, then a new children nodes are attached according to the outcome of the application of the rule.
- Pruning A proof tree can be pruned at any of its proof tree nodes. The rule and the children associated with that node will be removed (reset to null).
- Getting the list of pending nodes A list of pending nodes can be computed for any proof tree.
- Checking if the proof tree is complete A proof tree is complete if it does not contain any pending proof tree node.
Example of Proof Trees
TODO
