Uniform Variable Splitting

Roger Antonsen
In Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), Cork, Ireland, 04 July – 08 July, 2004, volume 106, pages 1–5, CEUR Workshop Proceedings, 2004.
@InProceedings{Antonsen04,
  author =    {Roger Antonsen},
  title =     {Uniform {V}ariable {S}plitting},
  year =      2004,
  booktitle = {Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), Cork, Ireland, 04 July – 08 July, 2004},
  volume =    106,
  publisher = CEUR Workshop Proceedings},
  pages =     {1–5},
  issn =      {1613–0073},
  ee =        {http://ceur-ws.org/Vol-106/01-antonsen.pdf}
}

Abstract

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.