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

Короткий опис

Содержание
Оглавление

Введение • 2

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

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

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

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

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

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

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

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

системы Kt...44

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

системы TKt...49

§5 Аналитические таблицы для расширений

временной системы Kt...86

§6 Аналитико-табличные формализации систем временной логики с нестандартным отношением между прошлым и будущим ...101

Заключение 106
Введение

Введение

Временная логика является одной из наиболее интенсивно изучаемых областей современной символической логики. Первоначально интерес к ней был вызван философскими проблемами, связанными с интерпретацией высказываний с временными модальностями. Толчок к развитию временной логики дали работы Артура Прайора [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 столетия наметился определенный всплеск интереса

6

к построению формализмов генценовского типа для модальных логик. Упомянем здесь таких авторов, как К. Дошен, Г. Вансинг, А. Аврон. Секвенциальные исчисления с префиксированными формулами для ряда стандартных систем временной логики были построены австралийскими логиками Р. Горе и Н. Боннетт [9, 10].

Среди российских логиков свой вклад в разработку секвенциальных исчислений для модальной логики внесли Г. Е. Минц, О. Ф. Серебрянников, П. И. Быстров и др.

В последнее время появились работы, в которых предлагается ряд технических усовершенствований, позволяющих улучшить алгоритмические характеристики аналитических таблиц и преодолеть «отставание» в отношении конкурирующих методов (например, процедура симплифи-кации представленная в работах [42, 43, 44], работающая в аналитико-табличных вариантах классической пропозициональной и модальной логик, дает возможность рассматривать с единой точки зрения различные исчисления, лежащие в основе систем автоматического поиска вывода, такие как DPLL, КЕ, HARP, BCP, KSAT, гипер-таблицы). В ряде исследований предлагаются также комбинированные методы — аналитические таблицы в сочетании с теоретико-игровым подходом [34, 35], средствами теории автоматов [5], элементами проверки модели (model-checking) [23J. Заметим еще раз, что, вообще говоря, аналитические таблицы не обязательно используются только как разрешающая процедура. Ничто не мешает использовать метод и для неразрешимых систем, как например, первопорядковой классической логики. В таком случае речь идет о полуразрешающей процедуре.

Метод аналитических таблиц очень успешно применяется в классических модальных логиках, в ряде систем временных логик вычислимости, в комбинированных логиках с временным измерением. Однако, под одним названием скрываются, на самом деле, далеко не однородные методы. Нередко оказывается, что для нового класса логических систем требуется придумывать и совершенно новый подход. Причины этого лежат в существенных семантических различиях логик, а аналитические таблицы тесно связаны с семантикой в первую очередь. Так, если пы-

таться адаптировать для прайоровских систем временной логики метод таблиц с префиксированными формулами, прекрасно работающий в модальной логике, то возникают немалые технические трудности. С другой стороны, табличные алгоритмы, разработанные для временных логик, интересных с точки зрения компьютерных наук, также оказываются не подходящими для других систем временной логики. Найти простой и естественный подход к построению аналитических таблиц, который был бы как можно более адаптивным и в то же время обладал удобством в применении и практической значимостью — важная и интересная, на наш взгляд, задача.

Целью диссертационного исследования является решение проблемы разработки аиалитико-табличных исчислений для стандартных прайоровских систем временной логики и систем с нестандартным отношением между прошлым и будущим. Требуемыми характеристиками исчислений являются максимальная понятность правил и простота в применении. В то же время основная идея, используемая при построении формализации, должна позволять адаптировать совокупность правил редукции для различных логических систем с минимальными изменениями. Для достижения указанных целей, в ходе диссертационного исследования, решались следующие задачи:

• Анализ различных подходов к построению аналитико-табличпых формализации систем модальной и временной логики с целью выявления их сильных и слабых сторон. Последующее нахождение наиболее общего метода, применимого при разработке аналитических таблиц для широкого класса стандартных систем временных логик. Детальное описание метода.

• Формулировка правил редукции для наиболее известных систем временной логики. Доказательство непротиворечивости и полноты построенных аналитико-табличных формализации.

• Формулировка правил редукции для систем временной логики с нестандартным отношением сопряженности между прошлым и будущим.

В ходе проведенной работы были получены следующие результаты:

• Разработан общий метод построения аналитико-табличных исчислений для систем временной логики, позволяющий охватить широкий класс известных логических систем при незначительных модификациях совокупности правил редукции. Фактически имеется минимальная совокупность правил редукции, непротиворечивая и полная относительно класса всех временных шкал Крипке, то есть аналог системы Kt. Добавочные правила редукции позволяют получить расширения минимальной системы. При этом правила редукции для логических связок, включая модальности, остаются общими для всех систем.

• Построены аналитико-табличные варианты известных систем временной логики — минимальной системы Kt ряда ее расширений: логики транзитивного (Kt.4), линейного, плотного и бесконечного времени.

• Доказаны теоремы об адекватности предложенных аналитико-табличных исчислений.

• Построены аналитико-табличные формализации некоторых логик времени с нестандартным отношением сопряженности прошлого и будущего.

Аналитико-табличные процедуры часто являются основой для создания компьютерных программ для автоматического поиска доказательства. Эта сфера исследований стала чрезвычайно важной в связи с развитием компьютерной техники и соответствующей теоретической дисциплины. Автоматические методы рассуждения на базе временных логик применяются при описании вычислительных процессов, верификации и спецификации программ, в сфере криптографии.

Глава 1

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

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

Секвенциальные исчисления являются, видимо, наиболее близким к аналитическим таблицам методом в теории доказательств. Правила для введения логических связок в секвенциальных исчислениях, и правила редукции в аналитико-табличных, действуют при построении доказательства сходным образом, поскольку используют одни и те же свойства логических связок. В этом смысле оба формализма стоят на одном основании. Различия состоят в том, что представляют собой объекты, над которыми строится исчисление. Это могут быть секвенции в одном случае и множества формул в другом. Естественно, различаются тогда и определения вывода, определения доказательства и технические приемы, служащие для доказательства метатеорем. Однако в ряде случаев можно показать, что правила редукции аналитических таблиц перестра-

10

иваются в правила введения связок исчисления секвенций и наоборот (см. пример в работе Р. Горе [26, с. 68] для модальной системы К).

Генценовские исчисления для наиболее известных систем нормальной модальной К, Т, S4 и S5, появились еще в 50-х годах. Одной из первых работ по этой тематике является статья X. Карри [14]. Далее последовали работы М. Ониши и К. Мацумото [48, 49, 50], в которых развивались полученные Карри результаты. Секвенциальные исчисления для модальных систем, исследуемые в указанных работах, получаются за счет добавления правил для модальностей к какому-либо варианту ген-ценовского исчисления классической пропозициональной логики. Правила для модальностей, дающие секвенциальный вариант системы S5, имеют следующий вид1:

пд _ пг,

. . -»ог

Где ПД = {П-^ | ф е А}, ОД = {О-^ | ф € Д}.

Ч

Если множество Г в правилах [— П]о и [О —]о пусто, то получается секвенциальный вариант системы S4. Если же правила [— П]о и [О —]0 заменить правилами

то это дает секвенциальный вариант системы Т. Наконец, генценовский вариант минимальной нормальной модальной системы К получится, если к генценовскому исчислению классической логики добавить только правило [—¦ а]х.

После выхода работ Ониши и Мацумото исследования в области ген-ценовских формализации модальной логики продолжались. В частности,

качестве источника была использована работа [60].

11

были получены секвенциальные исчисления ряда известных модальных систем: К4 [54], KD, KD4 [24], К45, KD45 [55], KB, KTB, KDB,

К4В [57]. Более полный обзор стандартных секвенциальных формализации модальных систем можно найти в работах [25] и [62].

Наряду с исследованиями, в которых строились секвенциальные варианты лыоисовских систем, появлялись также работы, в которых предлагались генценовские исчисления для временных логик. Например, статья X. Нишимуры [47], где дана генценовская формализация временных систем Kt и Kt4. Приведем правила для временных модальностей. Для системы Kt правила такие:

Где GA = {Gip | € Д}.

Правила для системы Kt4 выглядят следующим образом:

(ЗГ,Г—у,ЯД,НД

L ^ j4 (?Г — .

В последние годы предпринимались многочисленные попытки построить секвенциальные модальные исчисления, в которых бы преодолевались те или иные недостатки традиционных систем. Кратко упомянем некоторые работы, связанные с обобщением генценовского подхода.

13

ч

В работах Церрато [12, 13] используются особые модальные метазна-ки необходимости и возможности (modal signs). Каждой характеристической аксиоме (К, Т, В, 4, 5, D) соответствует свое правило введения связки. При этом правила удовлетворяют свойствам сепарабельности и, кроме того, выполняется свойство подформульности. Однако, устранение сечения доказывается лишь для системы К. Принцип Дошена в целом не выполняется. Специальные правила дуальности позволяют доказать О -|Щ-1.

Коста Дошен в работе [16] предлагает особые секвенциальные исчисления для систем S4 и S5. Секвенции могут быть произвольного конечного уровня. Секвенция уровня 1 такая же, как обычная, секвенция уровня п+1 может содержать но обеим сторонам стрелки конечные множества секвенций уровня п. Сечение устраняется только в том случае, когда правило содержит секвенции уровней 1 и 2. При этом неясно, как получить на основе этого метода секвенциальные исчисления для других модальных систем.

Интересный подход представлен в работах Масини [40, 37]. Используются так называемые многомерные секвенции. Подход Масини дает секвенциальные варианты лишь для систем К и KD, но при этом правила * обладают свойствами сепарабельности, эксплицитности и симметрично-

сти. Кроме того для эти систем имеет место теорема об устранимости сечения. Также доказывается разрешимость полученных систем.

Семантически ориентированные таблицы появились вместе с реляционной семантикой в фундаментальных статьях Саула Крипке [31, 32, 33]. Стиль этих таблиц позаимствован из работы Э. Бета, который использовал метод семантических таблиц как полуразрешающую процедуру для первопорядковой классической логики. Видимо, само название метода — «таблицы» — произошло от графического оформления этой процедуры. Формулы записывались в колонки таблицы, истинные (по предположению) — в левую, ложные в правую. Для доказательства формулы (р сначала принимается допущение о ее ложности. Поэтому построение таблицы для формулы ср начинается с помещения ц в правую часть таблицы. Некоторые правила предусматривают возможность расщепления табли-

14

цы на подтаблицы, что осуществляется удвоением каждой колонки исходной таблицы. Подтаблица считается замкнутой, если содержит одну и ту же формулу в истинной и ложной части. Вся таблица замкнута, если замкнута каждая ее подтаблица. Таким образом, формула ip считается доказанной, если построена замкнутая семантическая таблица для и \ Л, а также одной базисной модальностью П. Правила для связок, выра-

зимых через исходные, нетрудно получить при необходимости. Назовем табличный вариант системы S4 как TS4. Ограничимся здесь более или менее неформальными разъяснениями относительно устройства таблиц, избегая пока строгих определений. В самом общем плане рассмотрения можно сказать, что таблица есть последовательное преобразование некоторых совокупностей формул. В данном варианте таблиц мы будем использовать не просто формулы сами по себе, а формулы с отметками Т и F. Это метаязыковые символы, которые нужно понимать как допущения истинности или ложности формулы соответственно. С помощью левой и правой угловых скобок множества отмеченных формул отделяются друг от друга. Греческие заглавные буквы используются для обозначения множеств отмеченных формул, строчные — для обозначения формул. Таким образом, элементарная составляющая таблицы будет иметь

16

Список литературы