Removing Non-Determinism

A ''don't care'' non-deterministic choice is an arbitrary choice of one among multiple possible continuations for a computation, all of which return the same result. A ''don't know'' non-deterministic choice is one choice among multiple possible continuations, which do not necessarily return the same result. For completeness in a tableau calculus, it is sufficient to assume that all choices are ''don't know'' non-deterministic. However, a deterministic algorithm based on this assumption will be extremely inefficient since it has to consider all possible continuations for all choices. Thus it is imperative to remove as many forms of non-determinism as possible. Traditionally, logicians focus on the existence of a derivation tree rather than on how it is found. Conversely, automated reasoners focus on designing algorithms to search for a derivation tree as efficiently as possible. From a theoretical perspective, it is therefore not important to specify the order in which rules are applied or how the proof tree is explored. Practically, however, specifying a particular rule order can dramatically speed up the search and construction of a proof tree. Moreover, since different rule orders can produce different derivation trees, an efficient decision procedure should always try to build the smallest derivation tree. In general, we can identify three forms of non-determinism associated with three fundamental aspects of a generic decision procedure: *Node-choice: the algorithm chooses which leaf becomes the current node; *Rule-choice: the algorithm chooses which rule to apply to the current node; *Instance-choice: the algorithm chooses which formula to make the principal formula for the chosen rule and the chosen current node. That is, it determines the order in which to explore the different instantiations (partitions) of the current node created by the chosen rule. ==Node-choice== The first source of non-determinism is which (leaf) node to select as the current node and is usually handled by a visit algorithm that selects this node out of possibly many in the current tree. For exposition, we use a depth first visit function that deterministically selects the left most node, but our algorithm allows any visit strategy to be used to explore the search space (ie. breadth-first). ==Rule-choice== The second source of non-determinism in tableau methods arises from the lack of guidance when applying logical rules. If a node contains many different formulae, then many rules may be applicable to that node. How to choose? For example, in classical propositional logic, where all rules are invertible, the order in which rules are applied is not important. However specifying a strategy that applies all linear rules and the axiom first, and then all branching rules, can potentially shorten the proof tree. The problem is however different in basic modal logic, where not all sequences of rule applications ensure a solution since the (K)-rule is not invertible. The problem is even more complicated in tableau-sequent calculi with more than one non-invertible rule: for example intuitionistic logic. In this situation, at any given choice point, after all invertible rules are applied, we are forced to guess which non-invertible rule to apply, and eventually to undo this decision if it does not lead to the construction of an acceptable proof tree. Consequently, if the proof tree obtained from the application of the first rule of a sequence of non-invertible rules does not respect a logic-specific condition, the entire proof tree generated from that rule application must be discarded. To recover from this wrong choice, the proof must be re-started using the next non-invertible rule available in the sequence. Thus, for efficiency, tableau rules must be coupled with a ''strategy'' to control the order in which rules are applied. ==Instance-choice== The third form of non-determinism is the aforementioned choice of one rule instance (partition) of the current node from potentially many rule instances (partitions) of the current node. Then, this nondeterminism can be resolved by using optimisation techniques based on logic-specific considerations used to reduce the size of the search space. For example, if the chosen rule is an Or-rule, heuristics such as MOMS (Maximum number of Occurrences in disjunctions of Minimum Size) or iMOMS (inverted MOMS) order the disjunctions (formulae) in the node to always choose the less/more constrained disjunct, which, in principle, should lead to an earlier clash.