Intertible infinitary calculus without loop rules for a restricted FTL

R. Pliuškevičius

Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part VII, Tome 293 (2002), pp. 149-180

Résumé

In the paper a fragment of first order linear time logic (with operators “next” and “always”) is considered. The object under investigation in this fragment is so-called $t$-$D$-sequents. For cosidered $t$-$D$-sequents invertible infinitary sequent calculus $G^+_\omega$ is constructed. This calculus has no loop rules, i.e. rules with duplications of a main formula in the premises of the rules. The calculus $G^+_\omega$ along with $\omega$-type rule for the temporal operator “always” contains an integrated separation rule $(IS)$ which includes the traditional loop-type rule $(\Box\to)$, a special rule $(\forall\to)$ (without duplication of a main formula) and traditional rule for the temporal operator “next”. The rule $(\to\exists)$ is incorporated in an axiom. The soundness and $\omega$-completeness of the constructed calculus $G^+_\omega$ are proved.