Содержание к диссертации
Введение
Аналитические таблицы для логических систем с модальностями: различные подходы к построению 10
1 Родственные методы и история возникновения 10
2 Аналитические таблицы 15
Аналитико-табличная формализация стандартных систем временной логики 37
1 Стандартные (прайоровские) системы временной логики 37
2 Аналитические таблицы и свойства шкал Крипке 40
3 Аналитические таблицы для временной системы Kt 44
4 Непротиворечивость и полнота системы TKt 49
5 Аналитические таблицы для расширений временной системы Kt 86
6 Аналитико-табличные формализации систем временной логики с нестандартным отношением между прошлым и будущим 101
Заключение 106
- Родственные методы и история возникновения
- Стандартные (прайоровские) системы временной логики
- Аналитические таблицы для временной системы Kt
- Аналитико-табличные формализации систем временной логики с нестандартным отношением между прошлым и будущим
Введение к работе
Временная логика является одной из наиболее интенсивно изучаемых областей современной символической логики. Первоначально интерес к ней был вызван философскими проблемами, связанными с интерпретацией высказываний с временными модальностями. Толчок к развитию временной логики дали работы Артура Прайора [51, 52]. Временная логика явила собой мощный инструмент для формализации рассуждений в рамках различных концепций времени. Ей также нашлось применение в лингвистике, для анализа языковых контекстов с временными модальностями. В математической логике активно исследовались выразительные свойства языков с временными модальностями, отношения классической и модальной, в том числе и временной, логик. Изучались свойства семантических структур для модальных и временных логик.
В дальнейшем, с развитием компьютерного знания, возникла необходимость в разработке формализмов, позволяющих описывать вычислительные процессы и работу разнообразных вычислительных устройств. Поскольку временной параметр есть часть характеристики любого процесса, высказывания с временными модальностями, как правило, присутствуют в его описании. В результате временная логика стала привлекать внимание специалистов из области компьютерных наук и развиваться как прикладная дисциплина. Ее задачами стали верификация и спецификация программ и оборудования (hardware), анализ параллельных процессов, представление знания и передача информации, оптимизация работы компьютерных сетей и многое другое. В настоящее время логика с временными модальностями утвердилась как мощное и эффективное средство для решения перечисленных задач.
Среди наиболее важных и интересных проблем, встающих при изучении логических систем, выделяется проблема разрешимости и разработки разрешающих и полуразрешающих процедур. Эффективность понятия логического закона есть свойство, наличие или отсутствие которого является фундаментальной характеристикой любой логической системы. В связи с интенсивным развитием прикладной логики, проблема разрешимости и нахождения разрешающих алгоритмов приобрела еще и практическое измерение. Логики, ориентированные на прикладные аспекты, предназначены для описания определенных процессов или систем объектов, и здесь важно знать, выполняется ли формула в данной модели или нет. Здесь же, в дополнение к проблеме собственно разрешимости, добавляется и проблема сложности разрешающей процедуры. Если в чисто теоретическом аспекте мы игнорируем ограничения на вычислительные ресурсы, то с точки зрения приложений, мы ограничены ресурсами вычислительных устройств, реализующих нашу процедуру, даже если это абстрактные вычислительные машины. Традиционно принимаются ограничения на память и время работы вычислительного устройства.
Одной из конкретных реализаций разрешающей или полуразрешающей процедуры для логических систем является метод аналитических таблиц. Этот метод известен достаточно давно, он получил широкое применение начиная с классической работы Р. Смаллиана "First Order Logic" (1969). Часто бывает так, что удается доказать разрешимость некоторой логики, но построить формализм, который выступал бы как разрешающая процедура оказывается сложным. И именно аналитические таблицы, на наш взгляд, стали наиболее употребительным методом при разработке разрешающих и полуразрешающих алгоритмов.
В последнее время заметно увеличилось количество работ, посвященных построению аналитико-табличных формализации разнообразных логических систем. Это связано с тем, что возникает потребность в разработке логик на основе богатых в выразительном отношении языков, на базе сложно устроенных семантических структур. Ярким примером выступают исследования в области комбинированных и многомерных модальных логик.
Нацеленность компьютерных наук на прикладные аспекты привела к двоякому результату. С одной стороны, язык временной логики обогатился разнообразными модальными операторами, что дает возможность выражать всевозможные свойства временного потока. С другой стороны, интерес исследователей часто ограничивается лишь теми логиками, которые описывают традиционно принимаемые в компьютерных науках характеристики времени — дискретность, наличие начального момента, линейность и т.д. При этом модальности прошлого обычно не принимаются во внимание. Поэтому классические временные логики прайо-ровского типа оказались как бы в тени и реже привлекают внимание специалистов. Тем не менее они являются мощным инструментом для изучения разнообразных интересных моделей времени с широким спектром свойств.
Отметим еще одну тенденцию, связанную с развитием временной логики. Это построение и изучение комбинированных логик. С семантической точки зрения такие логики возникают в результате операций над модельными структурами. Наиболее стандартный способ — перемножение реляционных структур. Участие в таких составных логиках временных модальностей стало обычным явлением. Логики подобного типа находят широкое применение в области разработок по искусственному интеллекту. Литература по этой теме весьма обширна (см., например [17, 18, 53, 58]).
Таким образом, временная логика сегодня — это великое множество различных непохожих друг на друга систем, возникающих как из практических нужд, так и из чистого теоретического интереса. Естественно, что традиционные метатеоретические вопросы, которые обычно ставятся по поводу любой логики, появляются также и в случае временных логик.
Известно, что существуют по меньшей мере два пути к построению логики (здесь логика понимается в узком смысле слова, как совокупность выражений фиксированного языка, замкнутая относительно некоторой совокупности правил вывода). При синтаксическом подходе стремятся получить систему дедуктивных постулатов, например, множество акси-
ом и правил вывода, основных секвенций и фигур заключения и т.п. Семантический поход предполагает, что изначально имеется класс модельных структур и вопрос стоит о множестве законов и корректных способов рассуждений, определяемых этим классом. Этот путь исторически является несколько более молодым, чем первый подход (теоретико-множественная семантика для классической логики предикатов сформировалась в 30-е годы XX века в работах Тарского, теория моделей, как самостоятельная дисциплина, стала осознаваться в 50-е годы благодаря работам Генкина, Тарского, Робинсона и др.). Нам представляется, что аналитические таблицы в этом контексте являют собой уникальное средство, которое сочетает в себе черты как методов теории доказательств, так и методы теории моделей. Семантическая информация (истинностная оценка формул, отношение достижимости в реляционных моделях) может в той или иной степени присутствовать непосредственно в правилах редукции, которые как раз и составляют класс дедуктивных постулатов аналитико-табличного исчисления. В силу этого обстоятельства, аналитические таблицы являются чрезвычайно гибким — в отношении адаптации к различным логическим системам — и максимально удобным с практической точки зрения методом.
Одной из первых работ, в которых метод аналитических таблиц стал применяться к модальным логикам, является монография Мелвина Фит-тинга "Intuitionistic Model Theory and Forcing". Здесь было сформулировано аналитико-табличное исчисление для модальной системы S4. В 1972 году Фиттинг опубликовал статью, в которой были представлены аналитико-табличные исчисления для ряда известных модальных систем. В этой статье был использован метод префиксированных формул, который затем стал широко употребительным при построении анали-тико-табличных формализации неклассических логик. В 1983 году вышла большая монография этого же автора, посвященная теории доказательств в модальной и интуиционистской логиках.
Метод таблиц с префиксированными формулами получил развитие в работах таких авторов, как Ф. Массаччи, Р. Горе, Б. Беккерт, Г. Го-вернатори, А. Артози и многих других. В ряде статей Беккерта и Горе
реализована идея префиксов, содержащих переменные, заменяемые произвольными префиксами. Это позволяет применять метод унификации для нахождения замкнутых ветвей в таблице. Особо выделяется подход Массаччи-Горё, связанный с разработкой так называемых «одношаго-вых» префиксных аналитических таблиц (single step analytic tableaux). Преимущество этого метода в том, что получаемые аналитико-таблич-ные исчисления обладают свойством модулярности. Другими словами, существует базисное минимальное аналитико-табличное исчисление, обозначаемое как ТК, а каждое его расширение получается путем добавления характеристических правил. Помимо этого, правила предельно просты, легко просматривается связь с семантикой. В 1999 году вышел объемный "Handbook of Tableaux Methods", в котором обобщены разработки в области построения аналитических таблиц для классической и неклассической логики. Раздел о табличных процедурах в модальной и временной логиках написан крупнейшим специалистом этого направления, австралийским логиком Р. Горе.
Среди отечественных работ следует отметить книгу А. Т. Ишмурато-ва «Логический анализ временных контекстов», в которой автор предлагает вариант построения аналитических таблиц для временной системы Kt. Особенностью подхода является то, что конструкцию аналитической таблицы сопровождает граф, изображающий отношение достижимости в модели Крипке.
В контексте исследования по аналитическим таблицам нельзя обойти стороной такую область, как построение исчислений генценовского типа для модальных и временных логик. Ранние работы в этой области можно рассматривать как предшествующие появлению аналитико-табличных формализации. Геиценовские исчисления для наиболее известных систем нормальной модальной логики К, Т, S4 и S5, появились в 50-х годах XX века. Одной из первых работ по этой тематике является статья X. Карри 1952 года. Далее последовали работы М. Ониши и К. Мацумото, в которых развивались полученные Карри результаты. Впоследствии статьи на эту тему время от времени появлялись в литературе. В конце XX столетия наметился определенный всплеск интереса
к построению формализмов генценовского типа для модальных логик. Упомянем здесь таких авторов, как К. Дошен, Г. Вансинг, А. Аврон. Секвенциальные исчисления с префиксированными формулами для ряда стандартных систем временной логики были построены австралийскими логиками Р. Горе и Н. Боннетт [9, 10].
Среди российских логиков свой вклад в разработку секвенциальных исчислений для модальной логики внесли Г. Е. Минц, О. Ф. Серебрянников, П. И. Быстрой и др.
В последнее время появились работы, в которых предлагается ряд технических усовершенствований, позволяющих улучшить алгоритмические характеристики аналитических таблиц и преодолеть «отставание» в отношении конкурирующих методов (например, процедура симплифи-кацвпаг представленная в работах [42, 43, 44], работающая в аналитико-табличных вариантах классической пропозициональной и модальной логик, дает возможность рассматривать с единой точки зрения различные исчисления, лежащие в основе систем автоматического поиска вывода, такие как DPLL, КЕ, HARP, ВСР, KSAT, гипер-таблицы). В ряде исследований предлагаются также комбинированные методы — аналитические таблицы в сочетании с теоретико-игровым подходом [34, 35], средствами теории автоматов [5], элементами проверки модели (model-checking) [23]. Заметим еще раз, что, вообще говоря, аналитические таблицы не обязательно используются только как разрешающая процедура. Ничто не мешает использовать метод и для неразрешимых систем, как например, первопорядковой классической логики. В таком случае речь идет о полуразрешающей процедуре.
Метод аналитических таблиц очень успешно применяется в классических модальных логиках, в ряде систем временных логик вычислимости, в комбинированных логиках с временным измерением. Однако, под одним названием скрываются, на самом деле, далеко не однородные методы. Нередко оказывается, что для нового класса логических систем требуется придумывать и совершенно новый подход. Причины этого лежат в существенных семантических различиях логик, а аналитические таблицы тесно связаны с семантикой в первую очередь. Так, если пы-
таться адаптировать для прайоровских систем временной логики метод таблиц с префиксированными формулами, прекрасно работающий в модальной логике, то возникают немалые технические трудности. С другой стороны, табличные алгоритмы, разработанные для временных логик, интересных с точки зрения компьютерных наук, также оказываются не подходящими для других систем временной логики. Найти простой и естественный подход к построению аналитических таблиц, который был бы как можно более адаптивным и в то же время обладал удобством в применении и практической значимостью — важная и интересная, на наш взгляд, задача.
Целью диссертационного исследования является решение проблемы разработки аиалитико-табличных исчислений для стандартных прайоровских систем временной логики и систем с нестандартным отношением между прошлым и будущим. Требуемыми характеристиками исчислений являются максимальная понятность правил и простота в применении. В то же время основная идея, используемая при построении формализации, должна позволять адаптировать совокупность правил редукции для различных логических систем с минимальными изменениями. Для достижения указанных целей, в ходе диссертационного исследования, решались следующие задачи:
Анализ различных подходов к построению аналитико-табличиых формализации систем модальной и временной логики с целью выявления их сильных и слабых сторон. Последующее нахождение наиболее общего метода, применимого при разработке аналитических таблиц для широкого класса стандартных систем временных логик. Детальное описание метода.
Формулировка правил редукции для наиболее известных систем временной логики. Доказательство непротиворечивости и полноты построенных аналитико-табличных формализации.
Формулировка правил редукции для систем временной логики с нестандартным отношением сопряженности между прошлым и будущим.
В ходе проведенной работы были получены следующие результаты:
Разработан общий метод построения аналитико-табличных исчислений для систем временной логики, позволяющий охватить широкий класс известных логических систем при незначительных модификациях совокупности правил редукции. Фактически имеется минимальная совокупность правил редукции, непротиворечивая и полная относительно класса всех временных шкал Крипке, то есть аналог системы Kt. Добавочные правила редукции позволяют получить расширения минимальной системы. При этом правила редукции для логических связок, включая модальности, остаются общими для всех систем.
Построены аналитико-табличные варианты известных систем временной логики — минимальной системы Kt ряда ее расширений: логики транзитивного (Kt.4), линейного, плотного и бесконечного времени.
Доказаны теоремы об адекватности предложенных аналитико-табличных исчислений.
Построены аналитико-табличные формализации некоторых логик времени с нестандартным отношением сопряженности прошлого и будущего.
Аналитико-табличные процедуры часто являются основой для создания компьютерных программ для автоматического поиска доказательства. Эта сфера исследований стала чрезвычайно важной в связи с развитием компьютерной техники и соответствующей теоретической дисциплины. Автоматические методы рассуждения на базе временных логик применяются при описании вычислительных процессов, верификации и спецификации программ, в сфере криптографии.
Родственные методы и история возникновения
Метод таблиц с префиксированными формулами получил развитие в работах таких авторов, как Ф. Массаччи, Р. Горе, Б. Беккерт, Г. Го-вернатори, А. Артози и многих других. В ряде статей Беккерта и Горе реализована идея префиксов, содержащих переменные, заменяемые произвольными префиксами. Это позволяет применять метод унификации для нахождения замкнутых ветвей в таблице. Особо выделяется подход Массаччи-Горё, связанный с разработкой так называемых «одношаго-вых» префиксных аналитических таблиц (single step analytic tableaux). Преимущество этого метода в том, что получаемые аналитико-таблич-ные исчисления обладают свойством модулярности. Другими словами, существует базисное минимальное аналитико-табличное исчисление, обозначаемое как ТК, а каждое его расширение получается путем добавления характеристических правил. Помимо этого, правила предельно просты, легко просматривается связь с семантикой. В 1999 году вышел объемный "Handbook of Tableaux Methods", в котором обобщены разработки в области построения аналитических таблиц для классической и неклассической логики. Раздел о табличных процедурах в модальной и временной логиках написан крупнейшим специалистом этого направления, австралийским логиком Р. Горе.
Среди отечественных работ следует отметить книгу А. Т. Ишмурато-ва «Логический анализ временных контекстов», в которой автор предлагает вариант построения аналитических таблиц для временной системы Kt. Особенностью подхода является то, что конструкцию аналитической таблицы сопровождает граф, изображающий отношение достижимости в модели Крипке.
В контексте исследования по аналитическим таблицам нельзя обойти стороной такую область, как построение исчислений генценовского типа для модальных и временных логик. Ранние работы в этой области можно рассматривать как предшествующие появлению аналитико-табличных формализации. Геиценовские исчисления для наиболее известных систем нормальной модальной логики К, Т, S4 и S5, появились в 50-х годах XX века. Одной из первых работ по этой тематике является статья X. Карри 1952 года. Далее последовали работы М. Ониши и К. Мацумото, в которых развивались полученные Карри результаты. Впоследствии статьи на эту тему время от времени появлялись в литературе. В конце XX столетия наметился определенный всплеск интереса к построению формализмов генценовского типа для модальных логик. Упомянем здесь таких авторов, как К. Дошен, Г. Вансинг, А. Аврон. Секвенциальные исчисления с префиксированными формулами для ряда стандартных систем временной логики были построены австралийскими логиками Р. Горе и Н. Боннетт [9, 10].
Среди российских логиков свой вклад в разработку секвенциальных исчислений для модальной логики внесли Г. Е. Минц, О. Ф. Серебрянников, П. И. Быстрой и др.
В последнее время появились работы, в которых предлагается ряд технических усовершенствований, позволяющих улучшить алгоритмические характеристики аналитических таблиц и преодолеть «отставание» в отношении конкурирующих методов (например, процедура симплифи-кацвпаг представленная в работах [42, 43, 44], работающая в аналитико-табличных вариантах классической пропозициональной и модальной логик, дает возможность рассматривать с единой точки зрения различные исчисления, лежащие в основе систем автоматического поиска вывода, такие как DPLL, КЕ, HARP, ВСР, KSAT, гипер-таблицы). В ряде исследований предлагаются также комбинированные методы — аналитические таблицы в сочетании с теоретико-игровым подходом [34, 35], средствами теории автоматов [5], элементами проверки модели (model-checking) [23]. Заметим еще раз, что, вообще говоря, аналитические таблицы не обязательно используются только как разрешающая процедура. Ничто не мешает использовать метод и для неразрешимых систем, как например, первопорядковой классической логики. В таком случае речь идет о полуразрешающей процедуре.
Метод аналитических таблиц очень успешно применяется в классических модальных логиках, в ряде систем временных логик вычислимости, в комбинированных логиках с временным измерением. Однако, под одним названием скрываются, на самом деле, далеко не однородные методы. Нередко оказывается, что для нового класса логических систем требуется придумывать и совершенно новый подход. Причины этого лежат в существенных семантических различиях логик, а аналитические таблицы тесно связаны с семантикой в первую очередь. Так, если пы таться адаптировать для прайоровских систем временной логики метод таблиц с префиксированными формулами, прекрасно работающий в модальной логике, то возникают немалые технические трудности. С другой стороны, табличные алгоритмы, разработанные для временных логик, интересных с точки зрения компьютерных наук, также оказываются не подходящими для других систем временной логики. Найти простой и естественный подход к построению аналитических таблиц, который был бы как можно более адаптивным и в то же время обладал удобством в применении и практической значимостью — важная и интересная, на наш взгляд, задача.
Целью диссертационного исследования является решение проблемы разработки аиалитико-табличных исчислений для стандартных прайоровских систем временной логики и систем с нестандартным отношением между прошлым и будущим. Требуемыми характеристиками исчислений являются максимальная понятность правил и простота в применении. В то же время основная идея, используемая при построении формализации, должна позволять адаптировать совокупность правил редукции для различных логических систем с минимальными изменениями. Для достижения указанных целей, в ходе диссертационного исследования, решались следующие задачи: Анализ различных подходов к построению аналитико-табличиых формализации систем модальной и временной логики с целью выявления их сильных и слабых сторон. Последующее нахождение наиболее общего метода, применимого при разработке аналитических таблиц для широкого класса стандартных систем временных логик. Детальное описание метода. Формулировка правил редукции для наиболее известных систем временной логики. Доказательство непротиворечивости и полноты построенных аналитико-табличных формализации. Формулировка правил редукции для систем временной логики с нестандартным отношением сопряженности между прошлым и будущим.
Стандартные (прайоровские) системы временной логики
Поясним, что имеется в виду. Пусть применяется правило [v] к некоторой формуле аїр и требуется проверить, использовался ли в ветви нужный префикс а . Для этого необходимо подняться вверх по текущей ветви (от узла, содержащего аср к корню) и проверить, содержится ли в каком либо из попадающихся нам узлов формула с префиксом а . Для применения правила, требующего, чтобы префикс а был новым, нужна несколько более длительная проверка. Необходимо просмотреть все узлы уже построенного дерева таблицы и проверить, нет ли такого узла, что его формула имеет префикс а . Правила для пропозициональных связок и модальные правила [v] и [ет] составляют ядро для конструирования аналитико-табличных исчислений. Для того, чтобы получилось требуемое исчисление, требуется добавить к этому базису еще некоторые условия (side conditions), специальные для каждого конкретного исчисления. Условия связаны с правилом перехода v, правило 7Г обычно одинаково для разных систем, единственным требованием является то, чтобы префикс а.к был новым. Условия достижмости на множестве префиксов для некоторых известных систем модальной логики приведены в таблице 1.2.
Метод таблиц с префиксированными формулами получил развитие в работах Массаччи [41, 43, 45], Горе и Беккерта [6, 7, 26], Говернатори и Артози [4, 27, 28], ряда других авторов (см. [15]). В работах [4, 6] реализована идея префиксов, содержащих переменные, заменяемые произвольными префиксами. Это позволяет применять метод унификации для нахождения замкнутых ветвей.
Особо выделяется подход Массаччи-Горё, связанный с разработкой «одношаговых» префиксных аналитических таблиц (single step analytic tableaux) [26, 45]. Преимущество этого метода в том, что получаемые аналитико-табличные исчисления обладают свойством модулярности. То есть, существует базисное минимальное аналитико-табличное исчисление, ТК, а каждое его расширение получается путем добавления характеристических правил. Помимо этого, правила предельно просты, легко просматривается связь с семантикой.
Вместо того, чтобы вводить дополнительные условия на отношение достижимости на префиксах, как у Фиттинга, вся необходимая информация заключается в конструкции правила. В отличие от систем Фиттинга, v - правила позволяют использовать только простые расширения исходного префикса. С точки зрения шкалы Крипке, это означает, что разрешены лишь переходы из исходного мира в его непосредственный наследник. Однако, любой «длинный» переход по некоторой последовательности миров, позволяемый фиттинговским правилом, может быть осуществлен шаг за шагом правилами таблиц в стиле Массаччи-Горё. В результате дополнительные условия (side conditions) фиттинговских правил могут быть смоделированы за счет многократного применения одношаговых правил.
В целом таблицы имеют те же конструктивные особенности, что и в рассмотренном фиттинговском варианте. Префиксы формул представляют собой последовательности индексов. Индексы отделяются точками. Число различных индексов, содержащихся в префиксе есть его длина. Префикс т есть простое расширение префикса а, если г = а.п, где п есть индекс. Префикс г есть расширение префикса х, если т = о-.щ.щ ...щ. Множество префиксов Г называется строго порожденным.
Множество строго порожденных индексов может рассматриваться как дерево, каждый узел которого отмечен некоторым индексом. В качестве индекса, находящегося в корне дерева обычно используется 1.
Аналитическая таблица представляет собой дерево, в котором каждый узел отмечен префиксированной формулой, или, более просто, есть дерево префиксированных формул. При этом каждая префиксированная формула в дереве, за исключением корневой, содержащаяся в некоторой ветви В, получена по одному из правил редукции из формулы, предшествующей данной в В. Ветвь аналитической таблицы замкнута, если в ней содержатся префиксироваиные формулы аїр и а-кр одновременно. Аналитическая таблица замкнута, если замкнута каждая ее ветвь. Доказательством формулы (р называется замкнутая аналитическая таблица с корнем 1-1 3. Префикс а использовался в ветви В, если В содержит префиксиро-ванную формулу аїр. В противном случае префикс а является новым в ветви. Аналитико-табличное исчисление ТС классической пропозициональной логики получается в том случае, если ограничиться правилами [ -і ], [ Л ] и [ -іЛ ]. Каждое аналитико-табличное исчисление TL модальной логики содержит ТС в качестве подсистемы. Кроме того, каждое модальное исчисление должно содержать правило [ ж ]. Оно одинаково для всех модальных исчислений. В перечне 1.4 приведены все остальные правила, необходимые для формализации различных модальных систем. В таблице 1.3 представлены наборы правил редукции, соответствующие каждому модальному аналитико-табличному исчислению.
Аналитические таблицы для временной системы Kt
Метод таблиц с префиксированными формулами представляется нам более удобным с практической точки зрения, чем метод таблиц, где правила требуют удаления формул из множеств или модификации ветви. Кроме того, метод префиксированных таблиц имеет преимущество с точки зрения построения расширений исходной (минимальной) логической системы. В случае таблиц с вычеркиваниями требуется изменение правил для модальностей при переходе к новой системе. Префиксирован-ные таблицы фиттинговского типа предполагают неизменяемый базис правил, а для формализации расширений исходной системы нужно добавлять ограничения на отношение на множестве префиксов. Таблицы в духе Горе-Массаччи напоминают аксиоматические построения по способу получения расширений. В последнем случае расширения исходной системы получаются за счет варьирования множества аксиом, добавляющихся к базисным. В таблицах Горё-Массаччи также имеется базисный набор правил для системы К, а ее расширения можно получить путем добавления к базисному набору необходимой для каждой системы совокупности правил.
Возникает естественный вопрос: можно ли успешно применять метод таблиц с префиксированными формулами и для систем временной логики прайоровского типа? Прежде, чем ответить на этот вопрос, нужно более подробно рассмотреть связь аналитико-табличных правил и свойств шкал Крипке.
В последнее время появился ряд работ, в которых исследовался вопрос о том, что служит причиной устойчивой разрешимости (английский термин "robust decidability") модальных логик [29, 39, 59]. Авторы перечисленных работ сходятся в том, что разрешимость и приемлемые слож-ностные характеристики модальных логик обусловлены главным образом двумя принципами локальности. Первый принцип связан с тем, что вместо произвольной модели для некоторой формулы р можно рассматривать (бисимулярную ей) древесную модель. Второй принцип говорит о том, что ветвление и глубина этого дерева ограничены модальным рангом формулы (р, который всегда конечен. Таким образом, в классической модальной логике модели могут быть представлены в виде конечных деревьев.
Это обстоятельство важно для построения аналитических таблиц с префиксированными формулами. Доказательство теоремы о непротиворечивости показывает, что модель, которая определяется исходя из построения аналитической таблицы имеет специальный вид. Напомним, что область этой модели содержит в качестве точек все префиксы, встречающиеся в построении. Во-первых, это коническая модель — множество префиксов, участвующих в построении является строго порожденным. Иными словами, модель содержит точку, из которой есть путь в любую другую точку модели. Во-вторых, это древесная модель, поскольку для всякого префикса а множество его о-предшественников конечно и линейно упорядоченно. Префикс кодирует путь от корневой точки модели до той точки, в которой «находится» префиксированная формула. Эта конструкция похожа на ту, которая применяется в доказательстве теоремы о развертке (то есть о возможности представить произвольную коническую модель в древесной форме). Для того, чтобы перестроить исходную (коническую) модель в древесную, нужно взять в качестве точек новой модели всевозможные пути из корня модели. При этом новое отношение (обозначим через R ) определяется так: если имеется путь т = (w0,... ,wn) и точка v такая, что R(wn,v), где R есть отношение на области исходной модели, то Я (т, т ), где т = {wo,..-,wn,v). Таким образом, таблицы с префиксами, состоящими из последовательностей индексов, напрямую ориентированы на построение древесной модели и предполагают возможность всегда ограничиваться только такими моделями.
Однако, ситуация с системами временной логики Прайора несколько иная. Наличие двух базисных взаимно неопределимых модальностей принципиально не разрушает возможность представлять всякую модель в древовидной форме. Однако ветви дерева теперь могут порождаться разными модальностями. Поэтому в дереве получается как-бы два сорта путей. Кодирование путей с помощью префиксов приводит к тому, что появляются префиксы разных типов или разных сортов. Прежде всего возникает необходимость различать разносортные префиксы и формулировать правила редукции с учетом этого различения. Естественно ожидать, что это усложнит структуру правил. Подобная стратегия реализована в работах Боннетт-Горё [9, 10], где строится секвенциальная формализация некоторых прайоровских систем временной логики, ориентированная на машинную реализацию на языке Пролог. Префикс представляет собой последовательность формул, каждая из которых может находиться в одной из позиций — «направлена» вперед или назад. Нам представляется, что подход Боннетт-Горё обладает некоторыми нежелательными особенностями. Помимо сложной структуры правил, данная система ориентирована главным образом на компьютерную реализацию процедуры поиска вывода.
Возможно ли какое-либо еще продуктивное использование префикси-рованных таблиц для построения аналитико-табличных формализации прайоровских систем временной логики? Как при этом избежать слишком громоздких правил и сохранить, насколько это возможно, ясность и прозрачность метода, как в случае формализации систем нормальной модальной логики?
Один из возможных ответов на этот вопрос предлагается в настоящей работе и состоит в следующем. Вместо префиксов, образующихся из последовательностей индексов, нужно использовать в качестве префиксов просто индексы. Каждая формула несет с собой теперь лишь один индекс, а не всю свою историю, как раньше. Наличие префиксов предполагает, что отношение достижимости в модели будет представлено в табличном построении эксплицитно. Раньше такую возможность давала структура префикса, теперь необходимо другое средство для представления отношения достижимости в модели. Точные определения приводятся в следующем параграфе.
Аналитико-табличные формализации систем временной логики с нестандартным отношением между прошлым и будущим
Модели для прайоровских временных логик тоже могут быть представлены в виде деревьев, но уже, по крайней мере, двусортных. Это связано с наличием двух базисных модальностей в языке. Таким образом, если использовать подход с построением сложных префиксов, то уже сами эти префиксы должны внутри своей структуры изображать эту двусортность деревьев на временных шкалах. Буквальная реализация такой идеи сложна в техническом исполнении и уже далека от простоты аналитико-табличных формализмов обычной модальной логики.
В то же время, не хотелось бы совсем отказываться от метода пре-фиксированных формул. В настоящей работе мы поставили целью найти среднюю линию, позволяющую соединять выразительные возможности метода, с одной стороны, и простоту реализации с другой. Идея состоит в том, чтобы префиксировать формулы простыми числовыми индексами, являющимися метками возможных миров, и собирать информацию об отношении достижимости в отдельном блоке. Конструкция таблиц такова, что всякое множество индексированных формул, участвующих в построении, снабжено особым множеством, хранящим информацию об отношении в модели.
Предлагаемый подход сочетает в себе черты многих других методов, разработанных в области аналитико-табличных формализации модальной логики за последние десятилетия. Стилистически наши таблицы восходят к работам М. Фиттинга, идея же индексировать формулы числами была предложены еще в 50-х годах Кангером. Наш подход не связан с какой-либо конкретной системой временной или модальной логики. Представляется, что на его основе могут быть разработаны аналитические таблицы для любой логики, которая допускает построение семантики типа Крипке и многообразие шкал которой характеризуется условиями, выразимыми в языке первопорядковой логики. В настоящее время выделилось целое направление в разработке теоретико-доказательственных методов, связанное с добавлением к формулам особых меток, имеющих семантический смысл (labelled deduction systems). Думается, что предлагаемый метод укладывается в русло этого развивающегося направления.
Для реализации метода были выбраны некоторые хорошо известные и некоторые оригинальные системы временной логики, выбор прайоров-ских систем временной логики был мотивирован тем, что, во-первых, это традиционные и хорошо известные для философской логики системы, и, во-вторых, они несколько отодвинуты на задний план временными логиками, пришедшими из компьютерных наук. Последнее обстоятельство повлияло на то, что большинство работ, посвященных разработке аналитических таблиц для временной логики, оставляют прайоровские системы в стороне. С другой стороны, мы также выбрали для исследования системы временной логики, почти совсем не известные широкому кругу специалистов, работающих в области неклассических логик. Это временные логики с нестандартным отношением сопряженности между прошлым и будущим, разработанные выдающимся отечественным логиком В.А. Смирновым.
В работе предложен аналитико-табличный вариант временной системы Kt и ряда ее расширений: логик линейного, плотного и бесконечного времени. Доказаны метатеоремы о полноте и непротиворечивости этих систем. Нужно заметить, что совокупность правил редукции для системы Kt содержится в виде собственной части каждым ее расширением. Более того, добавочные правила для расширений не затрагивают правила редукции для логических связок, а связаны только с преобразованиями множества, содержащего информацию об отношении достижимости. Здесь просматривается аналогия со структурными правилами и способом получения субструктурных логик варьированием набора структурных правил в исчислении. Помимо этого имеется аналогия с построением аксиоматических исчислений, когда каждое характеристическое свойство временного потока связано со своей специальной аксиомой. Такой способ построения аналитико-табличного исчисления представляется наиболее удобным. Аналитические таблицы для систем логик с нестандартным отношением В.А. Смирнова можно рассматривать как иллюстрацию идеи о широкой применимости метода.
Можно поставить ряд задач для дальнейшей работы. В первую очередь, хотелось бы исследовать вопрос о применимости изложенного в работе метода для построения аналитических таблиц для систем временной логики с двухместными временными операторами типа Until и Since. Временные логики с такими модальностями привлекают внимание исследователей в силу широких выразительных возможностей языков, обогащенных двухместными модальностями. Другая область применения метода — многомерные модальные логики. Такие модальные логики содержат в языке модальности различных типов. Например, временная логика параллелизма, описанная в работе М. Рейнольдса [53], строится на базе временной модальности логики Lin линейного времени и обычной S5 - модальности. Разрешающий алгоритм, основанный на методе мозаик (см. также статью [38]), оказывается весьма сложным. Было бы интересным исследовать вопрос, нельзя ли в этом случае разрабатывать разрешающий алгоритм на базе аналитических таблиц? В той же работе [53] указывается, что как примеры двумерных логик могут быть рассмотрены и временные логики исторической необходимости (см. работы Д. Берджеса [11] и А. Занардо [61]). Родственные им системы — это логики CTL и СТЬ в прикладных логиках для компьютерных наук. Однако, существующие аналитические таблицы для систем CTL и CTL используют аппарат ц - исчисления и имеют ряд семантических ограничений. Думается, что разработка аналитико-табличных вариантов систем логики исторической необходимости является сложной, но интересной задачей.
Нам представляется, что предлагаемые аналитико-табличные исчисления просты в работе и могут быть использованы как удобный и гибкий инструмент для решения вопроса об общезначимости формул для различных систем временной логики.
