Difference between pages "Proof Trees" and "Help:Contents"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
m
 
imported>Mathieu
 
Line 1: Line 1:
−
''Proof trees'' are recursive structure based on ''Proof Tree Nodes''. Each node has three components:
+
''Help copied from [http://www.mediawiki.org/wiki/Help:Contents]''
  
−
1. '''sequent''' A sequent.
+
==Reading==
 +
* [[Help:Navigation|Navigation]]
 +
* [[Help:Searching|Searching]]
 +
* [[Help:Tracking changes|Tracking changes]]
 +
* [[Help:Watchlist|Watchlist]]
  
−
2. '''rule''' A proof rule (possibly ''null'')
+
==Editing==
 +
* [[Help:Editing pages|Editing pages]]
 +
* [[Help:Starting a new page|Starting a new page]]
 +
* [[Help:Formatting|Formatting]]
 +
* [[Help:Links|Links]]
 +
* [[Help:User page|User pages]]
 +
* [[Help:Talk pages|Talk pages]]
  
−
3. '''children''' A list of proof tree nodes (possibly ''null'' or ''empty'').
+
===Advanced editing===
 +
* [[Help:Images|Images]]
 +
* [[Help:Tables|Tables]]
 +
* [[Help:Maths|Maths]]
 +
* [[Help:Categories|Categories]]
 +
* [[Help:Subpages|Subpages]]
 +
* [[Help:Managing files|Managing files]]
 +
* [[Help:Moving a page|Moving a page]]
 +
* [[Help:Redirects|Redirects]]
 +
* [[Help:Deleting a page|Deleting a page]]
 +
* [[Help:Protected pages|Protected pages]]
  
−
A proof tree is a proof tree node where its sequent corresponding to the proof obligation.
+
* [[Help:Templates|Templates]]
 +
* [[Help:Variables|Variables]]
 +
* [[Help:Namespaces|Namespaces]]
  
−
A proof tree node has different statuses:
+
* [[Help:Special pages|Special pages]]
 +
* [[Help:External searches|External searches]]
  
−
a. '''Pending''' No rule applied to this node, i.e. ''rule'' is ''null''. In this case, ''children'' must be ''null''.
+
===Personal customization===
 +
* [[Help:Preferences|Preferences]]
 +
* [[Help:Skins|Skins]]
  
−
b. '''Non-pending''' Has a rule applied to this node. In this case, ''children'' contains the list of child proof tree nodes.
+
==Wiki administration==
  
−
We now review the constraints on the proof trees, follows by different operations on the proof trees.
+
* [[Help:Sysops and permissions|Sysops and permissions]]
  
−
== Constraints on Proof Trees ==
+
The following features require extra permissions that are not normally granted to all wiki users.
−
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''
+
* [[Help:Protecting and unprotecting pages|Protecting and unprotecting pages]]
 +
* [[Help:Sysop deleting and undeleting|Sysop deleting and undeleting]]
 +
* [[Help:Patrolled edits|Patrolled edits]]
 +
* [[Help:Blocking users|Blocking users]]
 +
* [[Help:Range blocks|Range IP blocks]]
 +
* [[Help:Assigning permissions|Assigning permissions]]
  
−
A ''non-pending'' proof tree node is valid if:
+
[[Category:Help| ]]
−
 
+
__NOTOC__
−
* 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]]
 

Revision as of 09:19, 5 September 2008

Help copied from [1]

Reading

Editing

Advanced editing

Personal customization

Wiki administration

The following features require extra permissions that are not normally granted to all wiki users.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Proof_Trees&oldid=13315’