Аналитико-табличная формализация систем временной логики

• Автор: Григорьев, Олег Михайлович
• Шифр специальности: 09.00.07
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Москва
• Количество страниц: 115 с.

Введение
1 Аналитические таблицы для логических систем с модальностями различные подходы к построению

1 Родственные методы и история возникновения.

2 Аналитические таблицы

2 Аналитикотабличпая формализация стандартных систем временной логики

1 Стандартные прайоровские системы

временной логики.

2 Аналитические таблицы и свойства шкал Крипке

3 Аналитические таблицы для временной

системы Кь.

4 Непротиворечивость и полнота

системы ТК1.
5 Аналитические таблицы для расширений
времсппой системы Кг .
6 Аналитпкотабличные формализации систем временной ло
гики с нестандартным отношением между прошлым и будущим
Заключение
Введение


В контексте исследования по аналитическим таблицам нельзя обойти стороной такую область, как построение исчислений генценовского типа для модальных и временных логик. Ранние работы в этой области можно рассматривать как предшествующие появлению аналитикотабличных формализаций. Генценовские исчисления для наиболее из вестных систем нормальной модальной логики К, Т, 4 и 5, появились в х годах XX века. Одной из первых работ по этой тематике является статья X. Карри года. Далее последовали работы М. Опиши и К. Мацумото, в которых развивались полученные Карри результаты. Впоследствии статьи на эту тему время от времени появлялись в литературе. Упомянем здесь таких авторов, как К. Дошен, Г. Вансинг, А. Аврон. Секвенциальные исчисления с префиксированными формулами для рада стандартных систем временной логики были построены австралийскими логиками Р. Горб и Н. Боннетт 9,. Среди российских логиков свой вклад в разработку секвенциальных исчислений для модальной логики внесли Г. Е. Минц, О. Ф. Серебрянников, П. И. Быстров и др. В последнее время появились работы, в которых предлагается ряд технических усовершенствований, позволяющих улучшить алгоритмические характеристики аналитических таблиц и преодолеть отставание в отношении конкурирующих методов например, процедура енмплификацпи представленная в работах , , , работающая в аналитикотабличных вариантах классической пропозициональной и модальной логик, дает возможность рассматривать с единой точки зрения различные исчисления, лежащие в основе систем автоматического поиска вывода, такие как , КЕ, , ВСР, , гипертаблицы. В ряде исследований предлагаются также комбинированные методы аналитические таблицы в сочетании с теоретикоигровым подходом , , средствами теории автоматов 5, элементами проверки модели i . Заметим еще раз, что, вообще говоря, аналитические таблицы не обязательно используются только как разрешающая процедура. Ничто не мешает использовать метод и для неразрешимых систем, как например, первопорядковой классической логики. В таком случае речь идет о полуразрешающей процедуре. Метод аналитических таблиц очень успешно применяется в классических модальных логиках, в ряде систем временных логик вычислимости, в комбинированных логиках с временным измерением. Однако, под одним названием скрываются, на самом деле, далеко не одпородпые методы. Нередко оказывается, что для нового класса логических систем требуется придумывать и совершенно новый подход. Причины этого лежат в существенных семантических различиях логик, а аналитические таблицы тесно связаны с семантикой в первую очередь. С другой стороны, табличные алгоритмы, разработанные для временных логик, интересных с точки зрения компьютерных наук, также оказываются не подходящими для других систем временной логики. Найти простой и естественный подход к построению аналитических таблиц, который был бы как можно более адаптивным и в то же время обладал удобством в применении и практической значимостью важная и интересная, на наш взгляд, задача. Целью диссертационного исследования является решение проблемы разработки аналитикотабличных исчислений для стандартных прайоровских систем временной логики и систем с нестандартным отношением между прошлым и будущим. Требуемыми характеристиками исчислений являются максимальная понятность правил и простота в применении. В то же время основная идея, используемая при иосгроении формализаций, должна позволять адаптировать совокупносгь правил редукции для различных логических систем с минимальными изменениями. Диализ различных подходов к построению аналитикотабличных формализаций систем модальной и временной логики с целью выявления их сильных и слабых сторон. Последующее нахождение наиболее общего метода, применимого при разработке аналитических таблиц для широкого класса стандартных систем временных логик. Детальное описание метода. Формулировка правил редукции для наиболее известных систем времсиной логики. Доказательство непротиворечивости и полноты построенных аналитикотабличных формализаций. Формулировка правил редукции для систем временной логики с нестандартным отношением сопряженности между прошлым и будущим.