Generalised handling of variables in disconnection tableaux

Abstract

Recent years have seen a renewed interest in instantiation based theorem proving for first-order logic. The disconnection calculus is a successful approach of this kind, it integrates clause linking into a tableau guided proof procedure. In this paper we consider extensions of both the linking concept and the treatment of variables which are based on generalised notions of unifiability. These extensions result in significantly enhanced search space pruning and may permit the reduction of the length of refutations below Herbrand complexity which normally is a lower bound to the proof lengths of instantiation based methods. We present concise proofs of soundness and completeness of the new methods and show how these concepts relate to other instantiation based approaches.