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

• Автор: Антонова, Ольга Аркадьевна
• Шифр специальности: 09.00.07
• Научная степень: Докторская
• Год защиты: 2005
• Место защиты: Санкт-Петербург
• Количество страниц: 346 с. : ил.

Введение

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

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

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

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

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

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

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

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

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

.2.2. Таблицы Фиттинга
Глава Ш. Табличные методы в неклассических логиках
1.1. Методы логического вывода и таблицы в интуиционистской логике
Ш.1.1. Теоретический анализ методов логического вывода в интуиционистской логике аксиоматический, натуральный и секвенциальный вывод
Ш. 1.1.1. Аксиоматические системы интуиционистской логики
Ш.1.1.2. Натуральный вывод в интуиционистской
логике.
Ш. 1.1.3. Секвенциальные системы интуиционистской
логики.
1.1.2. Табличные методы в интуиционистской логике. Семантические таблицы Бета для систем
интуиционистской логики
III. 1.3. Аналитические таблицы для систем
интуиционистской логики
III. 1.4. Усовершенствованная табличная система Мильоли
МоскатоОрнаги.
III. 1.5. Расширение табличного метода для интуиционистских логик на модальные системы. Системы АвеллонеФеррари.
Ш.2.Табличные методы в модальной логике
Ш.2.1. Теоретический анализ методов логического вывода в системах модальной логики аксиоматический, натуральный и секвенциальный вывод
Ш.2.1.1. Аксиоматические варианты систем модальной
логики.
Ш.2.1.2. Натуральный вывод в модальной
логике.
Ш.2.1.3. Секвенциальные системы модальной
логики.
1П.2.2. Семантический анализ модальной логики методом таблиц. Семантические таблицы Крипке и модельные множества Хинтикки.
Ш.2.3. Табличные методы Фитгинга для модальной
логики.
ШЛ Применение табличных методов в многозначной логике
1.3.1. Теоретический анализ методов логического
вывода в многозначной логике аксиоматический, секвенциальный
Ш.3.1.1. Системы гильбсртовского типа в многозначной
логике.
Ш.3.1.2. Секвенциальные системы многозначной
логики.
Ш.3.2. Табличные методы в многозначной логике.
Аналитические таблицы для систем многозначной логики
1.3.3. Табличный метод Карниелли. Систематизация конечнозначных логик через метод таблиц.
1.3.4. Оптимизация табличного метода Карниелли.
Таблицы для множествзнаков Хэнла.
Ш.3.5. Расширение табличного метода для конечнозначных логик на системы интуиционистской
логики. Система БасаФермюллера.
Ш.4. Методы логического вывода и таблицы в релевантной логике.
Ш.4.1. Теоретический анализ методов логического
вывода в релевантной логике аксиоматический, натуральный и секвенциальный вывод
Ш.4.1.1 Аксиоматические системы релевантной логики
Ш.4.1.2. Системы натурального вывода в релевантной
Ш.4.1.3. Генценовские логистические исчисления для
релевантных систем
Ш.4.1. Таблицы для систем релевантной логики
Ш.4.1.1. Таблицы для систем ЯМ
Ш.4.1.2. Таблицы для релевантных систем с
мультипликативными связками.
Ш.4.1.3. Таблицы с индексированными формулами для
релевантных систем
Заключение
Литература


Табличные системы, основными свойствами которых являются анализ и опровержение, имеют подходящую форму для построения алгоритмов доказательства теорем. Современный этап развития табличного метода, подразумевает под собой автоматизацию табличного метода, или возможность его применения в автоматическом поиске вывода. Еще у Бета была идея автоматического доказательства теорем при помощи таблиц, но к сожалению, она не привела к дальнейшим результатам. Однако если Робинсон, открыв метод резолюций, сразу заинтересовался его автоматическим применением, то Смаллиан и Лис совершенно не обратили внимание на автоматическую эффективность открытого ими метода аналитических таблиц. В настоящее время исследования в области автоматического доказательства теорем методом таблиц являются приоритетными. Мы не будем рассматривать эту историю развития таблиц. Вопервых, потому что это выходит за рамки нашего исследования, посвященного, вообще говоря, логической истории развития табличного метода, а вовторых, исследования в области автоматического доказательства методом таблиц слишком многочисленны и все время продолжаются, быстро набирая темп. Важно только отметить, что таблицы будут продолжать играть центральную роль в области автоматического доказательства, потому что они легко модифицируются и могут использоваться для создания других методов в области автоматического доказательства теорем. Табличный метод связан с методом резолюций, как показал Г. Е. Минц, существует также связь с методом, исследованным Г. Райтсаноном, Э. Эдером, с матричным методом, рассмотренным I. Уолленом. Развитие методов автоматического доказательства теорем, не основанных на табличном методе, но выводимых из него, предмет исследования, который на сегодня является приоритетным. Ii v i iii Ii ii. Развивать табличный метод для новых логик, например логик смешанного типа, проще, чем создавать для них новые, более эффективные, процедуры доказательства. Причиной этого является тот факт, что именно табличный метод, как никакой другой, проясняет семантические связи, лежащие в основании той или иной логической системы. I. 2. В с годы Д. Гильбсрт разработал аксиоматический метод доказательства, идея которого заключается в том, что истинные формулы выводятся из некоторого множества основных формул, являющихся логическими аксиомами, посредством применения нескольких правил вывода. Выводом формулы А из множества формул Г называется такая последовательность формул А, . Ап что Ап есть А и для любого А есть либо аксиома, либо элемент Г, либо непосредственное следствие некоторых предыдущих формул по одному из правил вывода. Члены Г называются гипотезами, или посылками, вывода. Необходимо отметить, что если А выводимо из множества посылок Г, то оно также будет выводимо, если к Г добавить новые посылки. Существует большое количество разнообразных исчислений гильбертовского типа с разными наборами аксиом. Что касается правил вывода, то здесь разнообразие значительно меньше. Практически все исчисления этого типа содержат либо одно правило называемое в традиционной логике , или правило удаления импликации, либо два правило удаления импликации и правило подстановки. Правило подстановки означает, что формула, полученная из некоторой теоремы заменой всех переменных произвольными формулами, также будет теоремой. Очевидно, что правило подстановки необходимо в тех системах, где аксиомы рассматриваются как конкретные формулы. Исчисления, которые имеют в качестве аксиом схемы аксиом, не нуждаются в правиле подстановки. Среди большого разнообразия исчислений гильбертовского типа мы остановимся только на тех, которые либо действительно используются нами в тексте, либо представляют особый интерес, либо имеют историческое значение. Начнем наше рассмотрение с наиболее сложной и неэкономичной формулировки, принадлежащей Д. Гильберту. Однако следует отмстить, что данное исчисление, назовем его Рц следуя А. Черчу, предназначено, скорее, для выделения ролей различных связок, хотя и за счет неэкономности и потери независимости исходных связок. Гильберт Д. БернайсП. Основания математики. Теория доказательств. М., .