автореферат диссертации по философии, специальность ВАК РФ 09.00.07
диссертация на тему: Аналитико-табличная формализация систем временной логики

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

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ Имени М. В. ЛОМОНОСОВА ФИЛОСОФСКИЙ ФАКУЛЬТЕТ

На правах рукописи

ГРИГОРЬЕВ Олег Михайлович

АНАЛИТИКО-ТАБЛИЧНАЯ ФОРМАЛИЗАЦИЯ СИСТЕМ ВРЕМЕННОЙ ЛОГИКИ

Специальность 09.00.07 - логика

АВТОРЕФЕРАТ

Диссертации на соискание ученой степени Кандидата философских наук

Москва 2004

Работа выполнена на кафедре логики философского факультета Московского государственного университета им. М. В. Ломоносова.

Научный руководитель:

доктор философских наук МАРКИН В. И.

Официальные оппоненты:

доктор философских наук ВАСЮКОВ В. Л.

кандидат философских наук ЛЕВЕНЕЦ Е. В.

Ведущая организация:

Санкт- Петербургский государственный университет, кафедра логики

Защита состоится 29 июня 2004 года в 15 часов на заседании Диссертационного совета Д 501.001.48 по защите диссертаций на соискание ученой степени доктора философских наук в Московском государственном университете им. М. В. Ломоносова.

С текстом диссертации можно ознакомиться в научной библиотеке МГУ, 1 гуманитарный корпус.

Автореферат разослан «_» мая 2004 г.

Ученый секретарь Диссертационного совета кандидат философских наук

ЗАЙЦЕВ Д. В.

Общая характеристика работы

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

В дальнейшем, с развитием компьютерного знания, возникла необходимость в разработке формализмов, позволяющих описывать вычислительные процессы и работу разнообразных вычислительных устройств. Поскольку временной параметр есть часть характеристики любого процесса, высказывания с временными модальностями, как правило, присутствуют в его описании. В результате временная логика стала привлекать внимание специалистов из области компьютерных наук и развиваться как прикладная дисциплина. Ее задачами стали верификация и спецификация программ и оборудования (hardware), анализ параллельных процессов, представление знания (knowledge representation) и передача информации, оптимизация работы компьютерных сетей и многое другое. В настоящее время временная логика утвердилась как мощное и эффективное средство для решения перечисленных задач.

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

j foi. НАЦИОНАЛЬНАЯ I I БИБЛИОТЕКА {

! iygp/^j

го является фундаментальной характеристикой любой логической системы. В связи с интенсивным развитием прикладной логики, проблема разрешимости и нахождения разрешающих алгоритмов обрела еще и практическое значение. Одной из конкретных реализаций разрешающей или полуразрешающей процедуры для логических систем является метод аналитических таблиц. Этот метод получил широкую известность начиная с классической работы Р. Смаллиана "First Order Ligic" (1969).

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

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

класс дедуктивных постулатов аналитико-табличного исчисления. В силу этого обстоятельства, аналитические таблицы являются чрезвычайно гибким — в отношении адаптации к различным логическим системам — и максимально удобным с практической точки зрения методом.

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

Степень разработанности проблемы. Одной из первых работ, в которых метод аналитических таблиц стал применяться к модальным логикам, является монография Мелвина Фиттинга "Intuitionis-tic Model Theory and Forcing" (1969). Здесь было сформулировано аналитико-табличное исчисление для модальной системы S4. В 1972 году, в одной из своих публикаций, Фиттинг представил аналитико-табличные исчисления для ряда известных модальных систем. При этом использовался метод префиксированных формул, который затем стал широко употребляться при построении аналити-ко-табличных вариантов неклассических логик.

Метод таблиц с префиксированными формулами получил развитие в работах таких авторов, как Ф. Массаччи, Р. Горе, Б. Беккерт, Г. Говернатори, А. Артози и многих других. В ряде статей Беккерта и Горе реализована идея префиксов, содержащих переменные, заменяемые произвольными префиксами. Это позволяет применять метод унификации для нахождения замкнутых ветвей в таблице. Особо выделяется подход Массаччи-Горе, связанный с разработкой так называемых «одношаговых» префиксных аналитических таблиц (single step analytic tableaux). Преимущество этого метода в том, что получаемые аналитико-табличные исчисления обладают свойством модулярности. Другими словами, существует базисное минимальное аналитико-табличное исчисление, а каждое его расширение получается путем добавления характеристических правил. Помимо этого, правила предельно просты, легко просматривается связь с семантикой. В 1999 году вышел объемный "Handbook of Tableaux Methods", в котором обобщены разработки в области построения аналитических таблиц для классической и неклассической логики.

Среди отечественных работ по данной теме следует отметить книгу А. Т. Ишмуратова «Логический анализ временных контекстов» (1982), в которой предлагается вариант построения аналитических таблиц для временной системы Kt. Особенностью подхода является то, что конструкцию аналитической таблицы сопровождает граф, изображающий отношение достижимости в модели Крипке.

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

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

В контексте исследования по аналитическим таблицам нельзя обойти стороной такую область, как построение секвенциальных исчислений для модальных и временных логик. Ранние работы в этой области можно рассматривать как предшествующие появлению аналитико-табличного метода. Исчисления генценовского типа для наиболее известных систем нормальной модальной логики К, Т, S4 и S5, появились в 50-х годах XX века. Одной из первых работ в этой области является статья X. Карри, вышедшая в 1952 году. Далее последовали работы М. Ониши и К. Мацумото, в которых развивались полученные Карри результаты. Впоследствии статьи на эту тему время от времени появлялись в литературе. В конце XX столетия наметился определенный всплеск интереса к построению формализмов генценовского типа для модальных логик. Упомянем здесь таких авторов, как К. Дошен, Г. Вансинг, А. Аврон.

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

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

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

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

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

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

Научная новизна работы. В диссертации построены аналитико-

табличные исчисления для ряда систем временной логики, известных как системы Леммона-Прайора. При разработке исчислений применялся оригинальный метод, позволивший с единой точки зрения изучить разнородные системы. Предлагаемый метод характеризуется следующими чертами:

• Введение элементарной конструкции таблицы, в которой разделяются блок пар индексов (натуральных чисел) и блок индексированных натуральными числами формул. Строка аналитической таблицы состоит из совокупности таких элементарных конструкций. Правило редукции заменяет одну из элементарных конструкций в строке на одну или несколько новых.

• Различение двух типов правил — правил для логических связок (в том числе и модальностей) и правил для множества пар индексов. Такое различение аналогично различению структурных правил и правил для логических связок в субструктурных логиках. Оно дает похожий эффект: правила для логических связок являются общими для всех систем и сами по себе образуют исходную минимальную систему (систему Расширения же получаются за счет присоединения некоторой совокупности дополнительных правил редукции.

• Дополнительные правила редукции имитируют первопоряд-ковые свойства шкал Крипке, детерминирующих логику, для которой строится аналитико-табличная формализация. Это, с одной стороны, «встраивает» семантическую информацию в структуру правил редукции и сближает семантические и синтаксические методы обоснования общезначимости формул. С другой стороны, указанные правила редукции имеют ясный смысл: многие стандартные первопорядковые условия, характеризующие шкалы Крипке легко перестраиваются в добавочные правила редукции, что позволяет охватить широкий спектр временных систем, для которых класс шкал Крипке является элементарным.

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

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

• Разработан общий метод построения аналитико-табличных исчислений для систем временной логики, позволяющий охватить широкий класс известных логических систем при незначи-

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

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

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

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

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

Апробация работы. Полученные в ходе диссертационного исследования результаты докладывались на теоретическом семинаре кафедры логики философского факультета МГУ им. М. В. Ломоносова, на 7-ой Общероссийской конференции «Современная логика: проблемы теории, истории и применения в науке» (СПб, 2002), 3-их и 4-х международных конференциях Смирновские чтения (Москва, 2001, 2003).

Структура диссертации. Диссертация состоит из введения, двух глав, заключения, приложения и списка литературы.

Основное содержание работы

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

Первая глава диссертации называется «Аналитические таблицы для логических систем с модальностями: различные подходы к построению». В этой главе, состоящей из двух параграфов, приведены исторические сведения о развитии метода аналитических таблиц и представлены различные идеи, которыми руководствуются при построении табличных формализаций.

В первом параграфе — «Родственные методы и история возникновения» — дается обзор истории возникновения и развития родственных (и в каком-то смысле предшествовавших) аналитическим таблицам методов. Это секвенциальные исчисления и семантические таблицы Бета для нормальных систем модальной логики.

Генценовские исчисления впервые были сформулированы в работах Ониши и Мацумото в конце 50-х годов XX века, хотя некоторые идеи были взяты ими из еще более ранней работы Карри. После этого статьи на данную тему выходили время от времени и в них расширялся круг систем, для которых строились исчисления секвенций. Отметим таких авторов, как Л. Гобл, Г. Е. Минц, М. Такано, Г. Шварц, Г. Сабмин и С. Валентини. В конце XX века наметился всплеск интереса к генценовским формализациям модальных логик. Появились новые подходы к построению систем, обобщающие генце-новский. В параграфе кратко описаны идеи К. Дошена, А. Масини, К. Церрато. В каждом из этих подходов авторы стремились построить исчисления, удовлетворяющие определенным методологическим принципам, в частности, принципам подформульности, модулярности, устранимости сечения и др. Такое стремление приводило к

существенному усложнению правил с одной стороны, и ограниченности применения формализма, с другой.

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

Во втором параграфе — «Аналитические таблицы» — дается история развития собственно аналитико-табличного метода и обзор современных подходов к их построению.

Первоначально аналитические таблицы применялись в классической логике. Правила редукции для первопорядковой логики были сформулированы Р. Смаллианом в книге "First Order Logic". В область неклассической логики аналитические таблицы были перенесены в конце 60-х годов XX века. Одним из пионеров этого направления был М. Фиттинг. В его книге 1969 года "Intuitionistic Model Theory and Forcing" были сформулированы табличные правила для интуиционистской логики и модальной системы S4. Правила редукции для S4 предполагают вычеркивания некоторых формул при переходе от посылки правила к заключению. Поэтому такой тип таблиц условно назван «таблицы с вычеркиваниями». В параграфе подробно описаны идеи, лежащие в основе доказательств полноты и непротиворечивости для табличных систем с вычеркиваниями. Выявлен основной недостаток аналитических таблиц данного типа — это их чувствительность к конкретной логической системе. Каждая из логик требует изобретения своих правил для модальностей. Кроме того, правила для некоторых модальных систем получаются очень громоздкими. Ряд систем модальной логики, например системы с аксиомами, требующими симметричности отношения в шкале,

требуют наличия специального правила аналитического сечения. Успешное построение доказательства зависит от порядка применения правил из-за потери информации при вычеркивании формул.

В параграфе также рассмотрен другой метод построения аналитических таблиц, в котором используются особые правила модификации ветви. В 1983 году вышла обобщающая монография Фиттинга "Proof Methods for Modal and Intuitionistic Logics", в которой приведены аналитические таблицы для широкого класса систем модальной логики. Однако, в этой работе за основу взят метод таблиц с правилами модификации ветви. Отличие от метода таблиц с вычеркиваниями в следующем. Аналитическая таблица, построенная с применением правил с вычеркиваниями формул представляет собой дерево, в котором каждый узел отмечен множеством формул. Совокупность множеств, находящихся на одном уровне в дереве, представляет собой строку аналитической таблицы. Правило редукции модифицирует одно из множеств последней строки таблицы. Все, что находится выше последней строки в таблице не представляет интереса на текущем шаге построения. Таблица, построенная с применением правил модификации ветви есть дерево, в котором каждый узел отмечен лишь одной формулой. Поэтому информация, релевантная текущему шагу построения таблицы, рассредоточена по всей ветви, в которой содержится преобразуемая формула. При применении некоторых модальных правил возникает необходимость коррекции этой информации, то есть модификации ветви. Это не очень удобно с практической точки зрения, но правила получаются более гибкими в отношении различных систем, чем в случае таблиц с вычеркиваниями.

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

В заключительной части обзора изложен метод построения таблиц с префиксированными формулами. Идея состоит в том, что

всякая формула аналитической таблицы соотносится с некоторым миром шкалы Крипке. Префикс есть метка (label) того мира с которым соотнесена формула. Наличие префиксов позволяет иметь информацию об отношении достижимости на множестве (помеченных) миров в явном виде, что упрощает формулировку правил и построение модели при доказательстве полноты. Префиксы могут быть простыми, например, индексы-натуральные числа, и сложными. Сложный префикс представляет собой последовательность индексов. Обычно, в качестве индексов используются натуральные числа, в последовательности они для удобства разделяются точками. Примеры префиксов: 1.2.4, 1.2.4.5, а.п, где а есть некоторая последовательность индексов, расширенная индексом п. На множестве префиксов задается отношение, имитирующее отношение достижимости в шкале Крипке. К примеру, префикс а' достижим из а, где а' = (г.п.т. Таким образом, формулировка правил для модальностей сильно упрощается. Правила для модальностей одинаковы для всех систем. Спецификация происходит на уровне ограничений, накладываемых на отношение достижимости на множестве префиксов.

Особо выделен подход Массаччи-Горё, связанный с разработкой так называемых «одношаговых» префиксных аналитических таблиц (single step analytic tableaux). Преимущество этого метода в том, что получаемые аналитико-табличные исчисления обладают свойством модулярности. Другими словами, существует базисное минимальное аналитико-табличное исчисление, а каждое его расширение получается путем добавления характеристических правил. Вместо того, чтобы вводить дополнительные условия на отношение достижимости на префиксах, как у Фиттинга, вся необходимая информация заключается в конструкции правила. В отличие от систем Фиттинга, правила позволяют использовать только простые, в один индекс, расширения исходного префикса. В параграфе приведены правила редукции для модальных систем, которые могут быть формализованы на основе данного подхода.

Вторая глава — «Аналитико-табличная формализация систем временной логики» — заключает в себе основное содержание диссертации. В ней описываются аналитические таблицы для временной системы К1 и ее расширений: логик линейного, плотного и бесконечного времени. Доказывается непротиворечивость и полнота построенных систем. Представлены логики В. А. Смирнова с нестандартным отношением сопряженности между прошлым и будущим в аналитико-табличном варианте. Глава состоит из шести параграфов.

В первом параграфе изложены общие сведения о временных логиках, которые в диссертационной работе называются «прайо-ровскими». Приведены характеристические аксиомы для каждой и систем.

В синтаксическом отношении прайоровские временные логики отличаются от классической пропозициональной логики добавлением в язык временных модальностей G и Я, «всегда будет» и «всегда было», соответственно. Эти модальности не выразимы друг через-друга и имеют дуальные варианты Р и Р, «когда-нибудь будет» и «когда-то было». Стандартное определение формулы в языке пропозициональной логики дополняется пунктом: если <р —формула, то также формула, где есть любая базисная модальная связка. Семантика строится на базе реляционных структур — временных шкал Крипке. Временная шкала представляет собой конструкцию вида (IV,К), непустое множество с заданным на нем отношением. Модель ЯЛ есть тройка (IV,Я,0), гд<0есть функция из множества пропозициональных переменных в Отношение между точками модели и формулами определяется стандартно для переменных и для классических связок; для модальных формул условия истинности таковы:

Во втором параграфе детально исследуется связь аналитических таблиц и семантических особенностей формализуемой логической

т, X И в<р <(=> Уу(Щх, у) => Ш, у 1= <р), ШУу(Щу, х) => Ж, у И Ф).

(1) (2)

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

Иным решением является отказ от сложных префиксов в пользу префиксов-индексов. При этом подходе теряется возможность определять отношение достижимости через структуру префиксов и требуется иной механизм для сохранения информации о достижимости. Этот подход и реализован в диссертационной работе.

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

Определение 1. Индексированной формулой будем называть последовательность вида в которой п есть индекс, есть

формула в языке парой называется двойка

в которой 72. есть множество пар индексов, Г есть множество индексированных формул.

Определение 2. Конечная совокупность И-Г-п&р называется конфигурацией.

Определение 3. Последовательность конфигураций (<!>ьс>21 • • •)> в которой каждое получено из применением одного из правил редукции называется аналитической таблицей.

Определение 4. "Я,-Г- пара называется замкнутой, если в составе множества Г одновременно присутствуют индексированные формулы вида п-чр иК^.нфигурация замкнута, если замкнуты все

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

Определение 5. Доказательством формулы ф называется замкнутая аналитическая таблица, первая конфигурация которой состоит из пустого множества И и множества Г, содержащего единственный элемент

Пояснения к правилам редукции. Для того, чтобы показать, что множество содержит некоторый элемент, будем выписывать его в квадратных скобках после символа, обозначающего это множество. Например, запись r{t<p\ обозначает, что множество Г содержит индексированную формулу Аналогично указывает на

то, что пара (п,тп) является элементом TZ. Звездочка на месте верхнего индекса у символа Г говорит о том, что из множества Г выброшен тот элемент, который был показан в квадратных скобках в верхней части правила.

Четвертый параграф посвящен доказательству полноты и непротиворечивости сформулированной системы. Для доказательства непротиворечивости показывается, что правила редукции сохраняют выполнимость при переходе от верхней части правила к нижней. Доказательство полноты использует понятие насыщенной вниз Последнее представляет собой аналог насыщенного вниз множества (downward saturated set) — стандартной конструкции в доказательствах полноты аналитико-табличных исчислений. Отличие в том, что приходится учитывать наличие множества в каждой TZ-Г- паре. Насыщенная вниз И-Г- пара допускает построение модели. Если незамкнутая таблица образует насыщенную вниз TZ-Г- пару, то тогда можно построить модель, отвергающую недоказуемую формулу. Таким образом, всякая недоказуемая формула не является общезначимой или, по-другому, всякая общезначимая формула доказуема.

В пятом параграфе строятся аналитико-табличные формализации расширений временной системы Определения

Правила редукции 1 Временная система ТКЬ

{П \ Г[п^}) <тг|г[п(ул0)1)

(П I Г* и {тг<?}) 11 <тг I Г*и{п<р,Т11р}}

(К\ Г[тН<р Л ?/>)]) (П I г* и {п-.<р}> (К I Г* и {п-ч/>}>

<тг|г[п(у>у^)]) (тг I Г* и {тор}) (7г I Г* и {пф}}

<тг| гму уу>)]> <тг. 1 г* и {п-«р,п^'Ф})

(П1 Г[п(<р У>)])

(тг | г* и (я | г* и {ш/>})

где индекс А; - новый где индекс к - новый

{К\ Г* и {пр, п-ч/>})

{Щ(тп, и)] | Г[тпСф\) (П\Ги{п<р})

(Тг[(т,п)] | Г{пНф\) {П\Ги{т<р})

(111 ГН-^)]) {7ги {(т,к)} | Г-ЩА;-^})

(К | Г[тЬНу)\) <7ги{(/с,т)} | Г* и {к-чр})

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

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

Свойства временного потока Правила

Транзитивность (временная [tran]

система К4.4)

Отсутствие ветвления в про- [сопр]

шлое

Отсутствие ветвления в буду- [остр]

щее

Линейность времени [¿ran], [сопр], [amp]

Бесконечность в прошлое [end! р]

Бесконечность в будущее [endlp]

Плотность времени [dens]

Линейное, плотное, бесконеч- [tran], [сопр], [сопр], [endlp],

ное в прошлом и будущем вре- [егайг], [dens]

мя

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

Правила редукции 2 Добавочные правила для расширений временной системы 7"!^

В правилах [сопр\ и [сопр] запись {Ик | Гк) обозначает одновременную замену индексов пи2в верхней 72.-Г-паре правила на новый индекс к.

где индекс k — новый, индекс п встречается в Г

где индекс k — новый, индекс п встречается в Г

где индекс к

новый,

индексы тип встречаются в Г

Главное отличие от прайоровских систем заключается в свойствах шкал Крипке. Теперь достижимость в прошлое не является обращением достижимости в будущее и, поэтому, нельзя обойтись только одним отношением в шкале. Первопорядковые формулы, характеризующие шкалы этого класса, имеют следующий вид:

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

В заключении подводятся итоги проделанной работы и намечаются дальнейшие перспективы в области построения аналитико-табличных вариантов систем временной логики. Обращается внимание на логики с временными операторами Until и Since, логики исторической необходимости и ряд других интересных логических систем, предоставляющих широкое поле для исследований в указанном направлении.

Результаты диссертационной работы нашли отражение в следующих публикациях автора:

[1] Григорьев О. М. Аналитико-табличные процедуры для временных логик // Электронный журнал «Logical Studies», №4, 2000. ISBN 5-85593-140-4

http: //www. logic. ru/Russian/LogStud/04

Ri{x,y) R2{y,x), Ri(x, у) Л Да(у, г) -> R\ (x, z)V R2(x,z)V x = z, Wx3y(R2(x,y)).

(3)

(4)

(5)

[2] Григорьев О. М. Аналитико-табличные формулировки систем временной логики // Смирновские чтения. III Международная конференция. Москва, 2001.

[3] Григорьев О. М. Аналитико-табличная формализация систем временной логики с нестандартным отношением между прошлым и будущим // Электронный журнал «Logical Studies», №8, 2002.

http://www.logic.ru/Russian/LogStud/08

[4] Григорьев О. М. Аналитико-табличная формализация систем временной логики с нестандартным отношением прошлого и будущего // Материалы VII общероссийской научной конференции «Современная логика: проблемы теории, истории и применения в науке». СПб, 2002.

[5] Grigoriev О. М. Mosaic Method and Analytic Tableaux for Temporal Logics. // Смирновские чтения. IV Международная конференция. Москва, 2003.

Р1223^

Отпечатано в учебном множительном центре, Москва, Ленинские горы, МГУ, 1 гуманитарный корпус. Тир. 100 экз.

Оглавление научной работы автор диссертации — кандидата философских наук Григорьев, Олег Михайлович

Введение

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

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

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

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

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

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

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

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

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

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

Введение диссертации2004 год, автореферат по философии, Григорьев, Олег Михайлович

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

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

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

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

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

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

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

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

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

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

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

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

Заключение научной работыдиссертация на тему "Аналитико-табличная формализация систем временной логики"

Заключение

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

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

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

Предлагаемый подход сочетает в себе черты многих других методов, разработанных в области аналитико-табличных формализации модальной логики за последние десятилетия. Стилистически наши таблицы восходят к работам М. Фиттинга, идея же индексировать формулы числами была предложены еще в 50-х годах Кангером. Наш подход не связан с какой-либо конкретной системой временной или модальной логики. Представляется, что на его основе могут быть разработаны аналитические таблицы для любой логики, которая допускает построение семантики типа Крипке и многообразие шкал которой характеризуется условиями, выразимыми в языке первопорядковой логики. В настоящее время выделилось целое направление в разработке теоретико-доказательственных методов, связанное с добавлением к формулам особых меток, имеющих семантический смысл (labelled deduction systems). Думается, что предлагаемый метод укладывается в русло этого развивающегося направления.

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

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

Можно поставить ряд задач для дальнейшей работы. В первую очередь, хотелось бы исследовать вопрос о применимости изложенного в работе метода для построения аналитических таблиц для систем временной логики с двухместными временными операторами типа Until и Since. Временные логики с такими модальностями привлекают внимание исследователей в силу широких выразительных возможностей языков, обогащенных двухместными модальностями. Другая область применения метода — многомерные модальные логики. Такие модальные логики содержат в языке модальности различных типов. Например, временная логика параллелизма, описанная в работе М. Рейнольдса [53], строится на базе временной модальности логики Lin линейного времени и обычной 55 - модальности. Разрешающий алгоритм, основанный на методе мозаик (см. также статью [38]), оказывается весьма сложным. Было бы интересным исследовать вопрос, нельзя ли в этом случае разрабатывать разрешающий алгоритм на базе аналитических таблиц? В той же работе [53] указывается, что как примеры двумерных логик могут быть рассмотрены и временные логики исторической необходимости (см. работы Д. Берджеса [11] и А. Занардо [61]). Родственные им системы — это логики CTL и CTL* в прикладных логиках для компьютерных наук. Однако, существующие аналитические таблицы для систем CTL и CTL* используют аппарат ц - исчисления и имеют ряд семантических ограничений. Думается, что разработка аналитико-табличных вариантов систем логики исторической необходимости является сложной, но интересной задачей.

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

Список научной литературыГригорьев, Олег Михайлович, диссертация по теме "Логика"

1. А.Т. Ишмуратов. Логический анализ временных контекстов. Киев, 1982.

2. В.А. Смирнов. Временные логики с разным отношением сопряженности // Модальные и интенсиональные логики. Москва, 1982.

3. В.А. Смирнов. Определение модальных операторов через временные // Модальные и интенсиональные логики и их применение к проблемам методологии пауки. М.: Наука, 1984.

4. A. Artosi and G. Governatori. Labelled model modal logic, 1994.

5. F. Baader and S. Tobies. The inverse method implements the automata approach for modal satisfability. In F. Baader and U. Sattler, editors, Automated Reasoning, IJCAR 2001, volume 2083 of LNAI, pages 92106. Springer Verlag, 2001.

6. D. Beckert. Depth-first proof-search without backtracking for free-variable clasual tableaux. Lournal of Logic and Computation, submetted.

7. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001.

8. N. Bonnett and R. Gore. Labelled seguents for prepositional tense logics. Technical Report TR-ARP-02-97, Automated Reasoning Project, Research School of Information Sciences and Engeneering, Australian National University, February,10 1997.

9. N. Bonnette and R. Gore. A labelled sequent system for tense logic Kt. In Australian Joint Conference on Artificial Intelligence, pages 71-82, 1998.

10. J. Burgess. Logic and time. Journal of Symbolic Logic, 44:566-582,1979.

11. C. Cerrato. Modal sequents for normal modal logics. Mathematical Logic Quartarly, 39:231-240, 1993.

12. C. Cerrato. Modal sequents. In H. Wansing, editor, Proof Theory of Modal Logic, pages 141-166. Kluwer Academic Publishers, Dordrecht, 1996.

13. H. B. Curry. The elimination theorem when modality is present. Journal of Symbolyc Logic, 17:249-265, 1952.

14. L. V. D. Basin, S. Mattews. Labelled propositional modal logics: Theory and practice. Lournal of Logic and Computation, 7:685-717, 1997.

15. K. Dosen. Sequent-systems for modal logic. Journal of Symbolyc Logic, 50:149-159, 1985.

16. M. Finger and D. Gabbay. Adding a temporal demension to a logical system. Journal of Logic Language and Information, 1:203-233, 1992.

17. M. Finger and D. Gabbay. Combining temporal logic systems. Notre Dame Journal of Formal Logic, 37(2):204-232, 1996.

18. M. Fitting. Intuitionistic Model Theory and Forcing. North Holland Pub. Co., Amsterdam, 1969.

19. M. Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, 13:237-247, 1972.

20. M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983.

21. D. Gabbay. Labelled Deductive Systems. Oxford University Press, 1996.

22. G. D. Giacomo and F. Massacci. Combining deduction and model checking into tableaux and algorithms for converse-PDL. Information and Computation, 162(1-2):117-137, 2000.

23. L. Goble. Gentzen systems for modal logics. Notre Dame Journal of Formal Logic, 15:455-461, 1974.

24. R. Gore. Cut-Free Sequent and Tableau Systems for Propositional Normal Modal Logics. PhD thesis, University of Cambridge, Computer Laboratory, 1992.

25. R. Gore. Tableaux methods for modal and temporal logics. In M. D'Agostino, D. Gabbay, R. Heahnlc, and J. Posegga, editors, Handbook of Tableau Methods, pages 297-396. Kluwer Academic Publishers, Dordrecht, 1999.

26. G. Governatori. On the relative complexity of labelled modal tableaux. In R. Gore, A. Leitsch, and T. Nipkov, editors, IJCAR-2001 Short Paper, pages 44-53. University of Vienna, 2001.

27. E. Gradel. Why are modal logics so robustly decidable?

28. S. Kanger. Provability in logic. Stocholm Studies in Philosophy. Almqvist and Wiskell, University of Stocholm, Sweden, 1957.

29. S. Kripke. A completeness theorem in modal logic. Journal of Symbolyс Logic, 24:1-14, 1959.

30. S. Kripke. Semantical analysis of modal logic I: normal prepositional calculi. Zeitschrift filr Matematische Logic und Grundlagen der Mathematic, 9:67-96, 1963.

31. S. Kripke. Semantical considerations on modal logic. Acta Philosophica Fennica, 16:83-94, 1963.

32. M. Lange and C. Stirling. Model checking games for CTL*. In Proc. Int. Conf. on Temporal Logic, ICTL'2000, Leipzig, Germany, 2000.

33. M. Lange and C. Stirling. Focus games for satisfiability and completeness of temporal logic. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LIGS'01, Boston, MA, USA, 2001. IEEE Computer Society Press.

34. D. Makinson. On some cmpleteness theorems in modal logic. Zeitschrift filr Matematische Logic und Grundlagen der Mathematic, 12:379-384, 1966.

35. S. Martini and A. Masini. A computational interpretation of modal proofs. In H. Wansing, editor, Proof Theory of Modal Logic, pages 141— 166. Kluwer Academic Publishers, Dordrecht, 1996.

36. M. Marx, S. Mikulas, and M. Reynolds. The mosaic method for temporal logics. In R. Dyckhoff, editor, Proceedings of International Conference TABLEAUX-2000, volume 1847 of LNAI, pages 324-340. Springer Verlag, 2000.

37. M. Marx and Y. Venema. Local variations on a loose theme: modal logic and decidability. In Finite Model Theory and its Applications. Spinger Verlag, forthcoming.

38. A. Masini. 2-Sequent calculus: a proof theory of modalities. Annals of Pure and Applied Logic, 58:229-246, 1992.

39. F. Massacci. Strongly analitic tableaux for normal madal logics. In A. Bundy, editor, Proceedings of CADE-94, volume 814 of LNAI, pages 149-184. Springer Verlag, 1994.

40. F. Massacci. Simplification with renaming: a general proof technique for tableau and sequent-based provers. Technical Report 424, Computer Laboratory, University of Cambridge, UK, 1997.

41. F. Massacci. Efficient Approximate Deduction and an Application to Computer Security. PhD thesis, Universita degli Studi di Roma La Sapienza, Italy, 1998.

42. F. Massacci. Simplification, a general constraint propagation technique for propositional and modal tableaux. In H. de S warts, editor, Proc. of the Internat. Conf. on Analytic Tableaux and Related Methods TABLEAVX-98, LNAI. Springer Verlag, 1998.

43. F. Massacci. Single step tableaux for modal logics. Technical Report TR-04-98, Departamento di Informatica e Sistemistica, Universita di Roma La Sapienza, Italy, 1998.

44. G. Mints. Cut-free calculi of the S5 type. In Studies in constructive mathematics and mathematical logic. Part II. Seminars in Mathematics, volume 8, pages 79-82. 1970.

45. H. Nishimura. Combinations of tense and modality. In Publications of the research institute for mathematical sciences, volume 16, pages 343353. Kyoto University, 1980.

46. M. Ohnishi and K. Matsumoto. Corrections to our paper "gentzen method in modal calculi Iм. Osaka Mathematical Journal, 10:147, 1957.

47. M. Ohnishi and K. Matsumoto. Gentzen method in modal calculi I. Osaka Mathematical Journal, 9:113-130, 1957.

48. M. Ohnishi and K. Matsumoto. Gentzen method in modal calculi II. Osaka Mathematical Journal, 11:115-120, 1959.

49. A. Prior. Time and Modality. Clarendon Press, Oxford, 1957.

50. A. Prior. Past, present and future. Clarendon Press, Oxford, 1967.

51. M. Raynolds. A decidable temporal logic of parallelism. Notre Dame Journal of Formal Logic, 38(3):419-437, 1997.

52. G. Sabmin and S. Valentini. The modal logic of provability, the sequential approach. Journal of Philosophical Logic, 11:311-342, 1982.

53. G. Shvarts. Gentzen style systems for K45 and K45d. In A. Meyer and M. Taitslin, editors, Logic at Botic '89, volume 363 of LNCS, Berlin, 1989. Springer-Verlag.

54. R. Smallian. First Order Logic. Springer Yerlag, 1968. Republished by Dover, 1995.

55. M. Takano. Subformula property as a substitute of cut-elimination in modal propositional logics. Mathematica Japonica, 37:1129-1145, 1992.

56. R. Thomason. Combinations of tense and modality. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Vol II: Extensions of Classical Logic, pages 135-165. Reidel, 1984.

57. M. Vardi. Why is modal logic so robustly decidable? In DIM ACS Series in Discrete Mathematics and Theoretical Computer Science, volume 31, pages 149-184. American Math. Society, 1997.

58. H. Wansing. Displaying Modal Logic, volume 3 of Trends in Logic. Studia Logica Library. Kluwer Academic Publishers, 1998.

59. A. Zanardo. Branching-time logic with quantification over branches: The point of view of modal logic. Journal of Symbolic Logic, 61:1-39, 1996.

60. J. J. Zeman. Modal Logic. The Lewis-Modal Systems. Clarenden Press, Oxford, 1973.