The underlying engine contains a backtracking procedure which is turned on as soon as a
closed node is found and as soon as no rule is applicable to a node.
Each of the three forms of non-determinism give rise to And-branching.
That is:
- choosing different current nodes will give rise to different tableaux;
- choosing different rules to apply to the current node will give rise to different tableaux;
- choosing different principal formulae for the chosen rule and the chosen node will give rise to
different tableaux.
But we need only one of these tableaux to close.
Thus we have the following backtracking principle:
backtrack over all choice points until we find a tableau such that each And-node has at least one closed
child and each Or-node has all children closed.
At any stage, if the backtracking algorithm finds a closed tableau, then it stop backtracking
and simply returns closed.
Conversely, as long as it fails to find a closed tableau, it continues to backtrack over all
choice points.
Thus, on the way down, strategies tell us how to construct the current tableau and how to
leave And- and Or- choice points in creating the tableau.
During backtracking, some of these choice-points are activated, as long as we have not found
a closed tableau.
Comments
I would not put in these terms.
The twb has no backtracking procedure that is turned on when something happen. The visit algorithm simply looks for a tableau that respects all conditions associated to rules and the stategy. In principle, if all these conditions are left unspecified (that is we use only ||| both in the strategy and in the rule definitions) there will be no backtracking going on as the procedure will explore all branches of all trees. I say in principle as this is not implemented as does not make sense in my head.
If we consider only binary trees (open/closed trees) then we are basically instantiating these considitions to match the semantic of tableau (or sequents).
Since branching, both in the strategy and in the rules, is guarded by these conditions, the end result will alwyas be the first result that respects all the conditions. This result will be the generated by the search of a tree, but this tree will be left implicit in the recursion.
I think it's misleading to let the user think that these trees are tangible objects, as they have no mean to manipulate them at a global level. The can only look at the from a local/rule level. If you want to save the tree in a separate data structure and then do something with it, this is a different problem.