Termination of derivations for minimal tense logic

Abstract

It is known that loop checking and backtracking are extensively used in various non-classical logics. An efficient loop checking is obtained using a technique based on histories. In the paper a method for elimination of loop checking in backward proof search for minimal tense logic Kt is proposed. To obtain termination of derivation indices and marks are used instead of history.