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.