caa a22 4500 463182723 CHVBK 20180406164843.0 cr unu---uuuuu 170326e20070401xx s 000 0 eng 10.1007/s10817-006-9055-9 doi (NATIONALLICENCE)springer-10.1007/s10817-006-9055-9 Liberalized Variable Splitting [Elektronische Daten] [Roger Antonsen, Arild Waaler] Variable splitting is a technique applicable to free variable tableaux, sequent calculi, and matrix characterizations that exploits a relationship between β- and γ-rules. Using contextual information to differentiate between occurrences of the same free variable in different branches, the technique admits conditions under which these occurrences may safely be assigned different values by substitutions. This article investigates a system of variable splitting and shows its consistency by a semantical argument. The splitting system is liberalized with respect to β-inferences analogously to a well-known liberalization of δ-rules, and this is used to show an exponential speedup compared to free variable systems without splitting. Springer Science+Business Media, Inc., 2007 connection method nationallicence tableau calculus nationallicence first-order logic nationallicence free variables nationallicence variable splitting nationallicence Antonsen Roger Department of Informatics, University of Oslo, Oslo, Norway aut Waaler Arild Department of Informatics, University of Oslo, Oslo, Norway aut Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 3-30 0168-7433 38:1-3<3 2007 38 10817 https://doi.org/10.1007/s10817-006-9055-9 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9055-9 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Antonsen Roger Department of Informatics, University of Oslo, Oslo, Norway aut NATIONALLICENCE 700 1- Waaler Arild Department of Informatics, University of Oslo, Oslo, Norway aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 3-30 0168-7433 38:1-3<3 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer