| Abstract: | An infinitary calculus for a restricted fragment of the first-order linear temporal logic is considered. We prove that for this fragment one can construct the infinitary calculusG Lω * without contraction on predicate formulas. The calculusG Lω * possesses the following properties: (1) the succedent rule for the existential quantifier is included into the corresponding axiom; (2) the premise of the antecedent rule for the universal quantifier does not contain a duplicate of the main formula. The soundness and completness ofG Lω * are also proved. Institute of Mathematics and Informatics, Akademijos 4, 2600 Vilnius, Lithuania. Translated from Lietuvos Matematikos Rinkinys, Vol. 39, No. 3, pp. 378–397, July–September, 1999. Translated by R. Lapinskas |
