Abstract
Variable splitting is a recently introduced tableau technique for first order logic. It aims to identify when different occurrences of the same variable are independent and thus need not be treated as rigid. By removing the interdependency between universal and branching inferences that normally exists in LK-style tableaux it allows for greater freedom in the formulation of heuristics for proof search. This can potentially give rise to a significant improvement
in automated reasoning.
In this thesis I give two contributions to the theory of variable splitting. First, I show that determining if a solution to an equation set with variable splitting is NP-complete. In contrast, the situation without splitting is that linear algorithms exist. This is significant because such equation sets is one of the most important contributors to the run time of a tableaux prover. Second, I characterise a main concept, maximality of splitting relations, and use this concept to sketch a naive proof search algorithm.