Method of marks for propositional linear temporal logic
Articles
Regimantas Pliuškevičius
Vilnius University
Published 2014-12-15
https://doi.org/10.15388/LMR.A.2014.09
PDF

Keywords

sequent calculus
loop-check
temporal logics
termination
marks

How to Cite

Pliuškevičius R. (2014) “Method of marks for propositional linear temporal logic”, Lietuvos matematikos rinkinys, 55(A), pp. 46–50. doi: 10.15388/LMR.A.2014.09.

Abstract

It is known that traditional techniques used to ensure termination of a decision procedure in non-classical logics are based on loop-checking, in general. Nowadays, effective loop-check techniques based on histories are used instead of unrestricted loop-check. These techniques are widely and successfully applied also for non-classical logics containing induction-like axioms. These induction-like axioms create new type loops (“good loops”) along with ordinary “bad loops”. In this paper, some loop-check free saturation-like decision procedure based on some technique of marks is proposed. This saturation procedure terminates when special type marked sequents are obtained. This procedure is demonstrated for propositional linear temporal logic (PLTL) with temporal operators “next” and “always”.

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