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...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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.