А.Е.Болотов, В.А.Бочаров,
А.Е.Горчаков

Алгорифм поиска вывода
в классической пропозициональной логике^*

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

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

В 1992 году авторы поставили перед собой задачу осуществить поиск алгорифма вывода и доказательства (как линейной последовательности утверждений) для классической логики высказываний. Работа осуществлялась сотрудниками философского факультета Московского государственного университета им. М.В.Ломоносова и была завершена в 1994 году. Своеобразие предлагаемого ниже алгорифма, реализованного на языке "Си" для IBM PC, состоит в том, что авторам удалось формализовать эвристики, которые, как нам представляется, применяются обычно в естественном рассуждении. Это позволило авторам найти эффективную процедуру для осуществления так называемого субординатного вывода.

В основу дедуктивного аппарата было положено натуральное исчисление высказываний Квайна, которое было модифицировано сотрудниками кафедры логики философского факультета МГУ - профессорами Е.К.Войшвилло и В.А.Бочаровым. Выбор именно этого исчисления был обусловлен теми соображениями, что данная система обладает целым рядом дидактических преимуществ - наличие только прямых правил вывода, позволяющих переходить от формул к формулам, простая формулировка понятия вывода, - в силу чего она в течение долгого времени преподавалась и до сих пор преподается на факультете студентам-философам. Система содержит обычный алфавит, обычное понятие формулы и следующие дедуктивные принципы:

Правила вывода:

&вв: &_И и: ,

вв: , ии:

É вв: - где С - гипотеза É ии:

Ø вв: - где С - гипотеза Ø и:и:

Выводом в системе называется непустая конечная последовательность формул С1, С2,..., Сk, удовлетворяющая условиям:

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

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

Вывод С1, С2,..., Сk есть вывод вида А1, А2,..., Аn | ¾ В, если А1, А2,..., Аn - это неисключенные гипотезы, а формула В графически совпадает с Сk.

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

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

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

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

(I) По формулам вывода осуществляются следующие процедуры:

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

Процедура 2 - формирует новые цели; эта процедура выполняется в том случае, когда все возможные, указанные в процедуре 1, правила вывода применены, последней целью в последовательности целей является "F" (противоречие) и при этом данная цель не достигнута (см. процедуру 3). Какие именно вводятся цели, определяется видом содержащихся в выводе формул, и будет объяснено далее.

Процедура 3 - осуществляет проверку достижимости последней цели в списке целей. Если последней целью является некоторая формула, то она считается достигнутой просто по факту наличия в выводе графически равной ей формулы. Если же последней целью является F (противоречие), то она считается достигнутой, если в выводе содержатся формулы вида A и Ø A. Достигнутая цель из списка целей устраняются, а очередной целью становится предыдущая цель в списке целей.

(II) По последовательности целей осуществляются процедуры:

Процедура 4 - формирует подцели, которые помещаются в последовательность целей.

Процедура 5 - выбирает новые дополнительные посылки, помещаемые под очередным номером в последовательность формул вывода.

Процедуры 4 и 5 опишем вместе, так как они в определенных случаях применяются одновременно. Данные процедуры начинают использоваться, когда уже применена процедура 1, целью является некоторая формула, и при этом она не достигнута. В этом случае последовательность целей дополняется новой подцелью или совокупность посылок в выводе дополняется новой посылкой. Что конкретно происходит зависит от вида очередной (последней) цели и будет объяснено в формулировке алгорифма.

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

Изначально эти две последовательности формируются следующим образом:

Если необходимо осуществить вывод некоторой формулы В из множества посылок А1,...,Аk,, то формулы W1,...,Wk, составляют исходный список формул вывода, а формула W помещается в список целей. При этом формула W считается главной целью и если эта цель достигается, то вывод считается законченным.

если необходимо осуществить вывод W из пустого множества посы-

лок, то есть требуется осуществить доказательство W, то список вы-

вода является пустым, а формула W помещается в список целей. Ес-

тественно, эта формула и является главной целью.

1. 1.Определяется главная цель вывода. Таковой является формула, стоящая справа от знака выводимости. Данная формула помещается в качестве начальной в последовательность целей. Если слева от знака выводимости стоят формулы, то они помещаются в качестве начальных в последовательность формул вывода. Переход к 2.

2. Проверяется наличие отношения логического следования между посылками

W1,...,Wk и формулой W, а в случае доказательства W - наличие свойст-

ва общезначимости у исходной формулы W. В случае положительного отве-

та на первый или второй вопросы переходим к выделению главной цели -

2, в случае отрицательного ответа - выдается соответствующее сообще-

ние. Выход.

2. Определяется главная цель - это формула, стоящая справа от знака выводи-

Анализ множества формул вывода.

2.1. мости.

3. Если множество формул вывода пусто, то переход к 4.

2.2. Если множество формул вывода непусто, непусто, то переход к 3.

3. Умозаключения по формулам вывода.

3.1. Осуществляются все непосредственные умозаключения по аналитическим правилам; при этом на посылки правил вывода вида А & В, А Ú В, А É В, Ø Ø А, к которым были применены, соответственно, правила &и, и, É и и Ø и, ставиться метка “V0”, указывающая на недопустимость вторичного применения к ним указанных правил, а на заключения правил вывода ставиться метка “V+1” (смысл этой метки разъясняется далее). Переход к 9.

3.2. Если ни одно аналитическое правило не применимо, то - 9.

4. Анализируется главный знак очередной цели - W.

4.1. W - пропозициональная переменная. Переход к 5.

4.2. Главный знак W - Ø . Переход к 5.

4.3. W = Wi É Wj. Переход к 6.

4.4. W = Wi & Wj. Переход к 7.

4.5. W = Wi Ú Wj. Переход к 8.

4.6. Цель W - противоречие. Переход к 11.

5. Ø W включается в последовательность формул вывода в качестве посылки, подцелью становится получение противоречия, тип устраняемости - Ø . Переход к 3.

6. Формула Wi включается в последовательность формул вывода в качестве посылки, подцелью становится Wj, а тип устраняемости - É . Переход к 3.

7. Wi становится подцелью.

7.1. Подцель - Wi.

Если Wi достижима, то переход к 7.2.

В противном случае - 4.

7.2. Подцелью становиться Wj.

Если Wj достижима, то - 9.

В противном случае - 4.

8. Wi становится подцелью.

8.1. Цель - Wi, метка цели - "V1".

Если цель Wi достижима, то 9.

В противном случае - 8.2.

8.2. Цель - Wj, метка цели - "V2".

Из последовательности целей устраняются все подцели, начинаюшиеся с метки “V1”, а из последовательности формул вывода все формулы, начиная с посылки, соответствующей этой отмеченной цели.

Если цель Wj достижима, то - 9.

В противном случае - 8.3.

8.3. Из последовательности целей устраняются все подцели, начинаюшиеся с метки “V2”, а из последовательности формул вывода все формулы, начиная с посылки, соответствующей этой отмеченной цели.

Если на цели Wi Ú Wj не стоит метка “V-1” (об ее смысле будет сказано ниже), то формула Ø (Wi Ú Wj) берется в качестве новой посылки, тип устраняемости - Ø , а в качестве подцели берется противоречие. Переход к 3.

В противном случае осуществляется временный выход из доказательства исходного метаутверждения, цель Wi Ú Wj устраняется, а в качестве новой цели берется формула Ø Wi & Ø Wj и осуществляется вывод Ø (Wi Ú Wj) | ¾ Ø Wi & Ø Wj. Переход к 3.

9. Достигнута цель Wn.

9.1. Если Wn - главная цель, то Wn помечается как достигнутая, выход - выводимость обоснована.

9.2. Если Wn - противоречие, то Wn как цель устраняется, новой целью становиться предыдущая цель, а к формулам вывода применяется правило Ø в. Результатом является формула Ø B, где B - последняя посылка в выводе, и делается отметка, что все формулы, начиная с B и заканчивая формулой, предшествующей Ø B, в дальнейших шагах вывода принимать участия не могут. Если в число этих формул попадает формула с меткой “V+1”, являющаяся заключением некоторого правила вывод, то с соответствующей формулы, являющейся посылкой данного применения правила вывода, снимается метка “V0”. Переход к 3.

9.3. Если предыдущей к достигнутой цели Wn является цель Wn-1 = Wn Ú Wk или Wk Ú Wn, то из последовательности целей устраняются цели Wn и Wn-1, новой целью становится предыдущая цель, а в последовательность формул вывода включается формула Wn-1, которая является результатом применения правила Ú в к формуле Wn. Если на цели Wn-1 стояла метка “V-1”, то с формулы вывода, породившей данную цель (об этом будет сказано ниже) снимается метка “V-1”. Переход к 3.

9.4. Если предыдущей к достигнутой цели Wn является цель Wn-1 = Wk É Wn, то к формуле вывода Wn применяется правило É в. Цели Wn и Wn-1 помечаются как достигнутые. Очередной целью становится ближайшая ранее не достигнутая цель, и в последовательности формул вывода делается отметка, что все формулы, начиная с Wk и заканчивая формулой Wn, в дальнейших шагах вывода принимать участия не могут. Если в число последних формул попадает формула с меткой “V+1”, являющаяся заключением некоторого правила вывода, то с соответствующей формулы, являющейся посылкой данного применения правила вывода, снимается метка “V0”. Если на цели Wn-1 стояла метка “V-1”, то с формулы вывода, породившей данную цель cнимается метка “V-1”. Переход к 3.

9.5. Если предыдущей к достигнутой цели Wn является цель Wn-1 = Wk & Wn, то к формулам вывода Wk и Wn применяется правило &в. Цели Wn и Wn-1 помечаются как достигнутые. Очередной целью становится ближайшая ранее не достигнутая цель, и в последовательности формул вывода на формулу Wk & Wn ставится метка “V0”. Если на цели Wn-1 стояла метка “V-1”, то с формулы вывода, породившей данную цель cнимается метка “V-1”. Переход к 3.

9.6. Если последней целью Wn является формула и она не достигнута, то 4.

10. Выбор новых целей по формулам вывода.

Просматриваются сверху вниз все формулы последовательности формул вывода.

Если в последовательности имеются сложные формулы, не отмеченные метками “V0” или “V-1”, то к ним применяются следующие процедуры:

10.1. Если в выводе имеется импликативная формула вида Wi É Wj, то в качестве подцели берется Wi. Формулы Wi É Wj и Wi помечаются метками “V-1”. Переход к 4.

10.2. Если в выводе имеется дизъюнктивная формула вида Wi Ú Wj, то в качестве подцели берется Ø Wi. Формулы Wi Ú Wj и Ø Wi помечаются метками “V-1”. Переход к 5.

10.3. Если в выводе встречается формула Ø Wi, то в качестве цели берется Wi. Формулы Ø Wi и Wi помечаются метками “V-1”. Переход к 7.

В противном случае - завершение программы (утверждение нельзя обосновать).

11. Алгоритм поиска противоречий.

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

Если в последовательности формул вывода противоречие не найдено, то переход к 10.

Несколько слов о программе, реализующей описанный алгоритм. Программа написана на языке высокого уровня "Си" для компьютеров типа IBM PC AT. Программа занимает на диске 140 кбайт, время работы над доказательством тестированных теорем не превышает 4 сек. для персонального компьютера на базе процессора INTEL-386-DX с тактовой частотой 40 МГЦ. Программа имеет пользовательский интерфейс и может читать заранее заготовленные формулы из файла. Тестирование проводилось на множестве формул, выбранных из учебников по математической логике, в частности, из книги А.Черча "Введение в математическую логику". Это множество - около ста теорем классической логики - достаточно репрезентативно, что позволяет рассматривать предложенный алгоритм поиска вывода для натурального исчисления высказываний как эффективную процедуру осуществления субординатных выводов.

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

Требуется доказать: ((pÉ q) É p) É p

Объясним шаги вывода, строившегося по описанному выше алгоритму. Так как требуется доказать формулу ((p É q) É p) É p, то исходный список вывода пуст, а главной целью является сама эта формула. По этой формуле, согласно пункту 4, начинает формироваться последовательность формул вывода и в качестве первой посылки берется формула (p É q) É p), а целью становится формула р. Так как эта цель не достижима, то опять по пункту 4 в вывод помещается посылка Ø p, а целью становится F. Цель F не достижима, а поэтому по процедуре 9 первая посылка служит источником новой цели, которой становится формула p É q . Вновь по 4 в качестве новой посылки берется формула р, а в качестве новой цели - формула q. Опять-таки, последняя цель не достижима, а поэтому по 4 берется новая посылка Ø q, а новой целью становится F. На этом шаге автоматического поиска вывода машина устанавливает, что цель F достигнута, так как в выводе имеется противоречие - формулы p и Ø p (шаги вывода 1 и 2). Это служит сигналом для применения в выводе правила "введения отрицания". Именно таким образом в выводе появляется 4-й шаг - формула Ø Ø q. При этом все формулы, начиная с последней посылки (формулы 3) и вплоть до результата применения этого правила считаются из вывода устраненными (что помечено слева от номеров шагов вертикальной линией, длина которой равна числу строчек исключаемых формул). Заметим, что хотя в выводе уже ранее содержалось противоречие, это правило не применялось, так как на это не указывала никакая из целей. Цель F, так как она достигнута, исключается и целью становится предыдущая цель - формула q. Формула q легко достигается, так как к 4 шагу можно применить правило "исключения отрицания". Достижение формулы q служит сигналом для автоматического применения правила “É в", что дает формулу 6 вывода.

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