Restrictions for loop-check in sequent calculus for temporal logic with until operator
Articles
Adomas Birštunas
Vilnius University
Published 2009-12-20
https://doi.org/10.15388/LMR.2009.44
PDF

Keywords

sequent calculus
branchnig-time temporal logic
until operator
loop-check

How to Cite

Birštunas A. (2009) “Restrictions for loop-check in sequent calculus for temporal logic with until operator”, Lietuvos matematikos rinkinys, 50(proc. LMS), pp. 247–252. doi: 10.15388/LMR.2009.44.

Abstract

In this paper, we present sequent calculus for branching-time temporal logic with until operator. This sequent calculus uses efficient loop-checktechinque. We prove that we can use not all but only several special sequents from the derivation tree for the loop-check. We use indexes to discover these special sequents in the sequent calculus. These restrictions let us to get efficient decision procedure based on introduced sequent calculus.

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