Intertible infinitary calculus without loop rules for a restricted FTL

В статье рассматривается фрагмент линейной временной логики первого порядка с операторами “следующий” и “всегда”. Объектами рассмотрения в этом фрагменте являются секвенции специального вида – $t$-$D$-секвенции. Для $t$-$D$-секвенций построено обратимое секвенциальное исчисление $G_\omega^+$, не содержащее циклических правил, т.е. посылки правил этого исчисления не содержат дублирования главной формулы рассматриваемого правила. Исчисление $G_\omega^+$ содержит только два правила: $\omega$-правило для оператора “всегда” и интегрированное правило отделения $(IS)$. Это правило включает традиционное антецедентное (циклического типа) правило для оператора “всегда”, специальное (нециклическое) правило $(\forall\to)$ и традиционное правило для оператора “следующий”. Правило $(\to\exists)$ содержится в аксиоме исчисления $G_\omega^+$. Доказана корректность и $\omega$-полнота исчисления $G_\omega^+$. Библ. – 43 назв.