Some techniques for branch-saturation in free-variable tableaux

Abstract

We present a free-variable tableaux calculus that avoids the systematic instantiation of universally quantified variables by ground terms, but still permits branch-saturation (i.e. no backtracking on the applied substitutions is needed). We prove that our calculus is sound, refutationally complete, and that it is a decision procedure for function-free skolemized formulae (Bernays-Schönfinkel class). Comparison with existing works are provided, showing evidence of the interest of our approach.