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

• Григорьев, Олег Михайлович
• кандидат философских наук
• 2004

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

Введение

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

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

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

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

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

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

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

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

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

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

Введение диссертации (часть автореферата) на тему «Аналитико-табличная формализация систем временной логики»

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

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

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

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.