|
Записки научных семинаров ПОМИ, 1995, том 220, страницы 123–144
(Mi znsl4284)
|
|
|
|
Насыщенное исчисление для хорновских секвенций полной линейной темпоральной логики первого порядка
Регимантас Плюшкявичус Институт математики и информатики Академии наук Литвы
Аннотация:
Описано насыщенное исчисление для так называемых хорновских секвенций линейной темпоральной логики первого порядка. Насыщенное исчисление не содержит ни постулатов “индукционого” типа, ни правила сечения. Вместо постулатов “индукционного” типа насыщенное исчисление содержит конечное множество “насыщенных” секвенций, которое: (1) отражает периодическую структуру индуктивного рассуждения; (2) показывает, что “почти” ничего нового не может быть получено, продолжая поиск вывода данной секвенции; (3) явным образом позволяет строить так называемые “инвариантные” формулы в правилах индукционого типа. Насыщенное исчисление для хорновских секвенций позволяет: (1) доказать полноту линейной темпоральной логики первого порядка; (2) строить машинно-ориентированные алгоритмы поиска вывода; (3) доказать разрешимость этой логики для логически разрешимых хорновских секвенций. Библ. – 15 назв.
Поступило: 20.06.1994
Образец цитирования:
Регимантас Плюшкявичус, “Насыщенное исчисление для хорновских секвенций полной линейной темпоральной логики первого порядка”, Исследования по конструктивной математике и математической логике. IX, Зап. научн. сем. ПОМИ, 220, ПОМИ, СПб., 1995, 123–144; J. Math. Sci. (New York), 87:1 (1997), 3253–3266
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/znsl4284 https://www.mathnet.ru/rus/znsl/v220/p123
|
|