Method of marks for propositional linear temporal logic

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”.

Keywords

• sequent calculus
• loop-check
• temporal logics
• termination
• marks