Насыщенное исчисление для хорновских секвенций полной линейной темпоральной логики первого порядка

Описано насыщенное исчисление для так называемых хорновских секвенций линейной темпоральной логики первого порядка. Насыщенное исчисление не содержит ни постулатов “индукционого” типа, ни правила сечения. Вместо постулатов “индукционного” типа насыщенное исчисление содержит конечное множество “насыщенных” секвенций, которое: (1) отражает периодическую структуру индуктивного рассуждения; (2) показывает, что “почти” ничего нового не может быть получено, продолжая поиск вывода данной секвенции; (3) явным образом позволяет строить так называемые “инвариантные” формулы в правилах индукционого типа. Насыщенное исчисление для хорновских секвенций позволяет: (1) доказать полноту линейной темпоральной логики первого порядка; (2) строить машинно-ориентированные алгоритмы поиска вывода; (3) доказать разрешимость этой логики для логически разрешимых хорновских секвенций. Библ. – 15 назв.