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

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

с:

2?

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

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

АНТОНОВА

Ольга Аркадьевна

Табличные исчисления в классической

неклассических логиках

09.00.07 - логика

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

и

Санкт-Петербург 1998

Работа выполнена на кафедре логики философского факультета Санкт-Петербургского государственного университета.

Научный руководитель Доктор философских наук, профессор СЛИНИН Я. А.

Официальные оппоненты: Доктор философских наук, профессор Караваев Э. Ф.

Кандидат философских наук, доцент Спивак В. И.

Ведущая орг анизация: Санкт-Петербургский государственный институт точной механики и оптики (Технический университет)

Защита состоится "/■Чг/ал 1998 г. в 'У^"часов на заседании диссертационного совета Д.063.57.01. по защите диссертаций на соискание ученой степени доктора философских наук в Санкт-Петербургском государственном университете по адресу: 199034 Санкт-Петербург, Менделеевская линия, д.5, философский факультет, ауд

С диссертацией можно ознакомиться в научной библиотеке им. А.М.Горького Санкт-Петербургского университета.

Автореферат разослан 1" •>' Ученый секретарь Диссертационного совета

-^1998 г.

Райкова Л.М.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы исследования.

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

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

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

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

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

Применению табличных методов в неклассических логиках посвятили свои работы:

в модальных логиках - С.Крипке, П.И.Быстров, В.Н.Костюк, Н.Н.Непейвода, М.Фиттинг, Э.Бет, С.Кангер, Р.Горе, Ф.Массачи.

в многозначных логиках - С.Сурма, В.Карниелли, Д.Бочвар, В.Финн, М.Бааз, Г.Фермюллер.

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

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

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

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

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

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

-произвести сравнительный анализ различных вариантов табличных исчислений;

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

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

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

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

Научная новизна диссертации состоит в следующем:

- воссоздана целостная история развития табличного метода;

- проанализированы и систематизированы различные варианты табличных исчислений;

- проанализировано доказательство Основной теоремы с помощью таблиц и указаны основные преимущества данного доказательства по сравнению с доказательством, предложенного Генценом;

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

На защиту выносятся следующие положения:

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

-табличный метод является наиболее простой и эффективной процедурой поиска доказательства;

-Абстрактная теорема, доказанная Смаллианом, представляет собой обобщенный вариант Основной теоремы Генцена.

Теоретическое и практическое значение диссертации заключается в следующем:

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

во-вторых, материалы диссертации можно использовать в преподавании курсов «История современной логики» и «Теория логического вывода».

Апробация работы: Диссертация обсуждалась на заседании кафедры логики философского факультета Санкт-Петербургского государственного университета. Основные положения диссертации отражены в публикациях автора.

Структура и объем работы определяются ее целями и задачами. Диссертация состоит из введения, двух глав, заключения и списка литературы. Содержание работы изложено на 128 страницах машинописного текста. Список литературы состоит из 131 наименований.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

В первой главе «Табличные исчисления» сначала рассматриваются историко-логические и философские предпосылки возникновения табличного метода, а затем описываются основные варианты таблиц - семантические таблицы Бета, аналитические таблицы, таблицы доказательства Земана.

В первом параграфе анализируются причины возникновения табличного метода. В начале XX века в основаниях математики возникла кризисная ситуация, связанная с обнаружением в теории множеств парадоксов. Попытка разрешить проблемы, возникшие в основаниях математики, привела Хинтикку к созданию модельного множества, описанного в работе «Form and Content in Qauntification Theory», опубликованной в 1955 г. По словам Хинтикки, возникновение идеи о модельных множествах, связано с переосмыслением теории истинностных функций. Эта теория хорошо работает в логике высказываний, но в случае логики предикатов с бесконечными областями возникают проблемы. В общем виде подход Хинтикки состоит в продвижение от формулы к распределениям истинностных значений, т.е. начиная от данной формулы или данного множества формул, мы получаем распределение истинностных значений, которые удовлетворяют ей, посредством некоторого конструктивного процесса, проводимого шаг за шагом, согласно определенным простым правилам. Неудача такого построения будет служить критерием логической ложности. Этот подход можно применить и к бесконечным множествам формул. Надо заметить, что идея модельного множества схожа с идеей семантических таблиц, предложенных Бетом в 1955 г. Хинтикка, так же как и Бет, рассматривает доказательство общезначимости некоторой формулы

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

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

Основные достоинства метода семантических таблиц заключаются в следующем:

a) он похож на тот «естественный» способ рассуждения, которым мы обычно пользуемся, если не пытаемся действовать в некоторой заранее выбранной логической системе;

b)он полностью согласуется с семантической интерпретацией формул;

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

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

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

В 1973 г. на основе секвенциальных исчислений Дж. Земан строит таблицы-доказательства, описанные в работе «Модальная логика». Таблицы-доказательства являются вариантом семантических таблиц Бета. Если секвенция является базовой единицей генценовских исчислений, то базовой единицей подхода Бета является таблица. Между ними существует определенное

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

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

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

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

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

(A) Если некоторая а встречается па пути Ру, тогда можно присоединить либо (Х|, либо «2 как единственного наследника У.

(B) Если некоторая (3 встречается на пути Ру. тогда можно одновременно добавить £¡1 как левого иаспедника У и р? как правого наследника У.

Т является аналитической таблицей для х, если и только если существует конечная последовательность Ть Тг, ... Т = Т, так что Т[ - дерево первой степени, в котором начало х и такое, что для каждого 1 < п, Т,+| есть прямое продолжение Ъ. Доказательством х называется замкнутая таблица для ~х. Аналитические таблицы для пропозициональной логики всегда конечны. Что касается первопорядковой логики, то бывают случаи, когда аналитическая таблица может продолжаться бесконечно. Задача состоит в нахождении систематической процедуры, чтобы в любой бесконечно продолжаемой таблице каждый ее открытый столбец образовал множество Хинтикки. Такую систематическую процедуру предложил Смаштиан. Она состоит в построении систематической таблицы. Систематическая таблица строится следующим образом. Начинаем таблицу расположением формулы вначале. Если таблица уже вначале закрыта, тогда процесс останавливается. Также если все неэлементарные точки на каждой открытой ветви таблицы использованы. Если т.Х появляется на минимальном уровне, не была использована и появляется на

одной открытой ветви, то располагаем таблицу следующим образом: берем каждый открытый столбец (ветвь), содержащий X и

1) если X есть а, то расширяем © до (0, а.1 ,аг);

2) если X есть р, то разделяем © на два подстодбца (©, Р|) и (0, );

3) если X есть 8, то берем первый параметр а, который не появляется на дереве и расширяем 0 до (0,6(а)).

4) если X есть у, тогда берем первый параметр а, такой что у(а) не входит в 0 и расширяем © до (©, у(а), у). Имея законченными пункты 1-4, будем считать, что т.х использована и это завершает (п + 1) - й шаг процедуры.

Очевидно, что в любой завершенной систематической таблице каждый открытый столбец есть множество Хинтгоски.

В этом же параграфе также описываются таблицы, предложенные Фиттингом в 1969 г. Аналитическая таблица формулы А есть пепустая последовательность множеств {Г) ,..., Гп}, называемых конфигурациями, где Г] , ..., Г„ (п > 1) являются множествами отмеченных формул. Выражения вида «ТС» и «РС», где С - формула, будем называть отмеченными формулами. Исходной конфигурацией при построении аналитической таблицы для формулы А является {{РА}}, а каждое следующее множество получается из предыдущего по какому-нибудь из правил. Каждое правило применяется непосредственно к множеству {Г, М}, где Г - перечень отмеченных формул, возможно пустой, а М - выделенная в данном множестве отмеченная формула. Применение правил состоит в преобразовании М. Отсюда, в результате, получается два или одно множество под чертой и, таким образом, новая конфигурация. Преобразование М состоит в исключении из нее логической константы, представляющей собой главную операцию. Множество отличенных формул, в составе некоторой конфигурации, называется замкнутым, если среди его элементов встречаются ТС и РС. Множество называется исчерпанным, если оно или замкнуто, или ни к одной из отмеченных формул не применимо ни одно из правил. Аналитическая таблица замкнута, если каждое множество формул ее последней конфигурации является замкнутым. Формула тождественно-истинна, если ее аналитическая таблица замкнута. В противном случае незамкнутые множества указывают на условия ложности данной формулы.

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

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

Правило А указывает на то, что к любой конечной точке {в, а} можно добавить {Э, а(} как единственного наследника или можно добавить {Б, «2} также как единственного наследника.

Правило В обозначает то, что к любой конечной точке {Б, Р} можно прибавить одновременно {в, (?]} как левого наследника и {Б.рг} как правого. Превратить закрытую аналитическую таблицу в закрытую блок-таблицу для набора 8 нетрудная задача. Необходимо заменить каждую точку таблицы набором, содержащим саму эту точку вместе со всеми точками, которые находились выше на ветке. Получившееся дерево и есть закрытая блок-таблица. Надо заметить, что блок-таблицы совпадают с исчислением 03, но процесс построения вывода идет в противоположном направлении.

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

Если существует доказательство (чисто логическое) некоторого утверждения, то для этого утверждения существует и прямое доказательство без

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

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

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

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

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

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

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

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

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

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

конфигураций ei ,ег ..., где е начинается с ~А и c,+i получается из е, одним применением правила я.

Второй способ заключается в построение дерева, при помощи правил редукции. Для этого к аналитической формулировке пропозициональной логики присоединяем знаки □ ,С, Н, правило построения «если А - формула, то □ А, СА, НА - формулы», (О А - «А необходимо», СА - «А случайно», НА - «А невозможно»), а также правила редукции.

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

Табличная - конструкция является системой таблиц, построение которой начинается введением в левый (правый) столбец начальной таблицы формул Ai , Аг ,..., Am (m £ 0), Bi , В2 ,... , В„ (n £ 0), причем каждой вписываемой в начальную таблицу формуле приписывается индекс о. Построение конструкции осуществляется по соответствующим правилам.

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

Пропозициональной таблицей для формулы a,(F(X|,....,Xm)') является дерево, у которого первый узел формула a,(F(Xi,....,Xm)), остальные узлы определяются следующей процедурой:

РО после установления первого узла, следующие узлы получаются

применением Пц к а,(Р(Хь.....,Хт)) (формулы разделенные «•» находятся в той

же самой ветви, наборы формул, отделенные «+» находятся в разных ветвях).

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

Р-таблица для аЦХ) закрыта, если для каждой ветви, либо существуют узлы с а;(У) и а,(У) для щ, или ветвь содержит некоторую неатомическую формулу а,(У) и не существует определенного правила П^, где Р - главная связка У. Иначе таблица открыта.

Далее представляются аналитические таблицы для систем Вз и Ь'з, построенные Бочваром и Финном в 1976 г. Аналитической таблицей для формулы X является конечнопорождснное триадическое дерево 1", удовлетворяющее следующим условиям. Пусть Г) и Гз - два упорядоченных' триадических дерева, их точками являются вхождения формул. является прямым расширением Г;, если Г2 получено из Г| применением правил одного из типов А, В, С. Тогда Г - таблица для X, если существует конечная последовательность Гь Гг., Г„, где Г„ = Г такая, что Г] есть одноточечное дерево, чей корень есть X, и для каждого 1 < п 1",ц есть прямое расширение Г,.

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

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

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

констант и понятие вывода. В данном параграфе рассматриваются табличная система Ет, соответствующая релевантной системе Е и табличное исчисление индексированных формул Е]. Построение Е; - конструкции для формулы К начинается помещением Р в начальную таблицу справа, если знак -» не является в Р главным логическим знаком, или вписыванием в начальную таблицу А слева, а формулы В справа, если И имеет вид Л -» В. Построение продолжается по правилам, указанным в работе Быстрова.

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

В классической системе ТХ означает X и РХ означает ~Х. Доказательством является процедура опровержения. Предположим X не истинна (начнем таблицу с РХ), Выводим, что некоторая формула должна быть истинна и не истинна. Т.к. это не может случиться, X - истинна. В интуиционистском варианте ТХ означает, что известно, и X истинна (X доказуемо), РХ означает, что не известно X истинно ли. Доказательством аналогично является процедура опровержения. Предположим, X не доказуема. Выводим, что, возможно, что некоторая формула и доказуема, и не доказуема. Отсюда, невозможно, что X - доказуема.

Таблицей (аналитической) является конечная последовательность конфигурация ф|, фг,..., ф„, в которой каждая конфигурация, исключая первую, результат применения одного из правил к предшествующей конфигурации. Набор Б закрыт, если он содержит оба ТХ и РХ для некоторой формулы X.

Конфигурация {Б] , в: ..., 8„} закрыта, если каждая Б, закрыта. Таблица Ф1, ф2 , ..., фп закрыта, если некоторое ф, закрыта. Под таблицей для набора 8 обозначенных формул будем понимать таблицу фь фг , ..., ф„ , в которой ф| -

Если некоторая таблица для Б закрыта, то конечный набор обозначенных формул Б является противоречивым. Если {РХ} противоречиво, то X - теорема и закрытая таблица для {РХ} доказательство X.

Соответствующая классическая табличная система похожа на эту, но в правилах Р ~ и Рэ, Э т- заменяется на Б.

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

РВ, только если существует В| ....., В„ такие, что { В| ......В„}сГиВ| &.....

& В„ -» А £ Ь.

В пятом параграфе рассматривается применение табличных исчислений в области науки и искусственного интеллекта. Еще в 1958 г. Э.Бет в своей работе «Машины для доказательства теорем» указал на возможность представления семантических таблиц как теоретической базы для логической теории машин. В 60-е гг. исследования, начатые Э.Бетом, продолжили Р.Попплестон, И.Кохен, Л.Триллинг, П.Венер и др. В 70-80- е гг. направление исследования табличного метода в области искусственного интеллекта развивается в сторону логического программирования на основе таблиц. Здесь надо отметить работы К.Брода, В.Шонфелда, Л.Валлена, Д.Вритсона, С.Ривса.

В 1985 г. В.Шонфелд предложил табличную логику программирования со строгим отрицанием, но его исследование было неполным. С.Акама дал полное описание таблиц для логики программирования со строгим отрицанием. Табличное исчисление для логики программирования со строгим отрицанием (ТаРБ) имеет язык аРЯ, обогащенный (-») импликацией, V и Э. Надо отметить, что язык аР8 содержит только: &, V, 1 (истина).

Добавим к аРЯ следующее правило:

Ветвь таблицы закрыта, если она содержит обозначенную формулу F(l(t¡, ..., t„)), так что существует обозначенная формула клаузы Т (1(хь ..., х„)) S (ь ..., х„) и существует закрытая таблица для обозначенной формулы F(S(ti,..., tn)). Отметим, что клауза имеет форму k-S. Назовем таблицу, к которой прибавлено данное правило - а Р - таблицей.

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

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

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

корневой узел содержит Т(0) и возможно некоторую другую префиксно-обозначенную формулу;

узлы содержат наборы обозначенных формул Т(А), F(B), Т(А ф В), F(A В), или набор префиксно-обозначенных формул р (Т(А), F(B)). Таблица строится рекурсивно при помощи определенных правил. Таблица закрыта, если все пути в ней закрыты. Закрытая таблица с корнем-узлом {T(0i), ..., Т(0„), F (0О)} является доказательством 0о от 0i, ..., 0„ . Если существует доказательство 0О при 0¡, ..., 0„, тогда 0i,..., 0„ доказывает 0о , которое обозначается {0ь ..., 0„} |- 0о . Здесь каждое 0¡ для О í i í п, либо функциональная независимость, либо функциональная зависимость. Закрытые пути в таблицах можно интерпретировать как семантическую невозможность.

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

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

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

автора:

1. Метод семантических таблиц Э.В .Бета // Человек - Философия -Гуманизм: Тезисы докладов и выступлений Первого Российского философского конгресса (4-7 июня 1997 г.) т.З, Санкт- Петербург, 1997 г. с. 152.

2. Кризис рациональности современной цивилизации //Философия и цивилизация. Материалы Всероссийской конференции 30-31 октября 1997 г. Санкт-Петербург, 1997 г., с.135-136.

Отпечатано Í ООО „ Рщо - Принт " Тир- -/00