imported>Mathieu |
imported>Andy |
| Line 1: |
Line 1: |
| − | ''Proof trees'' are recursive structure based on ''Proof Tree Nodes''. Each node has three components:
| + | #REDIRECT [[Prover Diagrams]] |
| − | | |
| − | 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|}}
| |
| − | | |
| − | [[Category:Design]] | |
| − | [[Category:Rodin Platform]]
| |
| − | [[Category:Proof]]
| |
