Efficient loop-check for backward proof search in some non-classical propositional logics

Abstract

We consider the modal logics KT and S4, the tense logic Kt, and the fragment IPC(⋀, →) of intuitionistic logic. For these logics backward proof search in the standard sequent or tableau calculi does not terminate in general. In terms of the respective Kripke semantics, there are several kinds of non-termination: loops inside a world (KT), infinite resp. looping branches (S4, IPC(⋀, →)), and infinite branching degree (Kt). We give uniform sequent-based calculi that contain specifically tailored loop-checks such that the efficiency of proof search is not deteriorated. Moreover all these loop-checks are easy to implement and can be combined with optimizations. Note that our calculus for S4 is not a pure contraction-free sequent calculus, but this (theoretical) defect does not hinder its application in practice.