It is known that linear-time temporal logic (LTL), which is an extension of Such a theoretical merit may not be obtained for an unbounded and intuitionistic version of LTL, because the unbounded time domain requires some infinite inference rules. Such infinite inference rules are neither familiar to nor welcomed by researchers who study automated reasoning, since these rules cannot be implemented efficiently. Indeed, the replacement of such infinite rules of certain proof systems by finitary rules is known as an important issue. It is also known that to restrict the time domain is a technique that may be applied to obtain a decidable or efficient fragment of LTL. IB[ l ] and PB[ l ] may provide a good proof-theoretical basis for such practical applications as well as a good tool for automated reasoning with (bounded) linear-time formalisms. Information represented by ltr"
