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.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Please read the Copyright Notice in Journal Policy.