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.

Keywords

• tense logic
• sequent calculus
• indexation
• termination of derivation
• loop-check