Proof Trees: Difference between revisions
imported>Mathieu m Category + use of Template:TODO which allow to track all todo left in the wiki |
imported>Mathieu m Robot: Changing Category:Developer Documentation |
||
| Line 47: | Line 47: | ||
{{TODO|}} | {{TODO|}} | ||
[[Category:Developer documentation]] | |||
[[Category:Developer | |||
[[Category:Rodin Platform]] | [[Category:Rodin Platform]] | ||
Revision as of 21:27, 10 September 2008
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
