@article {IOPORT.06014273,
    author       = {Kamide, Norihiro},
    title        = {Bounded linear-time temporal logic: a proof-theoretic investigation.},
    year         = {2012},
    journal      = {Annals of Pure and Applied Logic},
    volume       = {163},
    number       = {4},
    issn         = {0168-0072},
    pages        = {439-466},
    publisher    = {Elsevier Science B.V. (North-Holland), Amsterdam},
    doi          = {10.1016/j.apal.2011.12.002},
    abstract     = {Summary: 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 the 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.},
    identifier   = {06014273},
}