Proof Trees
From Event-B
Revision as of 14:02, 10 September 2008 by imported>Son (New page: ''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. '''c...)
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.