A labeled sequent calculus LSC for propositional linear discrete time logic PLTL is introduced. Its sub-calculus LSC−TL is proved to be complete for some class of PLTL sequents.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Please read the Copyright Notice in Journal Policy.