Open AccessMethod of marks for propositional linear temporal logic
Author(s) -
Regimantas Pliuškevičius
Publication year - 2014
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.a.2014.09
Subject(s) - axiom , linear temporal logic , computer science , loop (graph theory) , algorithm , classical logic , temporal logic , interval temporal logic , mathematics , theoretical computer science , programming language , combinatorics , geometry
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”.