Bounded linear-time temporal logic: A proof-theoretic investigation

Citations of this article
Mendeley users who have this article in their library.


Propositional and first-order bounded linear-time temporal logics (BLTL and FBLTL, respectively) are introduced by restricting Gentzen type sequent calculi for linear-time temporal logics. The corresponding Robinson type resolution calculi, RC and FRC for BLTL and FBLTL respectively are obtained. To prove the equivalence between FRC and FBLTL, a temporal version of Herbrand theorem is used. The completeness theorems for BLTL and FBLTL are proved for simple semantics with both a bounded time domain and some bounded valuation conditions on temporal operators. The cut-elimination theorems for BLTL and FBLTL are also proved using some theorems for embedding BLTL and FBLTL into propositional (first-order, respectively) classical logic. Although FBLTL is undecidable, its monadic fragment is shown to be decidable. © 2011 Elsevier B.V.




Kamide, N. (2012). Bounded linear-time temporal logic: A proof-theoretic investigation. Annals of Pure and Applied Logic, 163(4), 439–466.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free