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

• Антонова, Ольга Аркадьевна
• доктор философских наук
• 2005

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

Введение.

Глава I. Теория логического вывода и табличный метод

1.1. Табличный метод и его история развития.

1.2. Аксиоматический и табличный методы доказательства.

1.3. Натуральный вывод и табличный метод.

1.4. Связь табличного и секвенциального методов доказательства.

Глава II. Табличные конструкции и их применение в классической логике

II.1. Семантический период развития табличного метода. Семантические таблицы Э. Бета и модельные множества

Я. Хинтикки.

II.2. Аналитический период развития табличного метода.

П.2.1. Аналитические таблицы Р. Смаллиана.

II.2.2. Таблицы Фитгинга.

Глава III. Табличные методы в неклассических логиках

III. I. Методы логического вывода и таблицы в интуиционистской логике

Ш.1.1. Теоретический анализ методов логического вывода в интуиционистской логике (аксиоматический, натуральный и секвенциальный вывод) ГОЛ. 1.1. Аксиоматические системы интуиционистской логики.

Ш.1.1.2. Натуральный вывод в интуиционистской логике.

Ш. 1.1.3. Секвенциальные системы интуиционистской логики.

III. 1.2. Табличные методы в интуиционистской логике. Семантические таблицы Бета для систем интуиционистской логики.

П1.1.3. Аналитические таблицы для систем интуиционистской логики.

П1.1.4. Усовершенствованная табличная система Мильоли

Москато-Орнаги.

1П.1.5. Расширение табличного метода для интуиционистских логик на модальные системы. Системы Авеллоне-Феррари.

Ш.2.Табличные методы в модальной логике

III.2.1. Теоретический анализ методов логического вывода в системах модальной логики (аксиоматический, натуральный и секвенциальный вывод)

Ш.2.1.1. Аксиоматические варианты систем модальной логики.

Ш.2.1.2. Натуральный вывод в модальной логике.

Ш.2.1.3. Секвенциальные системы модальной логики.

1П.2.2. Семантический анализ модальной логики методом таблиц. Семантические таблицы Крипке и модельные множества Хинтикки.

1П.2.3. Табличные методы Фитгинга для модальной логики.

III.3. Применение табличных методов в многозначной логике

Ш.3.1. Теоретический анализ методов логического вывода в многозначной логике (аксиоматический, секвенциальный)

Ш.3.1.1. Системы гильбертовского типа в многозначной логике.

Ш.3.1.2. Секвенциальные системы многозначной логики.

III.3.2. Табличные методы в многозначной логике. Аналитические таблицы для систем многозначной логики.

Ш.3.3. Табличный метод Карниелли. Систематизация конечнозначных логик через метод таблиц.

Ш.3.4. Оптимизация табличного метода Карниелли.

Таблицы для множеств-знаков Хэнла.

III.3.5. Расширение табличного метода для конечнозначных логик на системы интуиционистской логики. Система Баса-Фермюллера.

Ш.4. Методы логического вывода и таблицы в релевантной логике.

Ш.4.1. Теоретический анализ методов логического вывода в релевантной логике (аксиоматический, натуральный и секвенциальный вывод) Ш.4.1.1 Аксиоматические системы релевантной логики.

Ш.4.1.2. Системы натурального вывода в релевантной логике.

Ш.4.1.3. Генценовские логистические исчисления для релевантных систем.

Ш.4.1. Таблицы для систем релевантной логики

Ш.4.1.1. Таблицы для систем RM.

Ш.4.1.2. Таблицы для релевантных систем с мультипликативными связками.

Ш.4.1.3. Таблицы с индексированными формулами для релевантных систем.

Введение диссертации (часть автореферата) на тему «Современные проблемы использования табличных методов в логике»

История логики XX века во многом представляет собой историю развития теории логического вывода. Результатом развития теории логического вывода стали в настоящее время широко известные методы доказательства — аксиоматический, натуральный, секвенциальный и табличный.

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

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

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

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

Отсутствие систематического обзора истории развития табличного метода диктует необходимость данного исследования.

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

Степень разработанности темы.

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

В иностранной научной литературе ситуация сложилась существенно иная. Хотя исследований, которые прямо ставили бы своей целью всестороннее рассмотрение истории развития табличного метода, не существует, имеется большое количество работ посвященных различным этапам развития данного метода доказательства. Среди фундаментальных исследований, отметим работы Э.Бета, Дж.Земана, С.Кангера, С.Клини, Р.Смаллиана, М.Фиттинга, С. Лиса, С.Крипке.

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

Исследования Я. Хинтикки, С.Крипке, П.И.Быстрова, В.Н.Костюка, Н.Н.Непейводы, М.Фиттинга, Э.Бета, С.Кангера, Р.Горе, Ф.Массачи, А.Мазини, Т.Боргуиса, Р.Голдблатга, П.Уолпера посвящены проблемам применения табличного метода доказательства в различных системах модальной логики.

Работы У. Сакона, С.Сурмы, В.Карниелли, Д.А. Бочвара, В.К. Финна, М.Бааза, Г.Фермюллера, Р.Хэнла рассматривают вопрос наиболее эффективного использования метода таблиц в многозначной логике.

Среди работ посвященных применению метода таблиц в интуиционистской логике следует выделить работы Э.Бета, М.Фиттинга, М.Феррари, Р.Мильоли, Р.Дюкхоффа, С.Крипке,

A.Авеллоне, У.Москато, М.Орнаги.

Возможность использования табличного метода доказательства в релевантной логике рассматривалась в работах М. Мак-Робби, Н.Белнапа, П.И. Быстрова.

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

Среди работ, посвященных данной проблеме, отметим работы Э.Бета, Р.Попплестона, И.Кохена, Л.Триллинга, П.Венера, К.Брода, И.Шенфелда, Л.Валлена, С.Ривса, А.Авеллоне,

B.Москато, М.Орнаги, Ф.Массачи, П.Мильоли, П.Бонатги, Н.Бааз, Г.Фермюллер, Э.Эдера, JI. Уоллена.

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

Цель и задачи исследования.

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

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

Для достижения сформулированной цели автором решались следующие задачи исследования:

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

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

3. Проведение историко-логического анализа основных направлений и тенденций развития теории логического вывода на протяжении XX века.

4. Формирование представлений о наиболее эффективном методе логического вывода в рамках табличного метода доказательства.

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

6. Анализ новых решений традиционных логических проблем — табличное доказательство Теоремы полноты, Теоремы компактности, интерполяционной теоремы и Основной теоремы: оценка влияния табличного метода доказательства на возникновение новых методов доказательства в теории логического вывода.

7. Определение места и роли табличного метода доказательства в целом в истории теории логического вывода.

Методология исследования.

Автором использовались традиционные методы исследовательской работы: историко-логический анализ исследовательской литературы и сравнительный анализ различных концепций логического вывода.

Вместе с тем, в основу диссертационного исследования положены следующие теоретико-методологические принципы:

1. Исследование табличного метода доказательства как самостоятельного явления в теории логического вывода при одновременном рассмотрении его в контексте преобразования логической традиции (переходе от логик неклассического типа к логикам искусственного интеллекта).

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

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

Положения и выводы, выносимые на защиту:

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

2. Табличному методу доказательства соответствуют следующие хронологические рамки:

Начальный этап развития теории табличного метода доказательства — семантический этап, который составляют семантические таблицы Бета и модели Хинтикки.

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

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

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

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

4. В теории табличного метода доказательства произошло объединение двух путей развития теории логического вывода — синтаксического и семантического, которое не только изменило весь дальнейший ход развития методов логического вывода в XX в., но и продолжает воздействовать на структуру последующих форм доказательства. Табличные методы Бета, Смаллиана, Фиттинга, Лиса и др. являются одним из оснований, на которых строятся новые, более эффективные теории логического вывода.

5. Наибольшим вкладом табличного . метода доказательства в развитие теории логического вывода является: а. одно из главных преимуществ табличного вывода состоит в том, что в нем наиболее ярко выражается связь, существующая между семантикой и синтаксисом логического исчисления. Таким образом, именно табличный метод показывает нам те семантические связи, которые лежат в основании логической (синтаксической) структуры рассматриваемой логики. b. правила построения табличного вывода соответствуют способу обычных содержательных рассуждений, таким образом, выводы, полученные методом таблиц, оказываются более естественными, чем, выводы в рамках аксиоматического, натурального и секвенциального методов доказательства. c. в построении вывода с помощью табличного метода не участвуют более сложные формулы, чем исходная (доказываемая), и каждый шаг построения вывода детерминирован конечным числом альтернатив дальнейших логических шагов. d. процесс доказательства многих базовых теорем при использовании табличного метода упрощается.

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

Теоретическое и практическое значение.

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

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

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

Апробация исследования

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

Результаты работы представлялись автором в ходе различных научных форумов, среди которых:

1. Первый Общероссийский философский конгресс, Санкт-Петербург, июнь, 1997.

2. Современная логика: проблемы теории, истории и применения в науке, 5 Общероссийская научная конференция. Санкт-Петербург. 1998

3. Смирновские чтения: 2 Международная конференция, Москва, 1999

4. Современная логика: проблемы теории, истории и применения в науке, 6 Общероссийская научная конференция. Санкт-Петербург. 2000

5. Современная логика: проблемы теории, истории и применения в науке, 7 Общероссийская научная конференция. Санкт-Петербург. 2002

6. «Дни Петербургской философии», 15-16 ноября. Круглый стол «Философия науки и техники»2002.

7. Смирновские чтения: 4 Международная конференция, Москва, 2003

8. Конференция «Рациональность и вымысел». Санкт-Петербург, 12-14 ноября. 2003.

Основные положения диссертации отражены в публикациях автора.

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

Заключение диссертации по теме «Логика», Антонова, Ольга Аркадьевна

Заключение

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

Не вдаваясь в детали, мы дали только общий обзор того, как таблицы зарождались, как развивались и где они находятся сейчас. История таблиц, начиная свое существование с работ Г. Генцена, затем продолжает интенсивно развиваться в семантических исследованиях Э. Бета и Я. Хинтикки. С. Лис и Р. Смаллиан придают таблицам такую форму, что они становятся самым эвристичным методом доказательства. Таблицам становится тесно в рамках классической логики, и они распространяются на многие неклассические логики, параллельно развивая отношение с другими техниками доказательства и раскрывая тем самым возможности своей «автоматизации».

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

Хотя табличный метод был создан для логики и в логике, на настоящий момент область его применения значительно расширилась. Форма табличных систем, а именно анализ и опровержение, идеально подходят для построения алгоритмов доказательства теорем.

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

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

Л ч

Бекертом; С. Толедо предложил табличные системы для арифметики, которая использует со-правило; П. Эндрюс4 развил таблицы для теории типов; табличные построения для систем немонотонной логики были рассмотрены Н. Оливетги5.

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

1 Fitting М. Tableaux for logic programming // Journal of Automated Reasoning 13, 1994. P. 175—188.

2 Beckert B. Equality and other theories //Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht-Boston-London, 1999. P.197—254.

3 Toledo S. Tableau Systems for First Order Number Theory and Certain Higher Order Theories //Lecture Notes in Mathematics. V.447. Berlin, 1975.

4 Andrews P.B. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. 1986.

5 Olivetti N. Tableaux for nonmonotonic logics // Handbook of tableau methods. P.469—528.

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

Список литературы диссертационного исследования доктор философских наук Антонова, Ольга Аркадьевна, 2005 год

1. Aczel Р.Н. Some results on intuitionistie predicate logic // Journal of Symbolic Logic. Vol. 32. 1967. P. 113—115.

2. Anderson A.R., Belnap N.D. Entailment: The logic of relevance and necessity. Princeton, 1975.

3. Avelone A., Ferrari M. Almost Dublication-Free Tableau Calculi for Propositional Lax Logics // Theorem Proving with Analytic Tableaux and Related Methods. 5-th International Workshop, Tableaux 96. P. 75—89.

4. Avelone AMoscato V., Miglioli P., Ornaghi V. Generalized tableaux Systems for Intermediate propositional logics // Automated Reasoning with Analytic Tableaux and Related Methods. International Conference. Tableaux 97. P. 139—147.

5. Avron A. Natural 3-valued logics — characterization and proof theory // Journal of Symbolic Logic. Vol. 56 (1). 1991. P. 276—294.

6. Avron A. The method of hypersequents in proof theory of propositional non-classical logics. Tel Aviv University, 1994.

7. Baaz M., Fermuller C.G. Non-elementary Speedups between41.

8. Different Versions of Tableaux // Proceedings of Tableaux 95, 4 Workshop on Theorem Proving with Analytic Tableaux and Related Methods. 1995. P. 217—230.

9. Baaz M., Fermuller G. Combining Many-Valued and Intuitionistie Tableaux // Theorem Proving with Analytic Tableaux and Related Methods. 5-th International Workshop, Tableaux' 96. Italy, May 1996. P. 23—35.

10. Baaz M, Fermuller G. Combining many-valued and intuitionistic tableaux // Theorem proving with analytic tableaux and related methods. 5-th Intern. Workshop, 1996. P. 65—79.

11. Barth E. On natural deduction in modal logic with two primitives //Logiqueet Analyse. 12, 1969. P. 157—166.

12. Beckert В., Hahnle R. Analytic tableaux // Automated Deduction — A Basis for Applications. Vol.I/Ed. W.Bibel., P.H.Schmitt. 1998.

13. Beckert В., Hahnle R, Schmitt P. The even more liberalized 5-rule in free variable semantic tableaux // Computational Logic and Proof Theory, Proceedings of the 3rd Kurt Godel Colloquium, 1993. P. 108—119.

14. Beckert В., Rape C. Incremental theory reasoning methods for semantic tableaux // Proceedings of Tableaux 96, 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Palermo, 1996. P. 93—109.

15. Beckert В., Posegga J. LeanTAP: Lean tableau-based deduction // Journal of Automated Reasoning. Vol. 15 (3). 1995. P. 339—358.

16. Belnap N.DJr., Gupta A., Dunn J.M. A consecution calculus for positive relevant implication with necessity // Journal of Philosophical Logic. Vol. 9. 1980. P. 343—362.

17. Benthem J.F.A.K. The Logic of Time: a model-theoretic investigation into the varieties of temporal ontology and temporal discourse. Synthese library. Vol. 156. Dordrecht, 1983.

18. Beth E. W. Vexistence en mathematique. Paris, 1956.

19. Beth E.W. On machines which prove theorems // Simon Stevin Wissen-Natur-Kundig Tijdschrift 32,1958. P. 49—60.

20. Beth E.W. Semantic construction of intuitionistic logic // Mededelingen der Kon. Ned. Akad. Vol. Wet 19, 11. Amsterdam, 1956.

21. Beth E. W. Semantic entailment and formal derivability // Mededelingen der Kon. Ned. Akad. Vol. Wet. 18, 13. Amsterdam, 1955.

22. Beth E. W. The foundations of mathematics. Amsterdam, 1959. ll.Bibel W. Automated Theorem Proving. Vieweg, 1982.

23. Borghuis T. Interpreting modal natural deduction in type theory I I Diamonds and Defaults. 1993. P. 67—102.

24. BozicM., Dosen K. Models for normal intuitionistic modal logics // Studia Logica. Vol. 43. 1984. P. 217—245.

25. Broda K. The application of semantic tableaux with unification to automated deduction // Technical report, Department of Computing, Imperial College, 1992.

26. Broda K. The application of semantic tableaux with unification to automated deduction // Technical report, Department of Computing, Imperial College, 1992.

27. Broda K. The relation between semantic tableaux and resolution theorem proves // Tech. Rep. DOC 80/20, Imperial College of Science and Technology. London, Oct. 1980.

28. Burgess J. Basic tense logic // Handbook of Philosophical Logic. Vol. П: Extensions of Classical Logic /Ed. D.Gabbay, F.Guenthner. Dordrecht, 1984. P. 1—88.

29. Carnielli W.A. An algorithm for axiomatizing and theorem proving in finite many-valued prepositional logic // Logique et analyse. Vol. 28. № 112. Louvain, 1985. P. 363—368.

30. Carnielli W.A. Systematization of finite many-valued logics through the method of tableaux // Journal of Symbolic Logic. Vol. 52 (2). 1987. P. 473-493.

31. Catach L. TABLEAUX: A general theorem prover for modal logics // Journal of Automated Reasoning. Vol. 7.1991. P. 489—510.

32. Cerrito S., Mayer M. Hintikka Multiplicities in Matrix Decision Methods for Some Propositional Modal logics // Automated Reasoning with Analytic Tableaux and Related Methods. International Conference. Tableaux'97. P. 25—35.

33. Cook S.A. The complexity of theorem proving procedures // Proceedings of the 3rd Annual Symposium on the Theory of Computing, 1971.

34. D 'Agostino M. Tableaux methods for classical prepositional logic // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 45—123.

35. D Agostino M., Gabbay D, Broda K. Tableaux methods for substructural logics // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 397—467.

36. D 'Agostino M., Gabbay D. A generalization of analytic deduction via labeled deductive systems. Part 1: basic substructural logics // Journal of Automated Reasoning. Vol. 13. P. 243—281. 1994

37. Davis M. The prehistory and early history of automated deduction // Automation of Reasoning, /Ed. J. Siekman, G. Wrightson. New York, 1983. P. 1—28.

38. Davis M., Putnam H. A computing procedure for quantification theory // Automation of Reasoning /Ed. J. Siekman, G. Wrightson. New York, 1983. P. 125—139.

39. Dosen K. Sequent-systems for modal logic // Journal of symbolic logic. Vol. 50 (1). 1985. P. 149—168.

40. Dunn J.M. A «Gentzen system» for positive relevant implication // Journal of Symbolic Logic. Vol. 38. 1973. P. 356—357.

41. Dyckhoff R. Contraction—free segment calculi for intuitionistic logic // Journal of Symbolic Logic 57 (3). 1992. P. 111—118.

42. Eder E. An Implementation of a Theorem Prover based on the Connection Method // Artificial Intelligence Methodology Systems Applications. /Ed. W.Bibel, B.Petkoff. North Holland, 1985. P. 121—128.

43. Emerson E.A., Halpern J.Y. Decision procedures and expressiveness in the temporal logic of branching time // Journal of Computer and System Sciences. Vol. 30. 1985. P. 1—24.

44. Ferrari M, Miglioli P. Counting the maximal intermediate constructive logic // Journal of Symbolic Logic. Vol. 8 (4). 1993. P. 21—33.

45. Fisher M. A resolution method for temporal logic // Proceedings of 12th International Joint Conference on Artificial Intelligence 1991. Morgan-Kaufmann, 1991. P. 99—104.

46. Fitting M. An embedding of classical logic in S4 II Journal of Symbolic logic. Vol. 35. 1970. P. 529—534.

47. Fitting M. Intuitionistic Logic, Model theory and forcing. New York, 1969.

48. Fitting M. Model existence theorems for modal and intuitionistic logic // Journal of Symbolic Logic. Vol. 38. 1973 P. 213—218.

49. Fitting M. С. First-order modal tableaux I I Journal of Automated Reasoning 4. 1988. P. 191—213.

50. Fitting M.C. Intuitionistic Logic, Model Theory and Forcing. Amsterdam, 1997.

51. Fitting M.C. Tableau methods of proof for modal logics I I Notre Dame Journal of Formal Logic 13. 1972. P. 237—247.

52. Fitting M.C. Tableaux for logic programming // Journal of Automated Reasoning 13. 1994. P. 175—188.

53. Gale M. The philosophy of Time. New York. 1967.

54. Giambrone S. Gentzen systems and decision procedures for relevant logics // Bulletin of the section of logic. Warszawa; Lodz, 1982 (1983). Vol. 11 (3/4). P. 169—175.

55. Ginsberg M.L. Multi-valued logics // Computational Intelligence. Vol. 4 (3). 1988.

56. Goldblatt R.I. Logics of Time and Computation // Lecture Notes 7, Center for the Study of Language and Information. Stanford, 1987.

57. Gore R. Tableaux methods for modal and temporal logic // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 297—396.

58. Gough G. Decision procedures for temporal logics. Manchester, 1984.

59. Hahnle I. Automated Deduction in Multiple-Valued logics. New York. 1993.

60. Hahnle R. Tableaux for many-valued logics // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 529—580.

61. Hahnle R. Uniform notation of tableaux rules for multiple-valued logics // Proceedings International Symposium on Multiple-Valued Logic. Victoria, IEEE. 1991. P. 238—245.

62. Hintikka JForm and content in quantification theory // Acta Philosophica Fennica Two Papers on Symbolic Logic 8. 1955. P. 8—55.

63. Kawai H. Sequential calculus for a first-order infinitary temporal logic // Mathematical Logic Quarterly. Vol. 33. 1987. P. 423—432.

64. Kirin KG. Gentzen's method of the many-valued prepositional calculi // Zeitschrift fur mathematische logic und Grundlagen der Mathematik. Bd. 12. Leipzig, 1966. P. 317—332.

65. Komori Y. Some results on the super-intuitionistic predicate logics // Reports on mathematic logic. Warszawa; Cracow, 1983. №15. P. 13—33.

66. Letz R. First-order tableau methods // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 126—196.

67. Loveland D.W. Automated Theorem Proving: A Logical Basis. North Holland, 1978.

68. MasiniA. 2-sequent calculus: Intuitionism and natural deduction // Journal of Logic and Computation. Vol. 3 (5). 1993. P. 533—562.

69. McRobbie M., Belnap N.D. Proof-tableau formulations of some first-order relevant ortho-logics // Bulletin of the section of logic. Warszawa; Lodz, Vol. 13 (4). 1984. P. 233—240.

70. Meyer R.K., McRobbie M.A., Belnap N.D. Linear analytic tableaux I I Proceedings of Tableaux'95. 4 th Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Vol. LNAI 918. 1995. P. 278—293.

71. Miglioli P., Moscato U., Ornaghi M. An improved refutation system for intuitionistic predicate logic // Journal of Automated Reasoning, 13 (3). 1994. P. 361—373.

72. Miglioli P., Moscato U., Ornaghi M. Refutation systems for pro positional modal logics // Proceedings of the 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Vol. LNAI 918. 1995. P. 95—105.

73. Mints G. Gentzen-type systems and resolution rule. Part I: Propositional logic // Proceedings International Conference on Computer Logic, COLOG'88. Tallinn, USSR. Vol. 417 of Lecture Notes in Computer Science. Berlin, 1990. P. 198—231.

74. Mints G. Gentzen-type systems and resolution rule. Part П: Predicate logic // Proceedings ASL Summer Meeting, Logic Colloquium'90. Helsinki, Finland. Vol. 2 of Lecture Notes in Logic. Berlin, 1993. P. 163—190.

75. Mints G. Proof theory in the USSR, 1925—1970 // Journal of Symbolic Logic, 56 (2). 1991. C. 385-423.

76. Mundici D. A constructive proof of McNaughton's Theorem in infinite-valued logic // Journal of Symbolic Logic. Vol. 59 (2). 1994. P. 596—602.

77. Murray N.V., Rosenthal E. Resolution and path-dissolution in multiple-valued logics // Proceedings International Symposium on Methodologies for Intelligent Systems. Charlotte, 1991.

78. Ohnishi M, Matsumoto К. Gentzen method in modal calculi I // Osaka Mathematical Journal. Vol. 9. 1957. P. 113—130.

79. Ohnishi M, Matsumoto K. Gentzen method in modal calculi II // Osaka Mathematical Journal. Vol. 11. 1959. P. 115—120.

80. Ono H., Komori Y. Logics without the contraction rule // Journal of Symbolic Logic. Vol. 50. 1985. P. 16£—201.

81. Oppacher F., Suen E. HARP: A tableau-based theorem prover // Journal of Automated Reasoning, 4. 1988. P. 69—100.

82. Paech B. Gentzen-systems for propositional temporal logics // Proceedings of 2nd Workshop on Computer Science Logics, LNCS. 1988. P. 240—253.

83. Poplestone R.J. Beth-tree methods in automatic theorem-proving // Machine Intelligence /Ed. N.L.Collins, D.Michie. Vol. 1. New York, 1967. P. 31—46.

84. Pottinger G. Uniform, cut-free formulatins of T, S4 and S5 II Journal of Symbolic Logic. Vol. 48. 1983. P. 900—901.

85. Prior A. Past, present and future. Oxford, 1967.

86. Reeves S. Semantic tableaux as a framework for automated theorem-proving I I Advances in Artificial Intelligence (Proceedings of AISB-87). /Ed. C.S.Mellish, J.Hallam. Wiley, 1987. P. 125—139.

87. Reeves S.V. Adding equality to semantic tableaux // Journal of Automated Reasoning, 3. 1987. P. 225—246.

88. Rosser J.В., Turquette A.R Many-valued Logics. Amsterdam, 1952.

89. Rousseau G. Sequents in many valued logic I // Fundamenta Mathematica, LX. 1967. P. 23—33.

90. Rousseau G. Sequents in many valued logic ПУ/ Fundamenta Mathematics LXVII. 1970. P. 125—131.

91. Sambin G., Valentini S. A modal sequent calculus for a fragment of arithmetic // Studia Logica. Vol. 34. 1980. P. 245—256.

92. Schmitt S.f Kreitz C. Converting non-classical matrix proofs into sequent-style systems // Proceedings of 13th International Conference on Automated Deduction. Vol. 1104 of Lecture Notes in Artificial Intelligence. Berlin, 1996. P. 418—432.

93. Schroder J. Korner's criterion of relevance and analytic tableaux // Journal of Philosophical Logic. Vol. 21 (2). 1992. P. 183—192.

94. Shankar N. Proof search in the intuitionistic sequent calculus // Proceedings of 11th International Conference on Automated Deduction. Vol. 607 of Lecture Notes in Artificial Intelligence. Berlin, 1992. P. 522—536.

95. Smullyan R.M. Analytic natural deduction // Journal of Symbolic Logic, 30. 1965. P. 123—139.

96. Smyllyan R.M. First-order logic. New York, 1964.

97. Suchon W. La methode de Smullyan de construire le calcul n-valent des propositions de Lukasiewicz avec implication et negation // Reports on Mathematical Logic. Universities of Cracow and Katowice, 2. 1974. P. 37—42.

98. Sundholm G. Systems of deduction // Handbook of Philosophical Logic. Vol. I, chapter 1.2. /Ed. D.Gabbay, F.Guenther. Dordrecht, 1983. P. 133—188.

99. Surma S.I. An algorithm for axiomatizing every finite logic // Computer science and multiple-valued logic: theory and applications. Amsterdam, 1977. P. 143—149.

100. TakahashiM. Many-valued logics of extended Gentzen style П // Journal of Symbolic Logic. Vol. 35 (4). 1970. P. 493—528.

101. Thistlewaite P.В., Meyer R.K., McRobbie M.A. Advanced theorem-proving techniques for relevant logics // Logique et analyse. Vol. 28 (110/111). Louvain, 1985. P. 233—256.

102. Thomason R.H. On the strong semantical completness of the intuitionistic predicate calculus // Journal of Symbolic Logic. Vol. 33. 1968. P. 12—25.

103. Toledo S. Tableau Systems for First Order Number Theory and Certain Higher Order Theories // Lecture Notes in Mathematics. Vol. 447. Berlin, 1975.

104. Trzesicki K. Gentzen-style axiomatization of tense logic I I Bulletin of the section of logic. Warszawa; Lodz, 1984. Vol. 13 (2). P. 75—84.

105. Tuziak R. An axiomatization of the finite-valued Lukasiewicz calculus // Studia Logica. Vol. 47 (1). 1988. P. 49—55.

106. Urquhart A. Semantic for relevant logic // Journal of Symbolic Logic. Vol. 37. 1972. P. 11—17.

107. Urquhart A. The complexity of propositional proofs // The Bulletin of Symbolic Logic. Vol. 1. 1995. P. 425—467.

108. Urquhart A. The undecidability of entailment and relevant implication I I Journal of symbolic logic. Vol. 49 (4). 1984. P. 1059—1073.

109. Valentini S. The modal logic of provability: cut-elimination // Journal of Philosophical Logic. Vol. 12. 1983. P. 471—476.

110. Vellino A. The Complexity of Automated Reasoning. PhD thesis, University of Toronto, 1989.

111. Waaler A., Wallen L. Tableaux for intuitionistic logics // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 255—296.

112. Wallen L.A. Automated Deduction in Nonclassical Logics. 1990.

113. Warning H. Sequent calculi for normal modal propositional logics // Journal of Logic and Computation. Vol. 4. 1994.

114. Wolper P. The tableau method for temporal logic: an overview I I Logique et Analyse, 110—111. 1985. P. 119—136.

115. Woodruff P.W. A modal interpretation of three-valued logic I I Journal of Philosophical Logic. Vol. 3. 1974. P. 433—440.

116. Woolhouse R. Tensed modalities // Journal of Philosophical Logic. Vol. 2. 1973. P. 393—415.

117. Wrightson G. Non-classical theorem proving using links and unification in semantic tableaux // Tech. Rep. CSD-ANZARP-84-003. Wellington, 1984.

118. Zabel N. Nouvelles Techniques de Deduction Automatique en Logiques Polyvalentes Finies et Infinies du Premier Ordre. PhD thesis. Institut National Polytechnique de Grenoble. 1993.

119. Zach R. Proof theory of finite-valued logics. Master's thesis, Institut fur Algebra und Diskrete Mathematik. Wien, 1993.

120. Zeman I. Modal logic. Oxford, 1973.

121. Аншаков О.М.у Рынков С.В. О многозначных логических исчислениях // Семиотика и информатика. Вып. 19. М., 1982. С. 90—117.

122. Аншаков О.М., Рынков С.В. Об одном способе формализации и классификации многозначных логик // Семиотика и информатика. Вып. 23. М., 1984. С. 78—106.

123. Бочвар Д.А. К вопросу о непротиворечивости одного трехзначного исчисления // Математический сборник. Т. 12. № 3. 1943. С. 287—308.

124. Бочвар ДА., Финн В.К. О многозначных логиках, допускающих формализацию анализа антиномий // Исследования по математической лингвистике, математической логике и информационным языкам. М., 1972. С. 238—295.

125. Бродский И.Н. Индексация формул и поиск вывода // Вестник СПбГУ. Сер. 6. Вып. 4. СПб., 1992.

126. Быстрое П.И. Взаимное преобразование секвенциальных и натуральных выводов в модальной логике // Логические исследования. Вып. 6. М., 1999. С. 61—68.

127. Быстрое П.И. Нестандартный метод табличных конструкций для модальных и релевантных логик // Логические исследования. Вып. 1. М., 1993. С. 156—171.

128. Быстрое П.И. Погружение релевантной системы Е в табличное исчисление индексированных формул // Многозначные, релевантные и паранепротиворечивые логики. М., 1984. С. 20—26.

129. Войшвгишо Е.К. Философско-методологические аспекты релевантной логики. М., 1988.

130. Воробьев Н.Н. Конструктивное исчисление высказываний с сильным отрицанием // Доклады Академии Наук СССР. Т. 85. № 3 (1952). С. 465—468.

131. Воробьев Н.Н. Конструктивное исчисление высказываний с сильным отрицанием // Труды Математического института АН СССР. Т. LXXII (1964). С. 195—227.

132. ГейтингА. Интуиционизм. М., 1965.

133. Генцен Г. Исследования логических выводов // Математическая теория логического вывода. М., 1967. С. 9—49.

134. Катер С. Упрощенный метод доказательства для элементарной логики // Математическая теория логического вывода. М., 1967. С. 200—206.

135. Карпенко А.С. Многозначные логики // Логика и компьютер. Вып. 4. М., 1997.

136. Клини С.К Введение в метаматематику. М., 1957.

137. Клини С.К. Математическая логика. М., 1973.

138. Клини С.К. Перестановочность применений правил в генценовских исчислениях LK и ZJ // Математическая теория логического вывода. М., 1967. С. 208—236.

139. Крайзелъ Г. Основания интуиционистской логики // Математическая логика и ее применения. М., 1965. С. 229—244.

140. Крайзелъ Г. Исследования по теории доказательств. М., 1981.

141. Крипке С. Семантический анализ модальной логики. I. Нормальные модальные исчисления высказываний // Фейс Р. Модальная логика. М., 1974. С. 254—304.

142. Крипке С. Семантический анализ модальной логики. П. Ненормальные модальные исчисления высказываний // Фейс Р. Модальная логика. М., 1974. С. 304—324.

143. Максимова JI.JI. Предгабличные суперинтуиционистские логики // Алгебра и логика. 1972. № 11. С. 13—17.

144. Мардаев С.И. Две иерархии локально-табличных суперинтуиционистских логик. Новосибирск, 1987.

145. Марков А.А. Конструктивная логика // Успехи математических наук. Т. 5 № 3 (1950). С. 187—188.

146. Марков А.А. О конструктивной математике // Труды математического института им. В.А. Стеклова. Т. 67. 1962. С. Sr—14.

147. Маслов С.Ю. Возможности применения теории дедуктивных систем // Теория логического вывода. Ч. 1. М., 1974.

148. Маслов С.Ю. Обратимый вариант конструктивного исчисления предикатов // Записки научных семинаров ЛОМИ АН СССР. 1967. Т. 4. С. 96—110.

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

150. Маслов С.Ю., Минц Г.Е., Оревков В.П. Неразрешимость в конструктивном исчислении предикатов некоторых классов формул, содержащих только одноместные предикатные переменные // Доклады Академии наук. 1965. Т. 163 (2). С. 295—297.

151. Матулис В.А. Два варианта классического исчисления предикатов без структурных правил вывода // Доклады Ан СССР, 1962. Т. 147. №5. С. 1029-1031.

152. Минц Г.Е. Нормализация натуральных выводов и эффективность классического существования // Логический вывод. М., 1979. С. 246—266.

153. Минц Г.Е. Системы Льюиса и система Г(1965—1973) // Фейс Р. Модальная логика. М., 1974. С. 422—509.

154. Минц Г.Е. Теорема об устранимости сечения для релевантных логик // Записки ЛОМИ. Т. 32. 1972. С. 90—97.

155. Непейвода Н.Н. Префиксные семантические таблицы для модальных логик // Многозначные, релевантные и паранепротиворечивые. М., 1984. С. 60—68.

156. Новиков П.С. Конструктивная математическая логика с точки зрения классической. М., 1977.

157. Оревков В.П. Неразрешимость в конструктивном исчислении предикатов класса формул типа —,-i\/3 // Доклады Академии наук. 1965. Т. 163 (3). С. 581—583.

158. Плюшкевичус Р.А. Об одном варианте конструктивного исчисления предикатов без структурных правил вывода // Доклады АН СССР. 1965. Т. 161. №2.

159. Попов В.М. Логический анализ релевантных систем. М., 1979.

160. ПравицД. Натуральный вывод. М., 1997.

161. Серебрянников О.Ф. Эвристические принципы и логические исчисления. М., 1970.

162. Сидоренко Е.А. Релевантность и импликация // Модальные и интенсиональные логики и их применение к проблемам методологии науки. М., 1984. С. А—18.

163. Смирнов В. А. Поиск доказательств в натуральном интуиционистском исчислении предикатов // Логика, методология, философия науки. М., 1995. С. 176—180.

164. Смирнов В А. Представление логических систем с сильной релевантной импликацией в секвенциальной форме // Теория логического вывода. М., 1974. С. 149—159.

165. Смирнов В А. Формальный вывод и логические исчисления М., 1972.

166. Такеути Т. Теория доказательств. М., 1978.

167. Уусталу Т., Ленту с М. Секвенциальные системы модальных исчислений. М., 1989.

168. Шанин Н.А. О конструктивном понимании математических суждений // Труды математического института АН СССР. 1958. Т. 52. С.

169. Шанин Н.А. Об иерархии способов понимания суждений в конструктивной математике // Труды математического института им. В.А. Стеклова. Т. 129. 1973. С. 203—266.

170. Яблонский С.В. Функциональные построения в лг-значной логике // Труды математического института им. В.А. Стеклова. Т. 51. С. 5—142.