автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.01, диссертация на тему:Реализация обратного метода установления выводимости для модальной логики КТ

ВВЕДЕНИЕ

Актуальность задачи поиска вывода для неклассических логик

Постановка задачи

Обзор родственных работ

Структура работы

ГЛАВА I. ОБЩАЯ СХЕМА ОБРАТНОГО МЕТОДА ДЛЯ

ЛОГИЧЕСКОЙ СИСТЕМЫ КТ

1.1. Вводные замечания

1.1.1. Семантика и синтаксис модальной логики знания

1.1.2. Мультимножества и исчисление секвенций

1.2. Общая схема метода 27 1.3 Прямое и обратное исчисления секвенций для логики знания

ГЛАВА II. ИСЧИСЛЕНИЕ ПУТЕЙ

2.1. Прямое исчисление путей

2.2. Обратное исчисление путей

ГЛАВА III. АНАЛИЗ ИЗБЫТОЧНОСТЕЙ

3.1. Свойства исчисления путей

3.2. Теорема полноты обратного метода с критериями избыточности

3.3. Ф-упорядочение

3.4. Теорема полноты обратного метода для обратного исчисления путей без секвенций, относящихся к 'V'

3.5. Предпосылка

3.6. Общий алгоритм установления выводимости

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

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

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

АКТУАЛЬНОСТЬ ЗАДАЧИ ПОИСКА ВЫВОДА ДЛЯ НЕКЛАССИЧЕСКИХ

ЛОГИК

Большинство из известных алгоритмов поиска вывода основано на теореме Эрбрана [Herbrand 1930], которая формулирует некоторые необходимые и достаточные условия выводимости формулы для классического исчисления предикатов первого порядка. Использование этих условий облегчает автоматизацию поиска вывода. Тем не менее, при практической реализации по теореме Эрбрана процесса установления выводимости целевой формулы происходит, как правило, порождение большого числа излишних дизъюнктивных членов. В результате процесс удлиняется (экспоненциально) и для доказательства сравнительно простых утверждений требуется слишком много машинного времени.

Указанная проблема решается введением разнообразных критериев, позволяющих избавиться от избыточных дизъюнктивных членов. Различные методы, сокращающие поиск доказательства рассматриваются, например, в таких работах, как [Davis 1962], [Robinson 1964], [Friedman 1963]. Наиболее известным и получившим дальнейшее распространение из предлагаемых в этих работах методов является метод резолюций [Robinson 1964], предложенный Д.А.Робинсоном.

Одновременно с методом резолюций и независимо от него С.Ю. Масловым был предложен т.н. обратный метод поиска вывода [Маслов 1964]. Последний дает возможность, целенаправленно, опираясь на конкретные особенности доказуемой формулы, ограничить перебор, возникающий при непосредственном применении теоремы Эрбрана и получить вывод более экономным способом, что позволяет экономить вычислительные ресурсы.

На данный момент существует целый ряд реализаций программ автоматического поиска доказательств для неклассических логик, основанных, как правило, на методе резолюций или его модификациях. Они описаны в следующих статьях: [Giuchinglia et al. 1998], [Tachella 1999], [Giimchinglia et al. 1999], [Hustadt and Shmidt 1997], [Weidenbach et al. 1996], [Horrocks and Patel-Schneider 1998] и [Horrocks 1998]. Наболее эффективная программа автоматического поиска доказательства, основанная на обратном методе - система К-обратное К - реализована лишь недавно А. Воронковым [Voronkov 1999].

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

Помимо этого существует несколько работ, посвященных реализации обратного метода для таких неклассических логик, как S4, линейной и интуиционистской логики ([Mints 1993], [Tammet 1994], [Tammet 1996] и [Mints at al. 1996]). В [Voronkov 1992] приведена общая схема обратного метода для неклассических логик.

До сих пор не была рассмотрена такая важная неклассическая система, как КТ или логика знания. В ней модальный оператор □ принимает значение "известно". Такая трактовка оператора □ позволяет говорить о широком спектре применимости экспертных систем, логической моделью машины вывода которых является логика КТ.

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

Как уже отмечалось, в настоящее время существует ряд программ автоматического поиска доказательства, в основе большинства из которых лежат традиционные методы резолюций, семантических таблиц, а также различные их модификации. Лучшие из этих систем, такие как *SAT или DLP, ориентированы на тот или иной класс формул; они постоянно улучшаются путем добавления различных стратегий и эвристик, что позволяет говорить об их практической применимости. Программы автоматического поиска доказательства, основанные на обратном методе, начали интенсивно разрабатываться лишь в последние несколько лет, однако уже сейчас они успешно конкурируют с традиционными, о чем говорят результаты экспериментов проведенных с системой К [Voronkov 2001].

Постановка задачи

Сформулируем описанную выше проблему более подробно.

Пусть Ф - некоторая формула модальной логики КТ. Основной задачей, которую призвана решить эта работа, является получение ответа на вопрос: «Выводима ли Ф в КТ, т.е. существует ли опровержение ее отрицания в соответствующем исчислении секвенций KTSeq?»

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

• Построение алгоритма установления выводимости для произвольной формулы модальной логики знания.

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

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

• Построение исчислений путей, кодирующих вывод в базовых исчислениях KTSeq и КТФ1пу. Мы обозначаем их KT°Path и КТФ1Р соответственно. Эти исчисления вводятся для того, чтобы сделать поиск доказательства более наглядным и удобным для практического применения.

• Доказательство теорем полноты для КТфРаЙ1 и КТФ1Р, гарантирующих невыполнимость формулы Ф логики знания в том и только том случае, когда пустой путь s выводим в исчислении путей KT°Path, или соответственно, в обратном исчислении путей КТФ]Р.

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

• Изучение исчисления KT°Path, с целью поиска его свойств, которые бы позволили избавиться от избыточных секвенций в пространстве поиска вывода.

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

• Доказательство теоремы полноты для исчисления путей без избыточных секвенций КТФ'*!Р

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

• Доказательство теоремы полноты для исчисления путей без избыточных ветвей дерева вывода формулы Ф в КТФ'

• Описание стратегии сокращения пространства поиска вывода, основанной на понятиях предпосылки и префиксной предпосылки.

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

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

Обзор родственных работ

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

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

Эта идея поиска доказательства от аксиом была впервые высказана в [Gentzen 1934]. В этой работе Генцен показал, как доказать разрешимость интуиционистской пропозициональной логики, используя поиск снизу вверх в исчислении секвенций. Доказательство основывалось на свойстве подформульности. К сожалению работа [Gentzen 1934] осталась незамеченной на довольно долгое время.

Всеобщий интерес к обратному методу установления выводимости появился в связи с серией работ С.Ю. Маслова и группы математической логики ЛОМИ АН СССР: [Маслов 1964], [Маслов 1966], [Маслов 1967], [Маслов 1968], [Маслов 1969], [Давыдов и др. 1969], [Маслов 1971], и [Маслов 1972].

Сам термин "обратный метод" был введен С.Ю. Масловым в 1964 году в работе [Маслов 1964]. В этой работе автором был разработан метод установления выводимости для формул классического исчисления предикатов без равенства и функциональных символов. В этой работе не использовалась скулемизация и метод был разработан для применения к формулам вида: 8,

Qixi ■•• QnXn(va dij) i y=i где QtXi . Qnxn - кванторный префикс, a Dij - дизъюнкции литер. В [Маслов 1964] не используется исчисление секвенций и свойство подформульности, а доказательства опираются на теорему Эрбрана. В этой работе С.Ю. Маслов показал, как применить обратный метод для установления разрешимости классов формул, в частности класса формул вида

V*3*V*(va Dij)

1=1 ./=] где 5] < 2, ., 5Ц < 2. Этот класс формул в дальнейшем получил название Масловский класс формул ([Borger, Grader and Gurevich 1997]).

В [Маслов 1966] автор применяет обратный метод для доказательства разрешимости нескольких классов формул классического исчисления предикатов первого порядка универсальным способом.

В [Маслов 1967] описывается реализация обратного метода к произвольным формулам с функциональными символами.

В [Маслов 1969] описаны аналогии между обратным методом и методом резолюций.

В работе [Маслов 1971] обратный метод обобщается на исчисление предикатов с равенством.

Наконец, в работе [Маслов 1968] сформулирована общая схема обратного метода, как результат выявления основных черт конкретных его вариантов для нескольких ранее рассмотренных логических исчислений. Эта работа является, в некоторой степени, обобщающей в серии работ Маслова, поэтому рассмотрим ее более подробно.

Общая схема обратного метода заключается в следующем. Для данного произвольного исчисления секвенций генценовского типа G, обладающего свойством подформульности, и произвольной секвенции Е в языке этого исчисления, автор описывает принципы построения «исчисления благоприятных Е-наборов». Выводимые объекты этого исчисления -благоприятные Е-наборы - представляют собой некоторое подмножество синтаксически определяемого множества объектов, так называемых Е-наборов, в терминах которых и формулируется это исчисление. Выводимость в исчислении благоприятных наборов простейшего объекта последнего рода, -так называемого пустого Е-набора, - гарантирует выводимость исходной секвенции Е в исчислении G. С другой стороны, из выводимости Е в G следует благоприятность пустого Е-набора. Таким образом проблема выводимости секвенции Е в исходном исчислении сводится к проблеме выводимости благоприятного пустого Х-набора.

Отметим также, что понятие набора формируется по этапам. Х-наборы автор интерпретирует как некоторые списки формул (входящих в ветви деревьев поиска вывода секвенции Z) вместе с зависимостями, связывающими формулы этих списков. Для выделения интересующих подформул секвенции £ вводится понятие разбивки и понятие системы зависимостей, дающее язык для выражения именно тех зависимостей, которые нас интересуют.

В работе [Минц 1981] обратный метод был впервые применен к неклассическим пропозициональным логическим исчислениям, правда под названием "резолюции".

В [Воронков 1985] впервые появляется другая формулировка обратного метода. В этой работе обратный метод рассматривается для классической логики без равенства на основе обратного исчисления свободных переменных.

В 1992 году, в работе [Voronkov 1992] появляется описание обратных исчислений свободных переменных для неклассических предикатных логик.

Метод свободных переменных для классической логики с равенством был введен в работе [Degtyarev and Voronkov 1995]. В этой же работе рассматривается ряд критериев избыточности, в том числе и критерий, основанный на отношении упорядочивания.

Реализация обратного метода для предикатной интуиционистской логики описана в работе [Tammet 1996].

Исчисление путей было впервые введено А. Воронковым в 2000 году в работе [Voronkov 2000].

14

СТРУКТУРА РАБОТЫ

Работа построена следующим образом. В главе I вводятся основные определения и факты из теории неклассических исчислений и теории поиска вывода. В этой же главе приводится общая схема реализации метода для логики знания и строятся базовые исчисления обратного метода. В последнем параграфе главы формулируется и доказывается теорема полноты для исчисления KT°inv.

ЗАКЛЮЧЕНИЕ

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

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

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

3. Были исследованы свойства построенного исчисления путей, на основании которых предложены строгообоснованные стратегии сокращения поиска вывода в системе КТ.

4. Была предложена и теоретически обоснована стратегии, основанная на Ф-упорядочении, определяющая эффективную последовательность применения правил вывода к дизъюнктам из пространства поиска вывода.

5. Были предложены и теоретически обоснованы эффективные стратегии для системы КТ, подобные стратегиям предпосылки для логики К, позволяющие заметно сокращать пространство поиска вывода уже процессе порождения дизъюнктов.

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

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

Теоретическая и практическая ценность работы, на наш взгляд, заключается в следующем:

1. Было проведено глубокое исследование базовых исчислений обратного метода системы КТ и соответствующих им исчислений путей.

2. Был детально описан и теоретически обоснован механизм вывода для экспертной системы, база знаний которой формализована с помощью семантически довольно богатого языка модальной логики КТ.

3. Были предложены эффективные и технически легко реализуемые стратегии для системы КТ, сокращающие пространство поиска вывода уже в процессе пополнения базы данных дизъюнктов.

Описанный в данной работе метод поиска доказательства, по-видимому, применим и к некоторым другим неклассическим логикам. Несложно будет реализовать описанный выше метод на такие модальные системы, как KD, KB, S4, S5. Большинство доказательств для этих систем можно проводить аналогично рассмотренным в работе методами. Более интересным продолжением работ по рассматриваемой теме является расширение

93 применимости обратного метода на такие семантически богатые логики, как мультимодальные и темпоральные.

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

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

1. Барвайс Дж. Справочная книга по математической логике. - М.: Наука. -1983.

2. Воронков А.А. Метод поиска доказательства//Вычислительные системы. Новосибирск. 1985. - т. 107

3. Давыдов Г.В., Маслов С.Ю. и др. Машинный алгоритм установления выводимости на основе обратного метода// Записки ЛОМИ АН СССР. -1969. т.16. - С.8-20

4. Драгалин А.Г. Математический интуиционизм. Введение в теорию доказательств. -М.:Наука. 1979.

5. Маслов С.Ю. О поиске вывода в исчисленьях общего типа// Записки ЛОМИ АН СССР. 1972. - т.32. - С.59-65

6. Маслов С.Ю. Обобщение обратного метода на исчисление предикатов с равенством// Записки ЛОМИ АН СССР. 1971. - т.20. - С.80-96

7. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений// Труды Математического института АН СССР. 1968. -T.XCVIII. - С.26-87

8. Маслов С.Ю. Связь между тактиками обратного метода и метода резолюций// Записки ЛОМИ АН СССР. 1969. - т. 16. - С.21 -26

9. Маслов С.Ю. Стратегии в резолютивном и обратном методе./

10. Математическая логика и автоматическое доказательство теорем. М.: Наука.- 1983.- С. 327-332

11. Ю.Маслов С.Ю., Минц Г.Е. Теория поиска доказательств и обратный метод/ Математическая логика и автоматическое доказательство теорем. М.: Наука,- 1983.- С. 291-314

12. Маслов С.Ю. Обратный метод установления выводимости в классическом исчислении предикатов// ДАН СССР. 1964. - вып.159, №1. - С. 17-20

13. Маслов С.Ю. Обратный метод установления выводимости для непредваренных формул исчисления предикатов// ДАН СССР. 1967. -№1. - С. 22-25.

14. Маслов С.Ю. Применение обратного метода к теории разрешимых фрагментов классических исчислений// ДАН СССР. 1966. - №1. - С. 1720.

15. Н.Мендельсон Э. Введение в математическую логику. М.: Наука. - 1976.

16. Минц Г.Е. Резолютивные исчисления для неклассических логик//9-ый Советский Кибернетический симпозиум, М.: ВИНИТИ. 1981.- т.2. -С.34-36

17. Фейс Р. Модальная логика. М.: Наука. - 1974.

18. Auffray I., Enjalbert P., Hebrard J.-J. Strategies of modal resolution: Results and problems// Journal of Automated Reasoning 1990 - vol.9 - pp. 1-38

19. Baader F., Hollunder B. A terminological knowledge representation system with complete inference algorithm's// PDK'91, Boley H. And Richter M. Eds.,1.cture Notes in Artificial Intelligence. 1991. - vol.567, Springer Verlag. -pp.67-86

20. Bachmair L. Gansinger H. Resolution theorem proving// Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000

21. Borger E., Grader E. and Gurevich Y. The Classical Decision Problem, Springer Verlag 1997

22. Bowen K. Model Theory for Modal Logics// Synthese Library 1979 - vol.128

23. Calvanese D., De Giacomo G., Lenzerini M., Nardi D. Reasoning in expressive description logics// Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000

24. Catach L. Tableaux: a general theorem prover for modal logics// Journal of automated reasoning. 1991. - vol.7, №4. - pp.489-510

25. Chagrov A., Zakharyaschev M. Modal Logic 1996 - Oxford University Press

26. Curry H. Foundations of Mathematical Logic 1963 - McGraw-Hill, New-York

27. Davis M. Eliminating the Irrelevant from Mechanical Proofs// Proc. Symp. On Experimental Arithmetic, Chicago, 1962.

28. Degtyarev A. And Voronkov A. Equality elimination for the inverse method and extension procedures// UPMAIL Technical Report 92, Uppsala University, Computing Science Department 1994b

29. Degtyarev A. And Voronkov A. Equality elimination for the inverse method and extension procedures// Proc. International Joint Conference on Artificial Intelligence (IJCAI), C. Mellish ed., Montreal. 1995. - vol.1. - pp.342-347

30. Degtyarev A. And Voronkov A. The undecidability of simultaneous rigid E-unification// Theoretical Computer Science 1996. - vol.166, №1-2. - pp.291300

31. Fitting, M. First Order Logicand Automated Theorem Proving. 1996 -Springer Verlag, New-York, Second Edition

32. Fitting, M. Proof methods for modal and intuicionistic logics// Synthese Library, Reidel Pub. Сотр. 1983. - vol. 169.

33. Fitting, M., Mendelsohn R. First-Order Modal Logic 1998 - Kluwer Academic Publishers

34. Fitting, M., Thalmann L., Voronkov A. Term-modal logics// Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX2000), Dyckhoff R. Ed. Lecture Notes of Artificial Intelligence, Springer Yerlag 2000 - vol. 1847 - pp.220-236

35. Friedman J. A. Semi-decision procedure for the functional calculus// Journal of ACM. 1963.-vol. 10, №1. - pp. 1-25

36. Gentzen, G. Untersuchungen uber das logische Schliesen// Mathematical Zeitschrift-39. 1934. - pp.176-210, 405-431

37. Girard J.-Y., Lafont Y., Taylor P. Proofs and types 1989 - Cambridge University Press

38. Giuchinglia F. et al. More evaluation of decision procedures for modal logics//Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR'98), A. Cohn, L. Schubert and

39. S. Shapiro Eds. Morgan Kaufmann San Francisco, CA. 1998. - pp.616-635

40. Giuchinglia F. et al. SAT-based decision procedures for classical modal logics// Journal of automated reasoning. 1999. To appear in the Special Issues: Satisfiability at the start of the year 2000. (SAT 2000)

41. Giuchinglia F., Sebastiani R. Building decision procedures for modal logics from propositional decision procedure: Case study of modal К// CADE-13, M.McRobbie and J.Slaney, Eds. Lecture Notes in Computer Science 1996a. -vol.1104.-pp.583-597

42. Giuchinglia F., Sebastiani R. SAT-based decision procedure for ALS// KR'96 -1996b-pp. 304-314

43. Goble L. Gentzen system for modal logic// Notre Dame Journal of Formal Logic 1974-vol.15-pp.455-461

44. Goldblatt, R. Logics of time and Computation// Lecture Notes, Center for the Study of Language and Information. 1987. - №7

45. Haarslev V., Moller R., Turhan A.-Y. Implementing in ALSRP(D) A Box Reasoner-progress report// Proc. DL'98 International Descriptional Logic Workshop -1998

46. Herbrand J. Recherches sur la theorie de la demonstration. Warsaw, 1930.

47. Horrocks I. and Patel-Schneider P. Optimizing description logic subsumption// Journal of Logic and Computation 1999 - vol.9(3) - pp. 267-293

48. Horrocks I. Optimizing tableaux decision procedure for modal logic// Ph.D. thesis University of Manchester. 1997

49. Horrocks I., Patel-Schneider P., Sebastiani R. An analysis on empirical testing for modal decosion procedures// Logic Journal of the IGPL 2000 - vol. 8, №3 -pp. 293-323.

50. Hustadt U. and Shmidt R. On evaluating decision procedures for modal logic// IJCAI-97. 1997. - vol. 1. - pp.202-207

51. Kanger S. A simplified proof method for elementary logic// Automated of Reasoning. Classical Papers of Computational Logic, Siekmann J., Wrightson G. Eds., Springer Verlag- 1983 vol.1 - pp. 364-371

52. Kripke S.A. Semantical considerations on modal logic// Reference and Modality, Oxford University Press, London. 1971. - pp. 63-72

53. Kuechner D. A note on the relation between resolution and Maslov's inverse method// Machine Intelligence, Melzer В., Michie D. Eds., American Elsiver -1971 vol.6-pp.73-76

54. Lifschitz V. What is the inverse method?// Journal of Automated reasoning -1989 vol.5(1) - pp.1-23

55. Mints G. Resolution calculus for the first order linear logic// Journal of Logis, Language and Information. 1993. - №2. - pp.58-93

56. Mints G. Resolution strategies for intuitionistic logic// Constraint Programming. NATO ASI Series F. Springer Verlag 1994 - pp. 289-311

57. Mints G., Orevkov V. And Tammet T. Transfer of sequent calculus strategies to resolution for S4// Proof Theory of Modal logic. Studies in Pure and Applied logic, Kluwer Academic Publishers. 1996

58. Mints G., Voronkov A. And Degtyarev A. Inverse method.// Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000

59. Niewenhuis R., Rubio A. Paramodulation-based theorem proving// Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000

60. Patel-Schneider P. DLP-system description// Proc. DL'98 International Descriptional Logic Workshop -1998 pp. 87-89

61. Robinson J.A. On automatic deduction// Rice Univ. Studies. 1964. - vol.50, №1. - pp. 69-89.

62. Schmidt R. Resolution in a decision procedure for many propositional modal logics// Advances in Modal Logics, Kracht M., de Rijhte M., Zakharyaschev M. Eds., Lecture Notes, CSLI Publications 1998 - vol. 87 - pp. 189-208

63. Tachella A. *SAT system description// Proceedings of the 1999 International Description Logic Workshop (DL'99), P.Lambrix, A.Borgida, M.Lenzerini, R.Moller and P.Pattel-Schneider, Eds. CEUR-WS. 1999. - vol.22, - pp. 142144

64. Tammet T. A resolution theorem prover for intuitionistic logic//CADE-13, M.McRobbie and J.Slaney, Eds. Lecture Notes in Artificial Intelligence. -1996. vol.1104, Springer Verlag. - pp.2-16

65. Tammet T. Proof strategies in linear logic// Journal of automated reasoning. -1994. vol.12, №3. - pp.273-304

66. Tammet T. Resolution theorem prover for intuitionistic logic// CADE-13, M.McRobbie and J.Slaney, Eds. Lecture Notes in Computer Science 1996. -vol.1104.-pp.2-16

67. Voronkov A. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi// LICS'2000

68. Voronkov A. Theorem-proving in non-standard logic based on the inverse method//! 1th International Conference on Automated Deduction, D. Kapur ed.1021.cture Notes in Artificial Intelligence. 1996. - vol.607, Springer Verlag. -pp.648-662

69. Voronkov A. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi// ACM Transactions and Computational logic. 2001. - vol. 1. - pp. 1-35

70. Voronkov, A. K-inverse-K: a theorem prover for K// Automated Deduction. CADE-16, International Conference on Automated Deduction, H.Ganzinger Eds. Lecture Notes in Artificial Intelligence. 1999. - vol.1632, Springer Verlag.- pp.3 83-3 87

71. Wallen, L. Automated deduction in nonclassical logics. The MIT Press. -1990

72. По результатам разработанного спецкурса написано учебное пособие «Логический вывод в дедуктивных системах» в объеме 24 стр., утвержденное Ученым советом ММФ ТГУ к печати в 2001 г.

73. Диссертационные результаты используются, также, при выполнении курсовых и дипломных работ студентов.

74. Декан механико-математического факультета, к.ф.-м.н., доцент

75. Зав.кафедрой вычислительной математики и компьютерного моделирования, доцент1. Щербаков Н.Р.1. Берцун В.Н.