Uniform variable splitting

ended 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

• Type: Conference
• Year: 2004
• Where: CADE
• Authors: Roger Antonsen
• Keywords: Automated Reasoning, CADE 2004, Free Variable Calculi, Uniform Variable Splitting, Variable Independence