Proof Trees - Revision history

imported>Mathieu: Category:Proof

2009-08-12T12:52:03Z

← Older revision		Revision as of 12:52, 12 August 2009
Line 49:		Line 49:
	[[Category:Design]]		[[Category:Design]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]
			[[Category:Proof]]

imported>Mathieu at 14:18, 30 October 2008

2008-10-30T14:18:20Z

← Older revision		Revision as of 14:18, 30 October 2008
Line 47:		Line 47:
	{{TODO\|}}		{{TODO\|}}

	[[Category:~~Developer documentation~~]]		[[Category:Design]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Mathieu: Robot: Changing Category:Developer Documentation

2008-09-10T21:27:23Z

Robot: Changing Category:Developer Documentation

← Older revision		Revision as of 21:27, 10 September 2008
Line 47:		Line 47:
	{{TODO\|}}		{{TODO\|}}

			[[Category:Developer documentation]]
	[[Category:Developer ~~Documentation~~]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Mathieu: Category + use of :Template:TODO which allow to track all todo left in the wiki

2008-09-10T19:02:45Z

Category + use of Template:TODO which allow to track all todo left in the wiki

← Older revision		Revision as of 19:02, 10 September 2008
Line 45:		Line 45:

	== Example of Proof Trees ==		== Example of Proof Trees ==
	TODO		{{TODO\|}}


			[[Category:Developer Documentation]]
			[[Category:Rodin Platform]]

imported>Son at 15:21, 10 September 2008

2008-09-10T15:21:24Z

← Older revision		Revision as of 15:21, 10 September 2008
Line 43:		Line 43:

	* '''Checking if the proof tree is complete''' A proof tree is complete if it does not contain any pending proof tree node.		* '''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

imported>Son at 14:22, 10 September 2008

2008-09-10T14:22:44Z

← Older revision		Revision as of 14:22, 10 September 2008
Line 13:		Line 13:
	a. '''Pending''' No rule applied to this node, i.e. ''rule'' is ''null''. In this case, ''children'' must be ''null''.		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.		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.

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...

2008-09-10T14:02:52Z

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...

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. '''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.