Termination of derivations for minimal tense logic
Articles
Regimantas Pliuškevičius
Institute of Mathematics and Informatics
Published 2009-12-20
https://doi.org/10.15388/LMR.2009.47
PDF

Keywords

tense logic
sequent calculus
indexation
termination of derivation
loop-check

How to Cite

Pliuškevičius R. (2009) “Termination of derivations for minimal tense logic”, Lietuvos matematikos rinkinys, 50(proc. LMS), pp. 264–268. doi: 10.15388/LMR.2009.47.

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.

PDF
Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Please read the Copyright Notice in Journal Policy