Uniform variable splitting.
Roger Antonsen · 2004
This extended abstract motivates and presents techniques for identifying variable independence in free variable calculi for classical logic without equality. Two variables are called independent when it is sound to instantiate them differently. The goal of the uniform variable splitting technique, first presented in [14], is to label variables differently (modulo a set of equations) exactly when they are variable independent. The overall motivation is to have a calculus which simultaneously has: (1) invariance under order of rule application (to enable goal-directed search, since rules then can be applied in any order), (2) introduction of free variables instead of arbitrary terms (to reduce the instantiation problem to a unification problem), and (3) a branchwise restriction of the search space (to allow branchwise termination criteria and early termination in cases of unprovability). Following the notation of Smullyan [11], both formulae and inferences will have type , , or . A -inference always has a principal formula of type ; atomic formulae have no type.