Infinitary Calculus without Loop Rules for Restricted Sequents of the First-Order Linear Temporal Logic

A restricted first-order linear temporal logic with temporal operators next and always is considered. We prove that for this logic one can construct a sequential calculus without loop rules, i.e., the rules containing a duplication of the main formula in the premises of these rules. This paper continues the previous work of the author, where an infinitary calculus without loop rules on the logical level, but containing the traditional loop antecedent rule for the operator always, was constructed. In this paper, in order to remove this loop rule we introduce a nonlocal rule allowing us to eliminate loops in the process of the proof search. The soundness and >-completeness of the constructed calculus is proved.