| Title |
Cut, invariant rule, and loop-check free sequent calculus for PLTL / |
| Translation of Title |
Sekvencinis skaičiavimas be pjūvio, invariantinės taisyklės ir ciklų tikrinimo tiesinio laiko teiginių logikai. |
| Authors |
Alonderis, Romas ; Pliuškevičius, Regimantas Ričardas |
| DOI |
10.15388/LMR.2011.ml02 |
| Full Text |
|
| Is Part of |
Lietuvos matematikos rinkinys. LMD darbai.. Vilnius : Matematikos ir informatikos institutas. 2011, t. 52, p. 231-236.. ISSN 0132-2818 |
| Keywords [eng] |
Decision procedure ; Sequent calculus ; Loop-check ; Temporal logics ; Termination |
| Abstract [eng] |
In this paper, some loop-check free saturation-like decision procedure is proposed for propositional linear temporal logic (PLTL) with temporal operators “next” and “always”. This saturation procedure terminates when special type sequents are obtained. Properties of PLTL allows us to construct backtracking-free decision procedure without histories and loop-check. |
| Published |
Vilnius : Matematikos ir informatikos institutas |
| Type |
Journal article |
| Language |
English |
| Publication date |
2011 |
| CC license |
|
