Научное изыскательское исследование

Введение

Актуальность темы исследования. Проблема поиска логического вывода традиционно считается одной из центральной тем логики. Бурное развитие данной проблематики в XX веке стимулировали, с одной стороны, фундаментальные работы Г. Генцена и Ж. Эрбрана и, с другой, появление ЭВМ. Возможность использования ЭВМ в процессе поиска логического вывода привела к появлению проблематики автоматического (машинного) поиска логического вывода.

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

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

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

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

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

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

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

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

Исчисления последнего вида особенно интенсивно исследуются на предмет автоматического поиска в них вывода в конце 80-х - начале 90-х гг. ХХ века.

Так, Дж. Поллок [Pollock] предложил программу поиска натурального вывода OSCAR в классической логике предикатов (а также в некоторых неклассических логиках) с использованием сколемовских термов. Он показал, что OSCAR работает в 40 раз эффективнее программы OTTER [Pollock], основанной на методе резолюций. С другой стороны, круг логических проблем, которые решает OSCAR, шире, чем аналогичный круг для OTTER. Дж. Поллоком была выдвинута также гипотеза, что OSCAR обладает свойством семантической полноты, т.е. что OSCAR может найти вывод любой общезначимой формулы классической логики предикатов.

Д. Пеллетье [Pelletier] предложил программу поиска натурального вывода Thinker в классической логике предикатов (а также в некоторых неклассических логиках) с предикатом равенства. Показывается, что Thinker решает 75 тестовых проблем для произвольного алгоритма поиска вывода в классической логике предикатов с предикатом равенства. Thinker не обладает свойством семантической полноты, поскольку количество переменных, которые используются в выводе, заранее ограничено.

У. Сиг вместе с Дж. Бернсом [Sieg], [Sieg & Byrnes] предложили программу автоматического поиска натурального вывода CMU PT в классической логике (авторы также рассматривают возможность обобщения программы на неклассические логики). Специфика данного алгоритма состоит в том, что натуральный вывод строится не прямым, а косвенным образом. Сначала строится вывод в т.н. промежуточном исчислении, а затем показывается, каким образом можно преобразовать вывод в промежуточном исчислении в натуральный вывод. Авторы показывают, что CMU PT обладает свойством семантической полноты.

Д. Ли [Li] предложил программу поиска натурального вывода ANDP в классической логике. Особенно подчеркивая прикладное значение ANDP, Д. Ли дает машинные доказательства некоторых известных проблем математической логики: проблемы остановки машины Тьюринга, проблемы зависимости некоторых аксиом в формализации проективной геометрии и др. Вопрос, обладает ли ANDP свойством семантической полноты, остается открытым.

В.А. Бочаров, А.Е. Болотов и А.Е. Горчаков [Болотов и др.] предложили алгоритм поиска натурального вывода Prover для классической логики предикатов. Спецификой Prover является поиск вывода в натуральных исчислениях типа Куайна с использованием абсолютно и относительно ограниченных переменных. В процессе поиска вывода Prover использует также сколемовские термы. Касаясь вопроса о семантической полноте для Prover, авторы предлагают пути решения данной проблемы. Однако доказательства данного факта для Prover предложено не было.

Группа исследователей под руководством Н.А. Шанина [Шанин и др.] предложила процедуру поиска натурального вывода типа Генцена в классической логике высказываний. Отличительной особенностью данной процедуры является поиск вывода в секвенциальном исчислении. Затем полученный вывод в секвенциальном исчислении перестраивается в натуральный вывод типа Генцена. Отмечая пионерский характер данной работы (она вышла в 1964 году), подчеркнем, что вопрос о семантической полноте процедуры авторами не ставился, поскольку в формулах, для которых требуется найти натуральный вывод, разрешается использовать не более трех пропозициональных переменных. В значительной степени на работы группы под руководством Н.А. Шанина опирается У. Сиг.

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

Целью диссертационного исследования является пересмотр алгоритма поиска натурального вывода типа Куайна в классической логике предикатов первого порядка, предложенного В. А. Бочаровым, А. Е. Болотовым и А. Е. Горчаковым, и доказательство для этого алгоритма теорем о семантической непротиворечивости и семантической полноте.

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

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

- Представить содержательное описание алгоритма поиска вывода в виде формальных правил поиска вывода.

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

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

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

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

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

При решении поставленных задач автор опирался на современный аппарат символической логики. В диссертационной работе использовались формулировки систем натурального вывода, предложенные В. А. Бочаровым, Е. К. Войшвилло, Г. Генценом, Ф. Пеллетье, Дж. Поллоком, В.А. Смирновым и др.

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

Научная новизна исследования.

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

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

■ Предложено оригинальное доказательство теоремы о семантической непротиворечивости для натурального исчисления типа Куайна с абсолютно и относительно ограниченными переменными.

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

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

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

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

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

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

Глава 1. Автоматический поиск натурального вывода: история вопроса

§ 1.1. Натуральный вывод как тип логического вывода

Моментом появления натурального вывода (НВ) как одного из типов

логического вывода традиционно считается выход в 1934 году статьи Г. Генцена

«Исследования логических выводов» [Генцен] и статьи С. Яськовского «Правила

введения посылок в формальной логике» [Jaskowski].

В англоязычной литературе системы НВ называются «natural deduction». В отечественной литературе системы НВ иногда называются «естественным выводом».

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

Г. Генцен писал: «Я хотел прежде всего построить такой формализм, который был бы как можно ближе к применяющимся в действительности рассуждениям» [Генцен, с. 10]. Далее он определяет свою задачу более точно: «Мы хотим построить формализм, по возможности точно передающий логические заключения, которые в действительности встречаются в математических доказательствах» [Генцен, с. 17].

Созданию С. Яськовским систем НВ способствовало замечание Я. Лукасевича, что «математики строят свои доказательства, используя не аксиоматический метод, а иные способы рассуждения; главным образом, математики берут «произвольные посылки» и смотрят, что из этих посылок можно вывести» [Pelletier, с. 4].

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

Приведем цитаты, показывающие достоинства НВ перед другими типами логического вывода. «Естественный вывод гораздо более тонкий инструмент, чем семантические таблицы, обладающий большой аналитической силой и легко модифицируемый» [Непейвода, с. 297]. «Наиболее удобным способом ее (логики предикатов - В.Ш.) задания является система натурального вывода» [Ивлев, с. 95]. «Для применения в качестве логического аппарата наиболее удобными (системами исчисления предикатов - В. Ш.) являются натуральные системы (системы натурального вывода)» [Войшвилло, с. 85].

Размышляя о преимуществах натурального вывода перед методом резолюции, Д. Пеллетье пишет: «Я предположил, что представление вывода в виде натурального на самом деле обладает значительными преимуществами с познавательной точкой зрения: такое максимально обобщенное представление позволяет студентам глубже проникнуть в структуру логических проблем» [Pelletier, с. 6].

Характеризуя гильбертовские исчисления, авторы [Смирнов и др., с. 21] пишут: «Сами способы построения и выводов в этих системах в значительной степени не соответствуют естественным способам рассуждений». Характеризуя секвенциальные и аналитико-табличные исчисления, эти же авторы пишут: «Сам стиль осуществления этих процедур во многом перестает носить «естественный» характер, т.е. перестает соответствовать обычным способам рассуждений» [Смирнов и др., с. 21].

«Логическая система может быть задана различными способами: аксиоматически, в виде табличного исчисления и т. д. Не все из них одинаково удобны для анализа выводов. Самые широкие возможности в этом плане открывают секвенциальные исчисления и системы натурального вывода» [Быстров, с. 139].

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

с. 172].

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

Что касается дедуктивной силы НВ, то, представляя НВ, Г. Генцен конструктивно показал, что в классической логике предикатов НВ дедуктивно эквивалентен исчислению секвенций и гильбертовскому исчислению, т.е. вывод некоторой формулы в одном исчислении можно перестроить в вывод этой же формулы в другом исчислении [Генцен].

Также отметим, что в нашем исследовании используются только системы НВ для классической логики. Поэтому рассмотрение НВ для неклассических логик выходит за рамки нашего исследования. Подробнее о системах НВ для неклассических логик см. [Basin et al].

Возможны различные классификации систем НВ [Pelletier], [Смирнов].

Например, Д. Пеллетье выделяет девять основных пунктов («nine choice points»), по которым можно классифицировать системы НВ. В то же время он признает, что «многообразие систем НВ делает весьма затруднительным выделение необходимых и достаточных признаков, которые позволили бы однозначно назвать некоторую логическую систему натуральным выводом» [Pelletier, с. 11].

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

Первым основным пунктом является тип представления натурального вывода:

1) в виде дерева (Г. Генцен, Н.А. Шанин, Н.Н. Непейвода);

2) в виде линейного вывода (С. Яськовский, Ф. Фитч, В.А. Бочаров и В.И. Маркин), где подвыводы обозначаются некоторыми графическими объектами (скобками, квадратными скобками, линиями и др.);

3) в виде линейного вывода (С. Яськовский, У. Куайн), где подвыводы обозначаются различными (числовыми) префиксами;

4) в виде линейного вывода с множеством зависимостей (П. Суппес, Е. К. Войшвилло).

Вторым основным пунктом является присутствие (Г. Генцен, У. Куайн, Е. К. Войшвилло) или отсутствие (С. Яськовский) в системе НВ некоторых аксиом наряду с правилами вывода.

Назовем систему НВ симметричной, если в ней для любого логического символа (связки или квантора) содержатся хотя бы одно правило введения и хотя бы одно правило удаления (исключения). Тогда наличие (Г. Генцен, Н.Н. Непейвода, В.А. Бочаров и В.И. Маркин) или отсутствие (Д. Пеллетье, Е.К. Войшвилло, Дж. Поллок, А.М. Анисов) симметричности в системе НВ - это третий основной пункт.

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

Обычным непрямым правилом является з_в: если из посылки С выводима формула В, значит, можно построить вывод формулы С з В.

Например, Г. Генцен предложил следующее непрямое правило из формулы А v В, подвывода С из посылки А и подвывода С из посылки В выводима формула С. Однако можно предложить прямое правило из А v В, А з С, В з С выводима формула С, или из А v В, —А выводима формула В.

Д. Пеллетье также отмечает, что прямые и непрямые правила можно вводить для других пропозициональных связок (например, —, =).

Следующие основные пункты 5-9 касаются работы с переменными в системах НВ. Д. Пеллетье отмечает нетривиальность проблемы работы с переменными в системах НВ в сравнении с другими типами логического вывода.

Количество кванторов, которые используются в системах НВ, - это пятый основной пункт. Подавляющее большинство авторов используют и квантор общности, и квантор существования при формулировке своих систем НВ. Исключение составляет, например, С. Яськовский.

Шестой основной пункт - наличие прямого (У. Куайн, В.А. Бочаров и В.И. Маркин) или непрямого (Г. Генцен, Н.Н. Непейвода) правила удаления квантора существования.

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

В таких системах НВ появляется наряду с понятием вывода понятие завершенного вывода, т.е. вывода, в котором заключение логически следует из всех неисключенных посылок этого вывода. Далее мы подробнее остановимся именно на данном основном пункте.

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

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

В то же время, в системе НВ, предложенной В.А. Бочаровым и В.И. Маркиным, наличие произвольной переменной в формулировке правила У_в задается неявным образом.

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

Восьмым основным пунктом является разделение всех систем НВ на те, которые допускают вхождение свободных переменных в посылки и заключение выводов (У. Куайн, В. А. Бочаров и В. И. Маркин), и на те, которые не допускают посылок и заключений такого вида, т.е. посылки и заключения в таких системах могут быть только предложениями (В.А. Смирнов).

Дополнительно отметим, что возможна условная (В. А. Бочаров и В. И. Маркин) и универсальная (Д. Пеллетье) интерпретация свободных переменных.

Наконец, девятым основным пунктом является наличие (Дж. Поллок, В.А. Смирнов) или отсутствие (У. Куайн, В.А. Бочаров, В.И. Маркин) особых термов в формулировках кванторных правил.

Например, В.А. Смирнов формулирует кванторные правила У_в, З_и с помощью s-термов, содержательно трактующихся как неопределенные дескрипции.

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

В данной классификации система НВ, названная NC, с непрямым правилом удаления 3 называется системой НВ первого типа. Второй тип систем НВ (в качестве примера предлагается система NsC) содержит в множестве своих правил прямое правило удаления 3. Ниже мы подробно проанализируем систему NsC.

В оригинальной системе, предложенной Г. Генценом, имеется непрямое правило удаления 3: из формулы 3xA(x) выводима формула С, если формула С выводима из A(a), где a - новая, ранее не встречавшаяся в выводе константа. Таким образом, чтобы получить по такому правилу формулу С из формулы 3xA(x), необходимо построить вспомогательный вывод (он называется подвыводом) формулы С из формулы A(a). Только после построения такого подвывода можно утверждать, что из формулы 3xA(x) выводима формула С.

По-видимому, первым, кто обратил внимание на неудобство применения этого правила и кто предложил альтернативный вариант удаления 3, был У. Куайн [Quine]. В статье «On natural deduction» он сформулировал прямое правило удаления 3: из формулы 3xA(x) выводима формула A(y), где y - переменная, которая в алфавитном порядке не предшествует ни одной переменной, свободно входящей в 3xA(x).

Формулировка данного правила предполагает наличие некоторого упорядочения всех переменных из алфавита языка классической логики предикатов. Фактически речь идет о линейном порядке, заданном на множестве переменных языка. У. Куайн показывает, что именно такой порядок гарантирует непротиворечивость и полноту предложенной им системы НВ.

Однако подход У. Куайна не является единственным. Например, В. А. Смирнов в системе NsC предлагает следующую формулировку прямого правила удаления 3: из формулы 3xA(x) следует формула A(sxA(x)), где sxA(x) - это s-терм, содержательно трактующийся как неопределенная дескрипция вида «некоторые x, обладающие свойством А» [Смирнов].

Поскольку s-термы не являются термами классической логики предикатов, то система NsC не эквивалентна системе NC (системе НВ с непрямым правилом удаления 3, предложенной В.А. Смирновым там же): все, что доказуемо в NC, доказуемо в NsC, но обратное неверно.

Однако для NsC можно доказать теорему Гильберта об устранении s-термов: если в NsC можно из (возможно, пустого) множества посылок Г вывести А и Г, А не содержат s-термы, то А следует из Г в NC [Смирнов, с. 228], [Мендельсон, с. 111-112].

В. А. Бочаров и В. И. Маркин предлагают вводить абсолютно ограниченные и относительно ограниченные переменных в выводе. Тогда правило удаления 3 запишется следующим образом: из формулы 3xA(x, z^..., z_n) выводима формула A(y, z^..., z_n), при этом переменная y становится абсолютно ограниченной в выводе переменной, а все переменные z1,., zn - относительно ограниченными в выводе переменными (z1,., zn суть все свободные переменные из 3xA(x)).

При этом требуется, чтобы ни одна переменная не была абсолютно ограничена в выводе более одного раза и чтобы ни одна переменная не ограничивала сама себя (непосредственно, т.е. y не входит в z1,., zn, или по транзитивности, т.е. если x ограничивает y и y ограничивает x, то x ограничивает x). Во второй главе нашей работы показывается, что такой подход гарантирует непротиворечивость этой системы НВ.

Мы подробно останавливаемся на системах НВ с прямым правилом удаления 3, поскольку система BMV (Bocharov, Markin, Voishvillo), алгоритм поиска вывода в которой является предметом нашей работы, - система НВ именно такого типа.

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

В англоязычной литературе известна серия публикаций 60-70-х гг. XX века в «The Journal of Symbolic Logic» по поводу системы НВ, предложенной И. Копи (I. Copi). И. Копи публиковал не являющиеся семантически непротиворечивыми системы НВ с прямым правилом удаления 3 [Copi]. Семантическая противоречивость предлагаемых И. Копи систем НВ была установлена Д. Калишем (D. Kalish) [Kalish].

Не является семантически непротиворечивой система НВ, предложенная Е. К. Войшвилло [Войшвилло]. В этой системе доказывается, например, формула 3y(VxA(x, x) з VzA(y, z)). Данная формула ложна, если в качестве А взять отношение равенства на множестве натуральных чисел.

§ 1.2. История создания систем автоматического поиска вывода

В данном параграфе мы даем краткий обзор истории создания систем

автоматического поиска вывода. Поскольку неотъемлемой частью создания таких

систем является наличие программируемых электронно-вычислительных устройств, в

начале данного параграфа приводятся некоторые факты из истории создания ЭВМ.

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

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

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

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

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

В дальнейшем стали создаваться машины, совершенствующие модель Бэббиджа. В 1855 году Дж. и Э. Шутц, базируясь на работах Ч. Бэббиджа, построили свою механическую вычислительную машину. В 1869 году У.С. Джевонс, используя результаты Дж. Буля, построил усовершенствованную модель этой машины. В 1896 году Г. Холлерит создал первую электромеханическую вычислительную машину и основал фирму, которая впоследствии превратилась в корпорацию IBM.

Промежуток времени между двумя мировыми войнами считается сегодня периодом рождения первого компьютера. В 1927 году в Массачусетском технологическом институте был изобретен аналоговый компьютер. В 1937 году Дж. Стибитц построил первую вычислительную машину на основе двоичной системы счисления.

В 1938-41 гг. К. Цузе предложил несколько моделей (Z1, Z2 и Z3) своей механической программируемой цифровой машины. Модель Z1 иногда называют первым в мире компьютером. В 1942 году в Университете штата Айова Дж. Атанасов и К. Берри создают первый в США электронный цифровой компьютер.

В России созданием «умных» машин занимались П.Д. Хрущов и А.Н. Щукарев. Создание вычислительных машин активно велось в советское время.

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

Первая программа была создана М. Дэвисом на ламповом компьютере "Johniac". Эта программа могла доказать, что сумма двух четных чисел является четным числом - первое в истории доказательство математического утверждения, генерированное компьютером.

Вторая программа, которая могла доказывать ряд предложений из "Principia Mathematica" Б. Рассела и А.Н. Уайтхеда, была создана А. Невелом, Дж. К. Шоу и Г. Саймоном. Эта программа ориентировалась на человеческий способ рассуждений, пытаясь симулировать общие эвристические подходы и психологические моменты мышления.

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

В 1961 году М. Минский подвел итог этой дискуссии: «Кажется ясно, что программа решения реальных математических проблем должна комбинировать математические рассуждения... с эвристическими рассуждениями Невела, Шоу и Саймона».

В 1958-63 гг. Х. Ван предложил несколько версий своей первой логикоориентированной программы фирмы IBM по автоматическому доказательству. Это был большой шаг вперед: его программа могла доказывать около 350 предложений «Principia Mathematica» для чистого исчисления предикатов с равенством.

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

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

В 1960 году эту проблему решил Д. Правиц посредством механизма, названного унификацией. Позже был предложен унифицирующий алгоритм.

Независимо от этого над доказательствами математических утверждений в национальной лаборатории Аргонны работали Д. Карсон, Дж. Робинсон и Л. Уос. Ученые поставили перед собой задачу разработать такой принцип, в котором бы объединились различные методы в одно общее логическое правило.

В 1963-1965 гг. такое правило было найдено, и Дж. Робинсон публикует свою работу "A machine oriented logic, based on the resolution principle" [Robinson]. С тех пор метод резолюции прочно вошел в практически любую образовательную программу по логике и информатике.

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

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

К первому лагерю принадлежали ученые национальной лаборатории Аргонны под руководством Л. Уоса и группа под руководством Б. Мелтцера в университете Эдинбурга. В 1965-75 гг. они предложили десятки усовершенствованных стратегий поиска вывода.

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

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

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

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

В 60-е годы XX века Л. М. Нортон предложил эвристический прувер для теории групп, а А. Невинс - алгоритм, разрабатываемый на базе «человекоориентированной логики». Результаты данных программ оказались не достижимыми для резолюционных процедур того времени. Здесь можно отметить работу исследователей университета Техаса, развивавших специализированные методы доказательства для конкретных областей математики.

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

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

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

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

Системы доказательства теорем разбиваются на два больших лагеря. Первый лагерь - это системы интерактивного доказательства теорем (proof checker), другое название этих систем - редакторы доказательств.

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

Примером редактора доказательств является система AUTOMATH, которая создана для проверки математических доказательств. В этой системе доказывается значительная часть теорем из чистой математики. Однако запись доказательств в AUTOMATH, как правило, в 10-20 раз длиннее, чем в естественном языке.

Из отечественных работ можно привести программу DEDUCTIO, разработанную А.В. Смирновым при участии А.Е. Новодворского [Смирнов-мл]. Эта программа позволяет работать не только с одной стандартной логической системой, но и делать выбор из довольно широкого списка известных систем. Программа предоставляет также пользователю возможность описать некоторую собственную систему, после чего она автоматически начинает ее поддерживать.

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

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

Разработки программ в области автоматической дедукции проводятся в целом ряде крупных мировых научно-исследовательских центров. В национальной лаборатории Аргонны создана программа OTTER, основанная на теории резолюций. OTTER является последним продуктом в цепи систем (AURA, ITP), которые были созданы под руководством Л. Уoca. Программа создана для поиска доказательств для классической логики предикатов первого порядка с равенством, написана на языке С, занимает примерно 180 Кб и способна оперировать большим количеством дизъюнктов (миллиардами), что показывает ее высокую эффективность.

В Кембридже создана программа автоматической дедукции Isabelle. В Карнеги-Меллон университете создана программа для автоматического доказательства теорем для логики высоких порядков. В лаборатории KAKEHI и Университете WASEDA создана программа автоматического доказательства для секвенциального исчисления

В отечественной науке подобные программы начали создаваться также достаточно давно. В 60-е годы XX века под руководством Шанина Н.А. разработан алгоритм машинного поиска логического вывода [Шанин и др.]. Программа, реализованная по этому алгоритму, ищет вывод в классическом секвенциальном исчислении высказываний и перерабатывает его далее в натуральный вид.

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

Надо отметить, что концентрация внимания исследователей в области автоматического вывода на этих популярных дедуктивных методах не случайна и обусловлена, в первую очередь, практическими соображениями. Так, например, исследования в области теории резолюций тесно связаны с языками логического программирования (в частности, типа Пролог), где выводы основаны на методе резолюций, который изначально являлся составной частью Пролога [Братко].

Еще одной причиной такой ситуации является факт достаточно успешного практического применения неклассических логик в рамках различных проектов тестирования аппаратных средств [Bochmann], нередко спонсирующихся ведущими производителями таких средств (например, Intel).

На сегодняшний день самым распространенным и эффективным методом в данной области является метод тестирования моделей. В данном методе для описания моделей аппаратных средств используется дедуктивный аппарат, чаще всего основанный на модальной или временной логике, семантика для которых чаще всего строится в форме аналитических таблиц [Bochmann], [Bolotov & Fisher].

§ 1.3. Автоматический поиск вывода в натуральном исчислении

В данном параграфе мы анализируем алгоритмы поиска натурального вывода,

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

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

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

1) программа THINKER, разработанная Д. Пеллетье (J. Pelletier) [Pelletier];

2) программа OSCAR, разработанная Дж. Поллоком (J. Pollock) [Pollock];

3) программа ANDP (Automated Natural Deduction Prover), разработанная

Д. Ли (D. Li) [Li];

4) программа CMU PT (Carnegie Mellon University Proof Tutor), разработанная У. Сигом (W. Sieg), Р. Шейнсом (R. Scheines) и Дж. Бернсом (J. Byrnes) [Sieg], [Sieg & Byrnes], [Byrnes];

5) программа Symlog (Symbolic Logic), разработанная Ф. Портораро (F. Portoraro) [Portoraro];

6) программа Prover, разработанная В.А. Бочаровым, А.Е. Болотовым и А.Е. Горчаковым и модифицированная В. О. Шангиным [Болотов и др.], [Болотов и др.1], [Шангин], [Bocharov et al].

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

1) алгоритм работает с предикатом равенства;

2) алгоритм работает с эквиваленцией;

3) алгоритм работает с неклассическими логиками;

4) множество используемых алгоритмом переменных ограничено;

5) для алгоритма доказываются теоремы о его свойствах (непротиворечивость, полнота и т.д.);

6) алгоритм использует сколемовские термы;

7) алгоритм имеет программную реализацию.

Значениями данной таблицы будут символы: + (признак имеется), - (признак отсутствует) и +- (требует доработки).

		Thinker	Oscar	ANDP	CMU PT	Symlog	Prover
1	=	+	-	-	-	-	-
2	=	+	-	+	-	+	-
3	Неклассика	+	+	-	+	-	+
4	Ограничение на переменные	+	-	-	-	-	-
5	Свойства	-			+	-	+
6	Явная сколемизация	-	+	-	+	+	-
7	Реализация	+	+	+	+	+

Комментарий.

Из перечисленных программ только Thinker работает с предикатом равенства. Соответственно, среди предложенных программ только Thinker может построить вывод для всех 75 проблем, предложенных в [Pelletier2], [Pelletier3]. Данный факт неудивителен, поскольку у Thinker и у списка 75 тестовых задач для алгоритма поиска вывода один и тот же автор - Д. Пеллетье.

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

Безусловным преимуществом алгоритма является возможность работы не только в классической, но и в неклассических логиках. Программа Thinker умеет работать в модальной логике [Pelletier]; программа Oscar - в логике «отменяемых» (defeasible) рассуждений; программа ANDP - в интуиционистской логике, и, наконец, можно рассматривать работы [Макаров], [Шангин1], [Шангин3] о поиске вывода в интуиционистской логике высказываний как перенесение идей Prover на интуиционистскую логику.

Только программа Thinker допускает ограничение (по умолчанию - 20) на количество переменных, которое можно использовать при построении вывода. По желанию пользователя, это количество может меняться. Однако наличие данного ограничения принципиально для поиска вывода. Если множество таких переменных исчерпано (т.е. все n переменных использованы в выводе), то поиск вывода прекращается.

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

Строка «Свойства» отмечает разработанность метатеоретических проблем для данных алгоритмов. Например, «+-» столбце для Oscar и ANDP означает: доказано, что данные алгоритмы семантически непротиворечивы, т. е. все, что доказуемо, является логически общезначимым; и не доказано, что данные алгоритмы семантически полны, т. е. с помощью данных алгоритмов можно доказать все логически общезначимые формулы. Дж. Поллок, автор Oscar, предполагает, что его программа полна в указанном смысле, однако доказательства этого факта пока нет.

По разным причинам, метатеоретическая проблематика отсутствует для программ Thinker и Symlog. По словам Ф. Портораро, автора программы Symlog, «мы считаем вопрос о полноте алгоритма второстепенным: во-первых, он слишком далеко отстоит от темы нашего исследования; во-вторых, он не отвечает задачам алгоритма. Задача нашего алгоритма - предоставлять всестороннюю помощь при построении вывода, а не болезненно строить формальные выводы определенного вида. Поэтому вопрос о полноте нашего алгоритма отходит на второй план и вовсе исчезает тогда, когда алгоритм начинает оказывать помощь при работе с другими формальными системами, например, с арифметикой или теорией множеств» [Portoraro, с. 59].

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

Что касается Thinker, то данный алгоритм неполон, если учесть вышеуказанное ограничение на количество используемых в выводе переменных: «Очень трудно оценить семантическую полноту программы Thinker потому, что он может прийти к пункту J (остановка алгоритма) в различных случаях; в том числе и тогда, когда формула является логически общезначимой, Thinker может остановиться, потому что кончатся переменные» [Pelletier, с. 33]. С другой стороны, он пишет, что неясен ответ на вопрос, будет ли Thinker семантически полон, если данное ограничение на количество переменных будет снято.

Теорема о семантической полноте доказана для CMU PT. Предложенный У. Сигом метод (см. также [Sieg], [Sieg & Byrnes], [Byrnes]) заключается в том, что по дереву вывода, которое не является доказательством, можно построить контрмодель для данной формулы или для данной выводимости. Т.е. если формула не доказуема, то найдется (возможно, бесконечный) контрпример, показывающий, что при данных значениях исходная формула принимает значение «ложь». Сходным образом доказана семантическая полнота для Prover. О различиях в указанных подходах подробно говорится в конце данного параграфа.

Не все алгоритмы используют в своей работе сколемизацию. Под сколемизацией здесь имеется ввиду явная сколемизация, т. е. добавление в язык логики предикатов особых свободных переменных и предметных функторов, с помощью которых образуется сколемовский терм. Сколемизация осуществляется в Oscar, CMU PT и Symlog.

Однако поиск вывод не обязательно предполагает явную сколемизацию. Существуют различные формы неявной сколемизации. Например, Thinker предполагает в процессе поиска вывода использовать т.н. «шаблоны» (templates), которые при окончательном построении вывода превращаются в формулы. Например, снятие V с формулы VxA(x, y) порождает шаблон A(@, y). Prover также использует неявную сколемизацию, о чем подробно говорится далее.

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

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

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

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

Глава 2. Анализ системы натурального вывода BMV

§ 2.1. Формулировка системы BMV

Задается алфавит языка L классической логики предикатов:

1. х, у, z, xi, yi, zi, x₂,... - бесконечный список индивидных переменных,

2. a, b, c, a₁, b₁, c₁, a₂,... - бесконечный список индивидных констант,

3. f, g, h, f₁, g₁, h₁, f₂,... - бесконечный список предметно-функциональных констант (функторов) различной местности,

4. Р, Q, R, P₁, Q₁, R₁, P₂,... - бесконечный список предикаторных констант (предикаторов) различной местности,

5. &, v, з, —, V, 3 - логические символы,

6. (, ), , - технические символы.

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

Определение 2.1.1. Термом является объект, обладающий следующими свойствами:

1. Произвольная индивидная переменная есть терм,

2. Произвольная индивидная константа есть терм,

3. Если Ф - n-местный функтор, а t₁, t₂,..., t_n - термы, то выражение Ф(^, t₂,..., t_n) -терм.

4. Ничто иное не является термом.

Определение 2.1.2. Формулой является объект, обладающий следующими свойствами:

1. Если П - n-местный предикатор, а t₁, t₂,..., t_n - термы, то выражение П(^, t₂,..., t_n) - формула,

2. Если А - формула, то — А - формула,

3. Если А и В - формулы, то (А & В), (А v В), (А з В) - формулы,

4. Если А - формула и а - индивидная переменная, то VаА и 3аА - формулы,

5. Ничто иное не является формулой.

Формулы, определяемые пунктом 1, называются элементарными формулами. Все остальные формулы называются сложными формулами. Буквами А, В, С,... (с индексами и без них) обозначаются произвольные формулы.

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

В выражениях VaA и ЗаА формула А называется областью действия кванторов V и З, взятых по индивидной переменной а.

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

Вхождение квантора в выражениях VaA и ЗаА называется вырожденным, если ни одно вхождение переменной а не находится в А. Например, вхождение V в формулу Vx3yP(y) вырождено. Если некоторое вхождение переменной а в А связано двумя или более вхождениями кванторов по а, то все эти вхождения кванторов по а, кроме самого правого, являются вырожденными [Непейвода, с. 184]. Например, вхождение V в формулу Vx3хP(х) вырождено.

Пусть t - терм, а - индивидная переменная. Тогда выражение вида А(аЛ) обозначает результат подстановки в формулу А(а) вместо всех свободных вхождений а терма t. Подстановка A^/t) считается правильной, если никакое свободное вхождение а не лежит в области действия никакого квантора по каждой переменной, входящей в терм t.

Частным случаем выражения А(аЛ) является выражение A^/p), обозначающее правильную подстановку в А переменной Р вместо переменной а. При этом фиксируется множество всех свободных переменных уь..., y_n в А и Р g (Уь-•, y_n). Данное выражение обозначается как A^/p, уь..., y_n).

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

Задаются следующие правила системы BMV (BMV-правила):

А, В А & В А & В

&_в ---------------------------------------------------- &и ---------------------------- --------------------------------

^в А & В А В

А В А v В, -А

Vв -------------------------------------------------- -------------------------------------- v„ -----------------------

А v В А v В В

В А з В, А

С з В В

В, -В --А

-С А

VaA(a, yi,..., yn) Уъ---, Yn - огр. A(a/t)

A(a/t) ЗаA(a, у_ь..., yn) p - абс.;

Зв ------------------------------------------------------------------------------------------------------------------------ Зи ----------------------------

3aA(a) A(a/p, у_ь..., Yn) Уь-.., Yn - огр.

В правилах з_в и -_в формула С является последней неисключенной посылкой (это понятие будет разъяснено ниже). А(аЛ) и A(a/p) - результаты правильной подстановки.

В правилах V,, и З_и запись «p - абс.; уь-.., y_n - огр.» означает, что p абсолютно ограничена в выводе и переменная p относительно ограничивает в выводе каждую переменную из множества Уь-.., y_n, где (уь-.., y_n} - это множество всех свободных переменных, входящих в посылки данных правил.

В дальнейшем мы иногда вместо «p относительно ограничена в выводе» будем писать «p ограничена», не указывая на ту переменную, которая относительно ограничивает p, а вместо «p абсолютно ограничена в выводе» - «p абсолютна». Переменные, не ограниченные абсолютно в выводе, будут называться неабсолютными. Содержательный смысл понятий «абсолютно ограниченная переменная» и «относительно ограниченная переменная» см. [Бочаров и Маркин, с. 133-134].

A(a/p, уь..yJ p - абс.; VaA(a)

Определение 2.1.3. Выводом в системе BMV (В]У^-выводом) называется непустая конечная последовательность формул С₁, C₂,..., C_n (n > 1), удовлетворяющая следующим условиям:

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

2. при применении правил з_в и —_в все формулы, начиная с последней неисключенной посылки С; (1 > i > n) и вплоть до результата применения данного правила C_; з Cj (1 > j > n) или —С_;, исключаются из дальнейших шагов вывода в том смысле, что к ним запрещено применять правила вывода;

3. ни одна индивидная переменная в выводе не ограничивается абсолютно более одного раза;¹

4. ни одна переменная не ограничивает в выводе сама себя.

Выводом формулы В из непустого множества посылок Г называется BMV-вывод, в котором множество неисключенных посылок есть Г и последняя формула есть формула В.

Доказательством формулы В называется BMV-вывод формулы В из пустого множества неисключенных посылок.

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

Проанализируем правила системы.

Правила для конъюнкции, а также правило введения дизъюнкции, обычны для систем натурального вывода: их можно обнаружить в [Генцен].

Что касается правила для исключения дизъюнкции, то иногда его формулируют в виде правила разбора случаев (р.с.): из A v B, A з C, B з C следует C. Известно, что р.с. сильнее, чем Vj, в том смысле, что, например, в интуиционистской логике можно показать с помощью р.с. производность но невозможно показать с помощью v_и производность р.с.. Однако существуют определенные трудности с построением процедуры поиска натурального вывода типа Куайна с правилом р.с. [Макаров].

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

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

Правило -_и (снятие двойного отрицания) стандартно.

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

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

Пусть ЗуР(у) - формула, причем P - одноместный предикатор. Можно, например, не нарушая требования правильной подстановки, получить из ЗуР(у) по З_и формулу P(x), затем применить V,, и получить VyP(y). Из VyP(y) с помощью правил З_в можно снова получить ЗуР(у) и т.д.

Отметим, что в системе BMV такие бесконечные преобразования формул ограничиваются понятием вывода. Однако нам важен тот факт, что такие

Иногда пишут «не может абсолютно ограничиваться дважды». При этом Е.К. Войшвилло отмечал, что данное требование можно нарушить без ущерба для корректности, «когда правило Vjj или З_и вторично применяется для вывода из той же формулы» [Войшвилло, с. 90-91].

преобразования возможны, если не следовать понятию вывода, а следовать только формулировкам У_в, З_и и требованию правильной подстановки.

Иногда формулировки данных правил не позволяют такие взаимопревращения формул [Войшвилло]. Более того, Дж. Пеллетье вообще не формулирует правила введения квантора общности явным образом. Аналог этого правила имплицитно содержится в формулировке достижимости некоторого подвывода [Pelletier].

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

У. Куайн, например, явно указывает на наличие абсолютно ограниченных (flagged) переменных и не указывает явно на наличие относительно ограниченных переменных. Однако он задает свободные переменные в алфавитном порядке и требует, чтобы при применении правил З_и, У_в новая свободная переменная не предшествовала в алфавитном порядке имеющимся в формуле свободным переменным [Quine]. Именно таким образом У. Куайн избегает самоограничения переменной.

Касаясь правил вывода нашего исчисления в целом, отметим их симметричность: каждой логической связке соответствуют хотя бы одно правило исключения и хотя бы одно правило введения. Свойство симметричности правил натурального вывода идет от работ Г. Генцена [Генцен]. См. также [Fitch]. В то же время симметричность правил не является необходимым свойством натурального вывода. Можно указать на системы натурального вывода, где данное свойство не выполняется [Pelletier].

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

Требование, чтобы в правилах з_в, —_в формула С была последней
неисключенной посылкой, обосновывается следующим образом:
Г 1 А - пос.

| 2 В - пос.

| ....

|_ n C - BMV-правило

В данном выводе мы от вывода формулы С из посылок A, B по правилу зв перешли к доказательству формулы A з C. Однако такой переход семантически неверен, т.е. из A, B |= C не следует |= A з C.

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

Обоснование требования не ограничивать абсолютно некоторую переменную более одного раза, а также требований наличия завершенного вывода, можно найти в [Quine, стр. 97-99].

Что касается запрета на самоограничение переменной, которого нет в [Quine], то он обосновывается, например, невозможностью построения завершенного вывода 3xVyA(x, y) из Vy3xA(x, у) [Бочаров и Маркин, с. 136].

Необходимость введения понятия завершенного вывода (доказательства), наряду с понятием вывода (доказательства), является характерным свойством выводов в первопорядковых натуральных исчислениях типа Куайна, где в общем случае заключение не следует из своих посылок: «При незавершенности вывода не обеспечена истинность заключения при истинности посылок» [Войшвилло, с. 94].

Натуральные исчисления типа Куайна [Quine], [Войшвилло], [Бочаров и Маркин], [Ивлев] противопоставляются натуральным исчислениям типа Генцена [Генцен], [Fitch], [Li], не требующим введения понятия завершенного вывода.

В качестве примеров приведем завершенный BMV-вывод -3xP(x) |- Vx-P(x).

1 -3xP(x)

Г 2 P(x) - пос.

L 3 3xP(x) - Зв: 2

4 -P(x) - -в: 1, 3

5 Vx-P(x) - V„: 4 x - абс. огр Комментарий.

Помещаем формулу -3xP(x) в качестве посылки. Берем другую посылку P(x). Применяя к этой формуле правило З_в, выводим формулу 3xP(x). Поскольку формула -3xP(x) (шаг 1) противоречит формуле 3xP(x) (шаг 3), на шаге 4 выводим формулу -P(x), применяя правило -_в. Формула -P(x) является отрицанием последней неисключенной посылки P(x). При этом все формулы, начиная с формулы P(x) и заканчивая формулой 3xP(x), исключаются из дальнейших шагов вывода. Применяя к формуле -P(x) правило V,,, выводим формулу Vx-P(x). При этом переменная х является абсолютно ограниченной в выводе.

Данная последовательность формул является завершенным выводом формулы Vx—P(x) из посылки —3xP(x), поскольку она является выводом формулы Vx—P(x) из посылки —3xP(x) и абсолютно ограниченная переменная х не входит свободно ни в Vx—P(x), ни в —3xP(x).

§ 2.2. Семантическая непротиворечивость системы BMV

Определение 2.2.1. Переменная а называется активной (пассивной) в BMV-

выводе, если а абсолютно ограничена в этом выводе и (не) существует абсолютно

ограниченная в этом выводе переменная в, которую относительно ограничивает

переменная а.

При применении правила V,, к формуле А(а/р, Уь-.-, Y_n) выводится формула VаА(а), переменная в становится абсолютно ограниченной и в относительно ограничивает все переменные из Уь -. •, y_n.

При применении правила 3и к формуле 3аА(а) выводится формула А(а/в, Уь-.., y_n), переменная в становится абсолютно ограниченной и в относительно ограничивает все переменные из Уь -. •, y_n.

Построим следующий завершенный вывод 3xVyA(x, y) |- 3xVzA(x, z).

1. 3xVyA(x, y) - пос.

2. VyA(x, y) - 3_и: 1; x - абс.

3. A(x, y) - Vи: 2

4. VzA(x, z) - V_в: 3; y - абс., x - отн.

5. 3xVzA(x, z) - 3_в: 4

В этом выводе переменная x пассивна и переменная y активна, поскольку абсолютно ограниченная переменная y относительно ограничивает другую абсолютно ограниченную переменную x на шаге 4.

Лемма 2.2.2. В произвольном BMV-выводе D с непустым множеством М всех абсолютно ограниченных переменных в D найдется переменная а: а е М и а не ограничивает относительно в D ни одну переменную из М.

Доказательство: от противного.

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

² Техникой доказательства этой леммы мы обязаны В.М. Попову.

Для всякой переменной а, пусть [а] - это множество всех переменных из М, каждую из которых а ограничивает относительно в D, и пусть для всякого непустого множества X переменных (X)_min есть переменная из X, которая нестрого предшествует в алфавитном порядке переменных любой переменной из X.

Поскольку произвольный BMV-вывод конечен (определение 2.1.3), найдется такое натуральное число n: М есть n-элементное множество. Пусть для определенности n₀ есть натуральное число и М есть no-элементное множество.

Рассмотрим последовательность множеств М1, М2, Мп₀, Mn₀+1,

определяемую следующим образом: М₁ = [(M)_min], Mk+1 = [(Mk)_min], 1 < k < n₀.

Легко видеть, что все множества М1, М2, Мп₀, Mn₀+1 непусты, а (M1)_min, (M2)_min, ..., (Mn₀)_min, (Mn₀+1)_min - это переменные, принадлежащие множеству М.

Ясно, что для любого i и для любого j, 1 < i < j < n₀ +1, переменная (Мщ)_ть ограничивает относительно в D переменную (Мп^ишь

Отсюда из антирефлексивности и транзитивности отношения «переменная . ограничивает относительно в D переменную .» получаем, что (M1)min, (M2)min, ., (Mn0)min, (Mn0+1)min попарно различны.³

Но все они принадлежат множеству М. Следовательно, множеству М принадлежит не менее n0+1 элементов, что противоречит тому, что М есть n0-элементное множество.

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

Доказано.

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

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

Подробный логический анализ данного отношения проводится в параграфе 3.1 нашего исследования.

Таким образом, важным параметром любого завершенного вывода является число применений в нем правил вывода. Будем обозначать это число посредством q. Из определения вывода следует, что q > 0.

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

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

Лемма 2.2.3. В произвольном завершенном выводе, число применений правил вывода в котором есть q и ранг которого есть r, последняя формула этого вывода семантически следует из множества всех неисключенных в этом выводе посылок.

Доказательство.

Данная лемма будет доказана методом двойной математической индукции по числу применений правил вывода и по рангу произвольного завершенного вывода. В обосновании данного метода мы следуем [Смирнов, с. 122-123].

Запишем сокращенно данную лемму в виде VqVrJI(q, r).

Для доказательства этой леммы достаточно доказать три утверждения:

(А) J (0, 0)

(Б) Vm(m < n з VrJ(m, r)) з Л(п+1, 0)

(С) Vn(n < r з Л(п, ri)) з Л(п, г+1)

Принцип полной математической индукции имеет вид

{A(0) & Vn[Vm(m < n з A(m)) з A(n+1)]} з VnA(n)

Пусть A(n) равняется VrJ(n, r), тогда

(I) {VrJ(0, r)& Vn[Vm(m < n з VrJ(m, r)) з VrJ(n+l, r)]} з VnVrJ(n, r) Пусть A(r) равняется Л(п, r), тогда

(II) {Л(п, 0) & Vr[Vri(ri < r з Л(п, ri)) з Л(п, r+1)]} з VrJ(n, r) покажем, что из (А), (Б), (С), (I) и (II) следует VqVrJ(q, r).

1. {Л(0, 0) & Vr[Vr₁(r₁ < r з Л(0, r₁)) з Л(0, r+1)]} з VrЛ(0, r) (II), n = 0

2. Л(0, 0) (A)

3. Vr₁(r₁ < r з Л(0, r₁)) з Л(0, r+1) (C), n = 0

4. Vr(Vr₁(r₁ < r з Л(0, r₁)) з Л(0, r+1)) V_в: 3

5. Л(0, 0) & Vr(Vr₁(r₁ < r з Л(0, r₁)) з Л(0, r+1)) &_в: 2, 4

6. V^(0, r) з_и: 1, 5

7. Vm(m < n з VrЛ(m, r)) з Л(п+1, 0) (Б)

8. {Л(п+1, 0) & Vr[Vr₁(r₁ < r з Л(п+1, r₁)) з Л(п+1, r+1)]} з V^(n+1, r) (II), n = n+1

9. Vr₁(r₁ < r з Л(п+1, r₁)) з Л(п+1, r+1) (C), n = n+1

10. Vr(Vr₁(r₁ < r з Л(п+1, r₁)) з Л(п+1, r+1)) V_в: 9

K з M, L, (M & L) з D |-

11. Vm(m < n з VrЛ(m, r)) з VrЛ(n+1, r)

K з D: 7, 8, 10

12. Vn(Vm(m < n з V^(m, r)) з VrЛ(n+1, r)) V,,: 11

13. {VrЛ(0, r)& Vn[Vm(m < n з VrЛ(m, r)) з VrЛ(n+1, r)]} з VqV^(q, r) (I)

14. VrЛ(0, r) & Vn(Vm(m < n з VrЛ(m, r)) з VrЛ(n+1, r)) 6, 12

15. VqV^(q, r) з_и: 13, 14

Поэтому доказательство леммы сводится к доказательству утверждений (А), (Б) и (С).

(А) Л(0, 0): лемма верна для всех завершенных выводов, ранг и число применений правил вывода в которых равны 0.

Пусть последовательность формул С₁, C₂,..., С_t (t > 1) есть завершенный вывод, ранг и число применений правил вывода в котором равны 0. Для доказательства Л(0, 0) достаточно показать, что формула С семантически следует из множества всех неисключенных посылок в выводе С₁, C₂,..., С_t.

По определению семантического следования, получаем, что {С₁, C₂,..., С_t} |= С_t. Но множество {С₁, C₂,..., С_t} есть множество всех неисключенных посылок в выводе С₁, C₂,..., С_t. Поэтому С_t семантически следует из множества всех неисключенных посылок в выводе С₁, C₂,..., С_t.

Таким образом, имеет место Л(0, 0).

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

Ранг вывода равен 0, значит, в выводе не применялись правила V,,, З_и.

Таким образом, (Б) распадается на 10 случаев по количеству BMV-правил (все BMV-правила, кроме Vj,, 3_и).

- Последняя формула завершенного вывода получена по правилу &_и.

Тогда вывод имеет следующий вид: С₁, C₂,..., Cj,-.., Q, где t > 0, t > j, С] есть A & C_t и С есть В.

Вывод С₁, C₂,..., Cj является завершенным, т.к. в выводе С₁, C₂,..., Cj,-.., С_t не применялись правила V,,, 3_и.

По индуктивному предположению, Г₁ |= Cj, где Г₁ (Г₁ с: Г) - множество неисключенных посылок из С₁, C₂,..., Cj и Г - множество неисключенных посылок из С₁, C₂,..., Cj,-.., С_t. Значит, Г₁ |= A & B.

Учитывая Г₁ |= A & B и A & B |= B, получаем Г₁ |= B. Отсюда, используя Г₁ с: Г, получаем Г |= B.

Подслучай, когда СJ есть C_t & А, рассматривается симметрично.

Аналогичным образом рассматриваются еще 4 случая однопосылочных правил: v,,, —_и, V_и и 3_в.

- Последняя формула завершенного вывода получена по правилу &_в.

Тогда вывод имеет следующий вид: С₁, C₂,..., Cj,-.., С_;,..., С_t, где t > 1, t > j, t > i, С есть A, C_; есть В и С есть А & В.

Вывод С₁, C₂,..., Cj является завершенным, т.к. в выводе С₁, C₂,..., Cj,-.., С_;,..., С_t не применялись правила V,,, 3_и.

Вывод С₁, C₂,..., C_; является завершенным, т.к. в выводе С₁, C₂,..., Cj,-.., С_;,..., С не применялись правила V_в, 3_и.

По индуктивному предположению, Г₁ |= Cj, где Г₁ (Г₁ с: Г) - множество неисключенных посылок из С₁, C₂,..., Cj и Г - множество неисключенных посылок из С_ь C2,-.., Cj,-.., С;,..., С Значит, Г1 |= A.

По индуктивному предположению, Г₂ |= C_;, где Г₂ (Г₂ с: Г) - множество неисключенных посылок из С₁, C₂,..., C_; и Г - множество неисключенных посылок из С1, C2,-.., Cj,-.., С;,..., Сt. Значит, Г2 |= B.

Аналогичным образом рассматриваются еще 2 случая однопосылочных правил: v_и и з_и.

- Последняя формула завершенного вывода получена по правилу -_в.

Тогда вывод имеет следующий вид: С₁, C₂,..., d,..., Cj,..., Q,..., Q, где t > 2, t > j, t > i, t > h, С есть D, C_i есть -D и С есть -C_h, где C_h есть последняя неисключенная посылка в выводе.

Вывод С₁, C₂,..., Cj является завершенным, т.к. в С₁, C₂,..., d,..., Cj,..., d,..., С не применялись правила V_в, З_и.

Вывод С₁, C₂,..., C_i является завершенным, т.к. в С₁, C₂,..., d,..., Cj,..., d,..., С_t не применялись правила V_в, З_и.

По индуктивному предположению, Г₁ |= Cj, где Г₁ (Г₁ е Г) - множество неисключенных посылок из С1, C2,., Cj и Г - множество неисключенных посылок из С1, C2,..., d,..., Cj,..., d,..., Сt. Значит, Г1 |= D. Отсюда Г1, Сh |= D.

По индуктивному предположению, Г₂ |= C_i, где Г₂ (Г₂ е Г) - множество неисключенных посылок из С1, C2,., Ci и Г - множество неисключенных посылок из С1, C2,..., d,..., Cj,..., d,..., Сt. Значит, Г2 |= Отсюда Г2, Сh |= -D.

Учитывая Г₁, С_h |= D и Г₂, С_h |= -D, получаем Г₁, Г₂ |= -С_h. Отсюда, используя Г₁ е Г и Г₂ е Г, получаем Г |= С_t.

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

Тогда вывод имеет следующий вид: С₁, C₂,..., C_h,..., Cj,..., С_t, где t > 2, t > h, t > j, С есть C_h з Cj, где C_h есть последняя неисключенная посылка в выводе.

Вывод С₁, C₂,..., Cj является завершенным, т.к. в выводе С₁, C₂,..., Cj,..., С_t не применялись правила V_в, З_и.

По индуктивному предположению, Г₁ |= Cj, где Г₁ (Г₁ е Г) - множество неисключенных посылок из С1, C2,., Cj и Г - множество неисключенных посылок из С₁, C₂,..., Cj,..., С_t. Значит, Г₁ |= Сj. Отсюда Г₁, C_h |= Сj.

Из Г₁, C_h |= Сj получаем Г₁ |= C_h з Cj. Отсюда, используя Г₁ е Г, получаем Г |=

Ch з Cj.

Таким образом, имеет место Vm(m < n з VrЛ(m, r)) з Л(п+1, 0). (С) лемма верна для всех завершенных выводов, ранг которых равен r+1 и число применений правил вывода в которых равно n, в предположении, что лемма

верна для всех завершенных выводов, ранг которых меньше или равен r и число применений правил вывода в которых равно n.

Т.е. докажем VrJI(n, r+1) в предположении, что Vri(ri < r з Л(п, ri)).

Пусть имеется завершенный вывод Д с п+1 количеством абсолютно ограниченных переменных и {а₁, а₂, ..., а_п+1) - множество (п > 1) абсолютно ограниченных переменных в этом выводе.

По лемме 2.2.2, среди {а₁, а₂, ..., а_п+₁} найдется пассивная переменная а;, 1 < i < п+1. Если в Д несколько пассивных переменных, то мы выбираем первую (сверху вниз) из них.

Тогда (С) разбивается на 2 случая:

С1. Пассивная переменная а_; абсолютно ограничена по правилу Vn. С2. Пассивная переменная а_; абсолютно ограничена по правилу З_и.

Тогда вывод Д может принять один из двух видов:
Г Г

h. С(а_;) или h. ЭРС(Р)

k. VpC(P) - V_в: h; а_; - абс. огр. k. С(а_;) - Э_и: h; а_; - абс. огр.

В В

Построим следующий вывод Д*, который будет отличаться от предыдущего только наличием посылки 0 вида К з М, где К - формула, находящаяся на шаге h в выводе Д, и М - формула, находящаяся на шаге k в выводе Д.

Тогда вывод Д* может принять один из двух видов:
0. С(а_;) з VPC(P) - пос. 0. ЭрС(Р) з С(а_;) - пос.

Г Г

h. С(а_;) или h. ЭРС(Р)

k. VPC(P) - зи: 0, h k. С(а;) - Зи: 0, h

В В

Глава 3. Алгоритм поиска вывода в системе BMV

§ 3.1. Изменение формулировки системы BMV

В целях эффективности автоматического поиска вывода добавим к BMV-

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

__________ —ЭаЛ(а) -(А v В) -(А v В)

Vа—Л(а) -А -В

Несложно показать, что данные правила производны: их добавление не влияет

на множество теорем исчисления.

Теперь объясним необходимость введения именно таких правил.

Отсутствие этих правил приводит к следующим затруднениям [Болотов и др.].

Пусть (ситуация «а») в алгоритме необходимо доказать формулу А v В, но в выводе нет ни А, ни В.

Тогда (ситуация «б») в качестве последней посылки в последовательность вывода помещается —(А v В) и теперь необходимо получить не формулу А v В, а противоречие в выводе. Допустим, что противоречие не получено (и вывод, следовательно, не построен).

Значит, (ситуация «в») алгоритм использует формулу —(А v В) в качестве источника для взятия целей и теперь необходимо получить А v В снова, т.е. алгоритм возвращается к ситуации «а».

Значит, в работе алгоритма имеет место цикл.

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

В противном случае от ситуации «б» алгоритм переходит не к ситуации «в», а к ситуации «в1»: происходит «выход из алгоритма» и обосновывается выводимость формул —А, —В из —(А v В).

Т.к. алгоритм всегда построит вывод формул —А, —В из формулы —(А v В), отмечается, что формула —(А v В) не может быть источником для взятия целей и не возникнет необходимости получать А v В. Т. е. от ситуации «в1» алгоритм не перейдет к ситуации «а».

Таким образом, цикл в работе алгоритма ликвидирован. Нетрудно видеть, что выводимость формул —А, —В из —(А v В) в ситуации «в₁» есть ничто иное, как вводимое сейчас в системы правило —v^

Что касается правила —З_и, то объяснение необходимости данного правила сходно с объяснением необходимости правила —v^ учитывая аналогию между v и 3.

Еще раз обращаем внимание, что может быть построен алгоритм поиска вывода в BMV без правил —v^ —З_и [Болотов и др.], [Болотов и др.1].

Однако введение этих правил облегчает поиск вывода. Другими словами, вместо того чтобы переходить от ситуации «а» к ситуациям «в» или «в₁», если в выводе имеется формула —(А v В) или —ЗаА(а), мы предлагаем применять к этим формулам, соответственно, правило —v_и или —З_и.

Теперь рассмотрим правила V,, и З_и, т.е. те правила системы, которые приводят к появлению в выводе абсолютных переменных.

A(a/p, уь..., y_n) p - абс.; 3aA(a, у_ь..., y_n) p - абс.;

VaA(a, у_ь..., yn) ^уъ^.••^, ^yn ^- ^огр. A(a/p, у_ь..., yn) ТЬ"- ^yn ^- ^огр.

В формулировке V,, и З_и переменные уь..., y_n суть все свободные переменные, соответственно, из VaA(a, уь..., y_n) и 3aA(a, уь..., y_n). Отметим, что p не может принадлежать (уь..., y_n}, т.к., согласно определению BMV-вывода, ни одна переменная не может ограничивать сама себя (Определение 2.1.3).

Покажем, что система BMV неявно использует сколемовские функции в правилах Vn, З_и. (Явно сколемовские термы используются при формулировке правила З_и в системе натурального вывода, предложенной Е.К. Войшвилло [Войшвилло], т.е. в той системе, модификацией которой является BMV.)

Приведем вариант записи данных правил с использованием сколемовских функций а, а₁ и т.д. [Мендельсон, с. 111]: V,,: из А(а/о(уь..., y_n)) выводима VaА; З_и: из ЗаА выводима А(а/а(уь..., y_n)), где а - новая сколемовская функция, уь..., y_n - все свободные переменные в ЗаА и в VaА. При этом нульместные сколемовские функции обозначаются константами a, b и т.д.

Например, результатом сколемизации формулы 3_vV_w3_xV_y3_z(Q(v, w, y, z) з P(f(x, У), g(z))) будет Q(a, w, y, d(w, y)) з P(f(a(w), y), g(d(w, y))).

Теперь сравним запись с неявным использованием сколемовских термов и запись с использованием таких термов.

сколемовский вариант	вариант BMV
А(а/а(у_ь..., у_п)), где а - новая функция,	Л(а/р, уь..., у_п), где р - абс., уь..., у_п - отн.,
если n > 0;	если п > 0;
Л(а/а), где а - новая константа, если n = 0	Л(а/р), где р - абс., если n = 0

В обоих вариантах множество {уь..., у_п} совпадает. Подстановка везде

правильна.

Различия заключаются в следующем: (1) вариант BMV не использует функторы для образования сколемовского терма; (2) в случае п = 0 сколемовский вариант использует константы, а вариант BMV - абсолютные переменные. Более того, сколемовский вариант требует, чтобы константы и функторы были новыми, а вариант BMV не требует, чтобы абсолютные переменные были новыми.

Данные различия исчезают, если отметить содержательную трактовку (полностью верную для правила З_и и частично верную для правила Vn) абсолютной переменной как константы, обозначающей некий объект, для которого выполняется А в записи Л(а/р, уь..., у_п) или Л(а/р): «Переменная р в этом случае ... абсолютно ограничена в том смысле, что должна теперь рассматриваться как имя какого-то вполне определенного объекта, удовлетворяющего условию А» [Бочаров и Маркин, с. 133].

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

Что же касается первого различия в записях Л(а/р, уь..., у_п) и А(а/а(уь..., у_п)), то содержательно они обозначают одно и тоже: выбор значения для объекта, обозначенного в одном случае как «р - абс., уь..., у_п - отн.», а в другом - как «а(уь-.., у_п)», ограничивает значения для остальных свободных переменных уь -.•, у_п.

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

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

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

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

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

Проиллюстрируем необходимость запрета на самоограничение переменной примерами из [Бочаров и Маркин, с. 135]: именно данный запрет, а не требование правильной подстановки не позволяет вывести в системе из A(y, y) формулу VxA(x, y) и из 3xB(x, y) формулу B(y, y). Отмечается, что «при таком переходе переменная y ограничивает сама себя».

Далее авторы пишут: «Надо только учитывать, что ситуация, когда переменная ограничивает сама себя, может возникнуть не только прямым образом, как это было в приведенных примерах, но и косвенно. Здесь имеется в виду то обстоятельство, что отношение «x ограничивает y» является транзитивным, то есть для него верно соотношение: «если a ограничивает p, а p ограничивает у, то a ограничивает у». В силу этого в системе не проходит доказательство формулы Vx3yP(x, y) з 3yVxP(x, y).

Пусть запись p < у означает, что переменная p абсолютно ограничена и переменная у ограничена относительно переменной p. Т.е. при применении правила V,, или З_и по переменной p была относительно ограничена переменная у, входящая свободно в формулу VaA(a) или 3aA(a).

Свойства отношения ограничения на множестве переменных задаются двумя аксиомами:

Va—(a < a) - иррефлексивность: ни одна переменная не ограничивает сама

себя;

VаVрVy(((а < Р) & (Р < у)) з (а < у)) - транзитивность: если а ограничивает р и Р ограничивает у, то а ограничивает у.

Таким образом, отношение ограничения есть отношение строгого (частичного)

порядка.

Заметим, что теория строгого порядка разрешима.

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

§ 3.2. Унификация

Введем основные определения, следуя [Чень и Ли].

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

Определение 3.2.1. Подстановка - это конечное множество вида {а₁/1₁, апЛп}, где

1. каждая а; - неабсолютная переменная,

2. каждый t_; - терм, отличный от а_;,

3. все а_; различны.

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

Свойство 2 исключает подстановку неабсолютной переменной вместо ее

самой.

Свойство 3 исключает различные варианты подстановки для одной и той же неабсолютной переменной.

Пусть 9 = {а^, а_пЛ_п} - подстановка и А - формула. Тогда А9 - формула, полученная из А заменой одновременно всех вхождений а_; (1 < i < п) в А на t_;.

Пусть 9 = (a₁/t₁, a_n/t_n} и X = (p₁/t*₁, p_m/t*_m} - две подстановки. Тогда композиция 9 и X есть подстановка (9°X), которая получается из множества (a₁/t₁X, a_n/t_nX, p₁/t*₁, ..., p_m/t*_m} вычеркиванием (1) всех элементов aj/tjX, для которых tjX = aj, и (2) всех элементов p_;/t*i таких, что p_; g (a₁, ..., a_n}.

Свойство (1) отбрасывает подстановки неабсолютной переменной вместо самой себя.

Свойство (2) запрещает различные варианты подстановок вместо одной и той же неабсолютной переменной.

Композиция подстановок ассоциативна. Пустая подстановка s есть одновременно и левое и правое тождество, т.е. (9°Х)°ц = 9°(X°u) и s°9 = 9°s для всех 9,

X, ц.

Подстановка 9 накрывает подстановку 9₁ (обозначается 9 > 9₁), если существует подстановка 9₂: 9₁ = 9°9₂. Если 9 > 9₁ и 9₁ > 9, то 9 = 9₁.

Определение 3.2.2. Подстановка 9 называется унификатором для множества формул (A₁9, A_k9} т.т.т., когда A₁9 = A₂9 = ... = A_k9. Множество формул (A₁, A_k} унифицируемо, если для этого множества существует унификатор.

Например, подстановка 9 = (x/y, z/v}, где x, z - неабсолютные переменные, y, v - абсолютные переменные, в формулы A(x, v) и A(y, z) приводит к тому, что A(x, v)9 = A(y, v) = A(y, z)9. Значит, множество формул (A(x, v) и A(y, z)} унифицируемо.

Определение 3.2.3. Унификатор а для множества формул (A₁, A_k} будет наиболее общим унификатором т. т. т., когда для каждого унификатора 9 для этого множества существует такая подстановка X, что 9 = а°Х.

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

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

Например, алгоритм не будет стараться унифицировать формулы P(x, y) и Q(x, y), поскольку данные формулы различаются между собою входящими предикаторами.

Для целей нашего исследования можно ограничиться унификацией только пар

формул.

Множество рассогласований D для непустого множества подобных формул {А₁, A₂} получается выявлением первой (слева) позиции, на которой символы, входящие в формулы А₁ и A₂, не совпадают, и затем выписыванием из формул А₁ и A₂ каждого терма, занимающего эту позицию. Множество этих термов есть множество рассогласований в { А1, A2}.

Например, для формул А₁ = P(x, v) и A₂ = P(y, z), где x, z - неабсолютные переменные, y, v - абсолютные переменные, множество рассогласований D есть {x, y}.

Поскольку x - неабсолютная переменная и y - абсолютная переменная, то возможна подстановка 91 = {x/y}, которая устраняет множество рассогласований D1 (индекс 1 обозначает по-порядку номер позиции, на которой возникло данное множество рассогласований).

Однако 9₁ не является унификатором для {P(x, v), P(y, z)}, поскольку P(x, v)9 = P(y, v) * P(y, z)9.

Формулы P(y, v) и P(y, z) не совпадают на второй позиции, образуя множество рассогласований D2 = {v, z}. Поскольку z - неабсолютная переменная и v - абсолютная переменная, то возможна подстановка 92 = {z/v}, которая устраняет множество рассогласований D2.

Таким образом, унификатором для формул P(x, v) и P(y, z) является композиция подстановок 9₁°9₂ = {x/y, z/v}.

В процессе унификации возможно появление унификатора (подстановки, унифицирующей две формулы), который является композицией подстановок. Значит, первоначальные формулы, унификация которых является исходной задачей, в процессе поиска унификатора изменяются с помощью новых подстановок. В предыдущем примере из формулы P(x, v) при помощи подстановки {x/y} получили формулу P(y, v), а из формулы P(y, z) при помощи подстановки {z/v} получили формулу P(y, v).

Другими словами, если мы обозначим исходную формулу P(x, v) как А₀ и исходную формулу P(y, z) как В₀, то А₁ есть P(y, v) и В₁ = В₀ = P(y, z). Далее А₂ = А₁ = P(y, v) и В₂ есть P(y, v). Таким образом, А₂ = В₂, т.е. P(x, v) и P(y, z) унифицируемы.

При этом подстановка {x/y, z/v} - унификатор для формул P(x, v) и P(y, z) -является композицией подстановок {x/y} и {z/v}.

Поскольку {A, A} = {A}, мы будем называть множество вида {A, A} одноэлементным.

Алгоритм унификации двух подобных формул А и В. Символами /... / обозначены комментарии Шаг 1. k = 0, А_к = А, В_к = В, a_k = s (пустая подстановка). /Алгоритм берет исходные две формулы А и В, для которых необходимо найти унификатор. Исходным унификатором при этом является пустая подстановка s./

Шаг 2. Если ни одна переменная в выводе не ограничивает сама себя, то перейти к шагу 3.

Иначе стоп: A_k и В_к не унифицируемы. Выход из алгоритма. /Попытка унифицировать формулы A_k и В_к приводит к появлению в выводе переменной, которая ограничивает сама себя./

Шаг 3. Если {A_k, В_к} - одноэлементное множество, то стоп: а_к - наиболее общий унификатор для A_k и /Устранив k множеств рассогласований между формулами A₀ и В₀ и получив из формулы A₀(B₀) формулу А^Б^), алгоритм добился, что A_k = B_k. Значит, последняя подстановка является наиболее общим унификатором для формул A0 и В0./

Иначе найдем множество рассогласований D_k для формул A_k и

Шаг 4. Если существуют такие элементы и t_k в D_k, что - неабсолютная переменная, которая не входит в t_k, то перейти к шагу 5. /Подстановка, во-первых, осуществляется только вместо неабсолютной переменной и другие термы, а также предикаты и логические связки не подлежат замене. Во-вторых, осуществляя подстановку терма вместо неабсолютной переменной, необходимо следить, чтобы заменяемая переменная не входила в этот терм./

Иначе стоп: формулы A_k и В]₁ не унифицируемы. Выход из алгоритма.

Шаг 5. Пусть a_k+1 = {а^}, A_k+1 = Aii^ii/tii} и = В^а^}. /Осуществляем подстановку a_k+₁ в формулу A^^) и получаем формулу A+^^k)./

Заметим, что A_k+₁ = Aa_k+₁ и B_k+₁ = Ba_k+₁. /Это означает, что формула A^^^) может быть получена из формулы Af^o) с помощью подстановки a_k+₁ = ((a₁°a₂)°a₃)^°a_k)), т.е. с помощью композиции k подстановок./

Шаг 6. Присвоить значение k+1 и перейти к шагу 2. Теорема 3.2.4. Вышеприведенный алгоритм конечен и всегда находит наиболее общий унификатор для унифицируемого множества A.

Доказательство: наш алгоритм унификации отличается от оригинального алгоритма унификации, предложенного в [Чень и Ли], наличием шага 2, т.е. проверкой наличия переменной, которая ограничивает сама себя.

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

С другой стороны, данная проверка сужает множество подстановок, допустимых согласно алгоритму унификации в [Чень и Ли].

Поскольку алгоритм унификации в [Чень и Ли] конечен и всегда находит наиболее общий унификатор, наш алгоритм унификации также конечен и всегда находит наиболее общий унификатор.

Доказано.

Поясним данный алгоритм на примерах.

Рассмотрим несложный пример, когда необходимо унифицировать формулы P(x) и P(y), где х - неабсолютная переменная и y - абсолютная переменная.

Пусть А есть Р(х) и В есть Р(у). Помещаем эти формулы в алгоритм. Тогда А₀= Р(х) и В₀ есть Р(у), k = 0, a_k = s (пустая подстановка) (шаг 1).

Допустим, что в вывод не входит переменная, которая ограничивает сама себя

(шаг 2).

Тогда найдем область рассогласований D₀ = (x, y} для формул А₀ и В₀ (шаг 3).

Поскольку неабсолютная переменная х не входит в у, переходим к осуществлению подстановки (шаг 4).

Осуществляем подстановку а1 = ( х/у} в формулы А0, B0 и получаем формулы А₁, B₁. Отметим, что А₁ = А₀а₁ и B₁ = B₀a₁ (шаг 5).

Присвоить параметру k значение 1 и вернуться на шаг 2.

Допустим, что в вывод не входит переменная, которая ограничивает сама себя

(шаг 2).

А1 = P(y) и В1 = P(y). Значит, (A1, B1} одноэлементное множество. Стоп: а1 = ( х/у} - наиболее общий унификатор для Р(х) и Р(у) (шаг 2).

Если в вышеприведенном примере переменная x, как и переменная y, является абсолютной, то формулы не унифицируемы, т.к. подстановка 9 = {x/y} невозможна, поскольку в формулах, согласно определению подстановки, замене подлежат только неабсолютные переменные. В таком случае алгоритм унификации остановится и выдаст ответ, что данное множество формул не унифицируемо.

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

Пусть требуется унифицировать формулы P(x₁, y₁), P(y₂, x₂), где y₁ < x₁ и y₂ < x2 и х1, х2 суть неабсолютные переменные. Напомним, что yi < xi означает, что переменная yi абсолютна ограничена и xi относительно ограничена.

Пусть А есть P(x1, y1) и В есть P(y2, x2). Помещаем эти формулы в алгоритм. Тогда А₀ = P(x₁, y₁) и В₀ есть P(y₂, x₂), k = 0, a_k = s (пустая подстановка) (шаг 1).

Поскольку в y1 < x1 и y2 < x2 ни одна переменная не ограничивает сама себя (шаг 2), то

найдем область рассогласований D0 = {x1, y2} для формул А0 и В0 (шаг 3).

Поскольку неабсолютная переменная х1 не входит в у2, переходим к осуществлению подстановки (шаг 4).

Осуществляем подстановку а₁ = {х₁/у₂} в формулы А₀, B₀ и получаем формулы А₁ = Р(у₂, y₁) и B₁ = P(y₂, x₂). Отметим, что А₁ = А₀а₁ и B₁ = B₀a₁ (шаг 5).

Присвоить параметру k значение 1 и вернуться на шаг 2.

Поскольку в y1 < у2 и y2 < x2 ни одна переменная не ограничивает сама себя (шаг 2), то

найдем область рассогласований D1 = { у1, х2} для формул А1 и В1 (шаг 3).

Поскольку неабсолютная переменная х2 не входит в у1, переходим к осуществлению подстановки (шаг 4).

Осуществляем подстановку а₂ = {х₂/у₁} в формулы А₁, B₁ и получаем формулы А2 = P^2, y1) и B2 = P(y2, у2). Отметим, что А2 = А1О2 и B2 = B1C72 (шаг 5).

Присвоить параметру k значение 2 и вернуться на шаг 2.

В y1 < у2 и y2 < у1 переменная у1(у2) ограничивает сама себя по транзитивности (шаг 2). Значит, подстановку а₂ = {х₂/у₁} в формулы А₁, B₁ делать нельзя.

Из этого следует, что формулы P(x1, y1), P(y2, x2), где y1 < x1 и y2 < x2 и х1, х2 суть неабсолютные переменные, неунифицируемы.

В заключении отметим, что алгоритм унификации можно задать таким образом, чтобы он унифицировал формулы, отличающиеся между собой только вырожденными вхождениями кванторов, например, VxP(x) и VyVxP(x). Такой алгоритм предполагает упорядоченное переименование всех связанных переменных [Sieg & Byrnes].

Унификация класса формул, отличающихся вхождениями различных связанных переменных (например, VxP(x) и VyP(y)), требует введения в исчисление BMV правила правильной подстановки. Этого мы не будем делать. См. такой алгоритм унификации в [Sieg & Byrnes], [Li].

§ 3.3. Правила поиска вывода в системе BMV

Основная идея нижеследующего алгоритма - построение двух непустых

последовательностей. Интуитивно говоря, поиск вывода осуществляется в двух

(синтетическом и аналитическом) направлениях.⁴ С одной стороны, мы стараемся

получить необходимую формулу из уже имеющихся в выводе формул.⁵ С другой

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

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

успешно решить саму задачу.⁶

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

Особо отметим, что в данном контексте «правило» не понимается как преобразование формул в рамках некоторого исчисления (в таком смысле «правило» понимается в Главе 2 нашей работы, где речь идет о формулировке правил системы

BMV).

В англоязычной литературе синтетическое направление называется forward reasoning, а аналитическое направление - backward reasoning, соответственно.

⁵ «Задачу устранения «дырки» в строящемся выводе можно решать, как говорят, «в лоб», не сводя ее к подзадачам, а просто заполняя пробел, вставляя сверху от знака |- по определенным правилам новые и новые формулы, пока в конце концов не получится искомое заключение. Такой метод поиска вывода можно назвать синтетическим» [Смирнов и др., с. 40].

⁶ Однако в процессе поиска вывода наряду с синтетическими могут осуществляться и аналитические шаги. В этом случае мы сводим задачу по поиску данного вывода к одной или нескольким подзадачам по поиску вспомогательных выводов [Смирнов и др., с. 42].

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

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

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

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

Остановимся более подробно на последовательности целей.

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

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

Если текущей целью является противоречие, то текущая цель достижима (достигнута), если в выводе содержатся две неисключенные формулы вида A и —В,

В противном случае, множество аналитических и синтетических правил, заданных в смысле Главы 2 нашей работы, в совокупности с некоторым понятием вывода образовывало бы некоторое промежуточное исчисление, позволяющее искать вывод в системе BMV. См. данный подход в [Sieg], [Sieg & Byrnes].

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

В противном случае цель считается недостижимой (недостигнутой).

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

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

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

Например, необходимо достигнуть цель А & В. Мы можем достигнуть А & В с помощью BMV-правил из имеющихся в выводе посылок. Однако поиск вывода существенно облегчается, если применить к текущей цели А & В некоторое аналитическое правило и получить подцели А и В, из которых А становится текущей целью, а В - предыдущей целью по отношению к А (и подцелью по отношению к А & В) в ПЦ. Если подцели А и В достижимы (а значит, А и В находятся в ПВ), то, применяя &_в, можно достигнуть цель А & В.

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

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

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

В правиле —_ц формула А может быть либо элементарной формулой P(a), либо —C, либо C v D, либо 3aC.

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

Правило Vu позволяет от цели VaA(a, уь - • •, Y_n) перейти к подцели A(a/p, уь - • •, y_n), где Р - абсолютно ограниченная переменная и уь---, Y_n относительно ограничены. Если подцель A(a/p, уь---, Y_n) достигнута (т.е. в ПВ имеется формула В: В и A(a/p, уь-.., y_n) унифицируемы с помощью подстановки Q), то к ВО можно применить правило V,, по переменной Р, вывести формулу VaA(a, уь---, у_п)О и достигнуть цель VaA(a, yi, — , Yn)0.

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

Степенью формулы А, обозначается g(A), является количество вхождений логических символов в формулу А: g(P(a)) = 0, где P(a) обозначает элементарную формулу; g(—A) = g(VaA(a)) = g(3aA(a)) = g(A) + 1; g(A & B) = g (A v B) = g(A з B) = g(A) + g (B) + 1.

правила не работают с целью противоречие. Значит, сформулируем простое свойство ц-правил: процесс сведения произвольной цели из ПЦ с помощью ц-правил к цели противоречие конечен. Содержательно это означает, что процесс сведения некоторой цели к цели противоречие с помощью ц-правил конечен.

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

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

На первый взгляд, необходимость данного правила поиска вывода неясна: каким образом достижение (причем, А не всегда достижима) цели А связано с достижением цели противоречие?

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

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

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

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

Задаются следующие вц-правила с использованием метки М7 (ее смысл

приводится ниже, в описании алгоритма).

__________ А у В^М7 е ПВ_____________ А з В^М7 е ПВ___________

v_B„ —А^М7 е ПЦ ^Звц А^М7 е ПЦ

___________ УаА е ПВ______________ —А^М7 е ПВ___________

^Увц А(аЛ)^М7 е ПВ ^—вц А^М7 е ПЦ

В правиле —_вц формула А не имеет вида элементарной формулы P(a), или C у D, или 3aC.

В правиле У_вц терм t не может быть неабсолютной переменной. Более того, мы подставляем только такой терм t, что неисключенная формула А(аЛ) не находится выше в ПВ.⁹

Отметим, что правило У_вц отлично от правила У_и. Правило У_вц разрешает снимать квантор общности по некоторым определенным термам из ПВ. Таким образом, применение правила У_вц представляет собой конечное число применений правила У_и.

ВЦ-правилам соответствуют аналитические правила удаления в [Смирнов и

др.], [Смирнов-мл.] и [Смирнов-мл.1]. Сравнительный анализ данных групп правил

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

правило поиска вывода v_ae в [Смирнов-мл., с. 99] запишется следующим образом:

_____________ А у В е ПВ, C е ПЦ__________________

v_ae А - пос. е ПВ, C е ПЦ

В - пос. е ПВ, C е ПЦ

Если мы хотим достичь текущей цели C из формулы А v В, то мы помещаем А в ПВ в качестве посылки и в качестве текущей цели берем формулу С. Если С достижима, то формула В помещается в ПВ в качестве посылки и текущей целью становится формула С. Если и в этом случае С достижима, то в ПВ применяется правило разбора случаев.

В системе BMV нет правила разбора случаев. Поэтому предлагаемый алгоритм в такой ситуации берет в качестве текущей цели —А. Если она достижима, то к формулам А v В, —А из ПВ применяется правило у_и и в ПВ помещается формула В.

Таким образом предотвращаются избыточные применения правила У_и в ПВ.

Отметим, что формульным коррелятом правила v_ae является отношение между формулами (А v В) з С и (A з C) & (В з С). Данное отношение является отношением логического следования в обе стороны, т. е. эти формулы эквивалентны в классической пропозициональной логике. Таким образом, правило v_ae представляет собой эквивалентный переход.

В свою очередь, формульным коррелятом правила является отношение между формулами (А v В) з С и (—А з В) з С, которое также является отношением логического следования в обе стороны, т.е. эти формулы эквивалентны. Таким образом, правило v^, представляет собой иной эквивалентный переход.

Аналогичные замечания относятся к аналитическому правилу поиска вывода 3_ae в [Смирнов-мл., с. 99], которое в нашей нотации запишется следующим образом:

______________ А з В е ПВ, C е ПЦ___________________

з_ае —С - пос. е ПВ, А е ПЦ

В е ПВ, C е ПЦ

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

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

Формульным коррелятом правила з_ае является отношение между формулами (А з В) з С и (—С з А) & (В з С). Данное отношение является отношением логического следования в обе стороны, т.е. эти формулы эквивалентны в классической пропозициональной логике. Таким образом, правило з_ае представляет собой эквивалентный переход. Однако наш алгоритм в такой ситуации вводит новую текущую цель А, т. е. он не использует эквивалентные переходы.

Итак, алгоритм осуществляет поиск вывода в двух направлениях.

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

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

§ 3.4. Описание алгоритма поиска вывода в системе BMV Алгоритм описывается следующим образом.

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

- Далее описывается механизм меток: объясняется, когда и на какие формулы и цели ставятся (снимаются) метки.

- Затем следует пошаговое описание алгоритма поиска вывода в системе BMV. Пусть ПВ и ПЦ служат сокращениями для понятий «последовательность

вывода» и «последовательность целей», соответственно, тогда к формулам из ПВ применяются следующие процедуры, которые мы делим на три группы: процедуры 1*4*, которые применяются только к формулам из ПВ; процедура 5*, которая применяется только к целям из ПЦ, и процедуры 6*-7*, которые применяются как к формулам из ПВ, так и к целям из ПЦ.

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

Задается следующий порядок применения: пропозициональные правила (в произвольном порядке) применяются в первую очередь. Среди кванторных правил первым применяется —З_и. Затем применяется З_и.

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

Пропозициональные правила v_и и з_и применяются следующим образом:

з_и. Пусть А₂ з В е ПВ и формула А₂ з В не отмечена меткой МО (смысл данной метки см. далее).¹⁰ Если среди всех неисключенных формул в ПВ найдется формула А₁: А₁9 = А₂9, где 9 - унификатор, и ни одна переменная не ограничивает сама себя, то данный унификатор применяется к А₂ з В, А₁ и из формул А₁9, А₂ з В9 по правилу зи выводима формула В9. Аналогично з_и.

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

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

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

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

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

—в. Пусть цель противоречие является текущей целью в ПЦ. Если среди неисключенных формул из ПВ найдутся формулы А и —В: А9 = В9, где 9 -унификатор, и ни одна переменная не ограничивает сама себя, то к последней неисключенной посылке С из ПВ применяется правило —в, формула —С добавляется в ПВ, все неисключенные формулы из ПВ, начиная с формулы С и заканчивая формулой, предшествующей формуле —С, исключаются из ПВ, а цель противоречие помечается как достигнутая.

З_в. Пусть формула ЗаА(а) является текущей целью в ПЦ. Если среди неисключенных формул из ПВ найдется формула А^), где t - произвольный терм, то к формуле А(1) применяется правило З_в, формула ЗаА(а) добавляется в ПВ, а цель ЗаА(а) помечается как достигнутая.

У_в. Пусть формула УаА(а) является текущей целью в ПЦ. Если среди неисключенных формул из ПВ найдется формула А(а_;), где а; не является абсолютно

Грубо говоря, к формуле А₂ з В не применялось правило з_и.

ограниченной переменной, то, если ни одна переменная не ограничивает сама себя при абсолютно ограниченной a;, к формуле А(а_;) применяется правило Vn, формула VaА(a) добавляется в ПВ, делается отметка, что a_; относительно ограничивает все остальные свободные переменные в А(а_;), а цель VaА(a) помечается как достигнутая.

Процедура 3* определяет применение вц-правил, кроме V^,.¹¹ Алгоритм ищет первую сверху вниз сложную неисключенную формулу из ПВ, которая не отмечена метками МО или М5 (смысл этих меток см. далее). Эта формула является вц-формулой. Вид вц-формулы определяет, какое именно вц-правило применимо.

Процедура 4* применяется после всех остальных процедур, если в ПВ содержатся неисключенные формулы вида VaА(a), к которым уже применялось правило V_и (т.е. они отмечены меткой М1). В таком случае метка М1 снимается со всех таких формул квантор общности снимается по некоторым определенным термам из ПВ¹²

Напомним, что в правиле терм t не может быть неабсолютной переменной. Более того, мы подставляем только такой терм t, что неисключенная формула А(аЛ) не находится выше в ПВ.

К формулам из ПЦ применяются следующая процедура:

Процедура 5* определяет применение ц-правил.

Ц-правила применяются к текущей цели следующим образом:

&_ц. Пусть формула А & В является текущей целью в ПЦ. Если она не достижима, то формула А становится текущей целью и отмечается меткой М3. Если цель А достижима, то текущей целью становится формула В. Если цель В достижима, то текущей целью вновь становится формула А & В.

Применение определяется Процедурой 4*. ¹² Отметим, что метка М1 снимается с таких формул, а значит, впоследствии к ним применимо правило V_и по новой неабсолютной переменной из ПВ.

Пусть формула А v В является текущей целью в ПЦ. Если она не достижима, то формула А становится текущей целью и отмечается меткой М4. Если цель А недостижима, то цель А удаляется из ПЦ и формула В становится текущей целью и отмечается меткой М5. Если цель В недостижима, то цель В удаляется из ПЦ, формула —(А & В) помещается в ПВ в качестве последней посылки и цель противоречие становится текущей целью.

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

—ц. Пусть формула А является текущей целью в ПЦ, где А может быть либо элементарной формулой Р(а), либо —C, либо C v D, либо ЗаС Если она не достижима, то формула —А помещается в ПВ в качестве последней посылки и цель противоречие становится текущей целью.

Зц. Пусть формула ЗаА является текущей целью в ПЦ. Если она не достижима, то формула А(а/р), где Р - новая неабсолютная переменная, становится текущей целью.

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

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

Процедура 6* осуществляет глобальную подстановку Q в ПВ и ПЦ, если Q -наиболее общий унификатор. Если в процессе поиска вывода произошло достижение некоторой цели с помощью Q и ни одна переменная не ограничивает сама себя, то алгоритм осуществляет данную подстановку Q во всех (исключенных и неисключенных) формулах и целях из ПВ и ПЦ.

Процедура 7* осуществляет с помощью алгоритма унификации проверку достижимости текущей цели.

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

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

Важную роль в работе алгоритма играет механизм меток.
•S Следующие метки ставятся на формулы из ПВ:

МО - ставится на посылку (в однопосылочных) или на большую посылку (в двухпосылочных) правила исключения после применения данного правила.

М1 - ставится на формулы вида УаА после применение к ним правила У_и.

М2 - ставится на формулы, полученные в результате применения правил исключения.

•S Следующие метки ставятся на цели из ПЦ:

М3 - ставится на левый конъюнкт А;, полученный из цели А; & Aj.

М4 - ставится на левый дизъюнкт А;, полученный из цели A; v Aj.

М5 - ставится на правый дизъюнкт Aj, полученный из цели A; v Aj.

М6 - ставится на формулу A(t), полученную из цели ЗаA(а).
•S М7 - ставится на формулы из ПВ и ПЦ при применении вц-правил.

Описание алгоритма

Символами /./ обозначены комментарии.

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

2. Применение правил исключения к формулам из ПВ.

2.1. Применяется процедура 1*. /Применяются правила исключения./ При этом на посылки правил вывода вида А & В, А v В, Аз В, ——А, —(А v В), —ЗаА, УаА и ЗаА, к которым были применены, соответственно, правила &_и, vjj, з_и, —_и, —vjj, —З_и, \/_и и З_и, ставится МО, указывающая на два обстоятельства: (а) недопустимость вторичного применения к ним указанных правил, (б) невозможность их использования в качестве вц-формул. На заключения правил вывода ставится М2. Правила З_и, У_и применяются следующим образом:

a) Квантор общности снимается по правилу V_и с формулы VaА по новой неабсолютной переменной. На формулу VaА ставится метка М1.

b) Если вхождение квантора V по переменной a в формуле А вырождено, то результатом снятия квантора V будет А.

a) Квантор З снимается по правилу З_и с формулы ЗаА по новой абсолютной переменной.

b) Рядом с так полученной формулой А(а/в) пишется "в - абс., у₁, у₂,..., y_n -огр.", где y₁, y₂,..., y_n - все свободные переменные, входящие в ЗаА.

c) Если первое вхождение квантора З по переменной а в формуле ЗаА вырождено, то результатом снятия квантора З будет А.

Переход к 10.

2.2. Если ни одно правило исключения не применимо, то переход к 3.

3. Применяется процедура 5* к текущей цели A.

• A - элементарная формула P(a). Переход к 4.

• Главный знак A------ 1. Переход к 4.

• A = A_; з Aj. Переход к 5.

• A = A_; & Aj. Переход к 6.

• A = A_; v Aj. Переход к 7.

• A = ЗаА. Переход к 8.

• A = VaА. Переход к 9.

• A есть _L Переход к 12.

4. Формула —А помещается в ПВ в качестве последней посылки. Текущей целью становится получение _ . Переход к 2. /Алгоритм начинает доказывать формулы от противного./

5. Формула A_; помещается в ПВ в качестве последней посылки. Текущей целью становится Aj. Переход к 2. /Алгоритм, доказывая импликативную формулу, берет в качестве посылки ее антецедент и пытается вывести ее консеквент./

6. Текущею целью становится формула A_;. На формулу А_; ставится метка М3. Переход к 10.

6.1. С формулы А; из ПЦ снимается метка М3. Текущей целью становиться формула Aj. Переход к 10.

7. Текущею целью становится формула A_;. На формулу А_; из ПЦ, ставится метка
М4. Переход к 10.

7.1. Удаляем цель А_;, отмеченную М4. Текущей целью становиться формула Aj. На формулу Аj ставится метка М5. Переход к 10.

7.2. Удаляем цель Аj, отмеченную М5. Текущей целью становиться _L Формула —(A_; v Aj) помещается в ПВ в качестве последней посылки. Переход к 2.

8. Текущей целью становиться формула А(а/у), где v - новая неабсолютная
переменная. На формулу А(аЛ^) ставится метка М6. Переход к 10.

8.1. Удаляем цель А(аЛ^), отмеченную М6. Текущей целью становиться _L Формула —ЗаА(а) помещается в ПВ в качестве последней посылки. Переход к 2.

9. Текущей целью становиться формула А(а/в), где в - новая абсолютная
переменная.

a) Отмечается, что «в - абс., y₁, y₂,..., y_n - огр.», где y₁, y₂,..., y_n - все свободные переменные, входящие в VaА.

b) Если первое вхождение квантора V по переменной а в формуле VaА(a) вырождено, то результатом снятия квантора V будет сама формула А.

Переход к 10.

10. Применяется процедура 7*.

10.1. Текущая цель достигнута. Применяется процедура 6* (глобальная
подстановка):

• Если текущая цель отмечена М3, то переход к 6.1. /Начинаем доказывать правый конъюнкт./

• Если текущая цель не отмечена М3, то переход к 11.

10.2. Текущая цель не достигнута:

• Если текущая цель отмечена М4, то переход к 7.1. /Начинаем доказывать правый дизъюнкт./

• Если текущая цель отмечена М5, то переход к 7.2. /Начинаем доказывать дизъюнкцию от противного./

• Если текущая цель отмечена М6, то переход к 8.1. /Начинаем доказывать цель ЗаА(а) от противного./

• Если текущая цель не отмечена М4-М6, то переход к 3. 11. Достигнута текущая цель A_n.

11.1. Если A_n - главная цель, то A_n устраняется из ПЦ. Выход из алгоритма

- вывод построен.

11.2. Если A_n не является главной целью, то
Если A_n есть то:

a) A_n устраняется из ПЦ.

b) Текущей целью становиться предыдущая цель и к формулам из ПВ применяется правило —в, результатом применения которого является формула —С, где С - последняя неисключенная посылка в ПВ.

c) Делается отметка, что все формулы, начиная с формулы C и заканчивая формулой, предшествующей —С, исключаются из дальнейших шагов вывода.

d) Если в число этих формул попадает формула с меткой М2, то с соответствующей формулы снимается метка МО. Переход к 2.

Если An не есть _ , то рассматриваем подцель An-1 из ПЦ. В зависимости от вида An-1 рассматриваются следующие случаи:

- A_n-1 = A_n v A_k или A_k v A_n, то:

a) An и An-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и в ПВ включается формула
A_n-1, которая является результатом применения правила v,, к формуле A_n (A_k).

c) На формулу A_n v A_k или A_k v A_n из ПВ ставится метка МО.

d) Если на A_n-1 стояла метка М7, то с соответствующей вц-формулы
снимается метка М7. Переход к 2.

^- ^An-1 ⁼ ^Ak ^з ^An^, ^то:

a) An и An-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и к формулам из ПВ
применяется правило зв, результатом применения которого является формула Ak з An,
где Ak - последняя неисключенная посылка в ПВ.

c) Делается отметка, что все формулы, начиная с A_k и заканчивая формулой An, исключаются из дальнейших шагов вывода.

d) Если в число этих формул попадает формула с меткой М2, то с соответствующей формулы снимается метка М0.

e) Если на цели A_n-1 стояла метка М7, то с соответствующей вц-формулы снимается метка М7. Переход к 2.

- An-1 = A_k & An, то:

a) A_n и A_n-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и в ПВ включается формула
A_n-1, которая является результатом применения правила &_в к формулам A_n и A_k.

c) На формулу Ak & An из ПВ ставится метка М0.

d) Если на цели An-1 стояла метка М7, то с соответствующей вц-формулы
снимается метка М7. Переход к 2.

- A_n-1 = VaА, то:

a) An и An-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и в ПВ включается формула
A_n-1, которая является результатом применения правила V,, к формуле А(а/в, y₁, y₂,...,

yn).

c) Делается отметка, что в абсолютно ограничена и y1, y2,... , yn относительно
ограничены.

d) На формулу VaА ставятся метки М0 и М1.

e) Если на цели An-1 стояла метка М7, то с соответствующей вц-формулы
снимается метка М7. Переход к 2.

- A_n-1 = ЗаА, то:

a) An и An-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и в ПВ включается формула
A_n-1, которая является результатом применения правила З_в к формуле А(а/в).

d) Если на цели An-1 стояла метка М7, то с соответствующей вц-формулы снимается метка М7. Переход к 2.

^- ^An-1 ⁼ ^_ ^, ^то:

a) An устраняется из ПЦ.

b) Текущей целью становится предыдущая цель An-1.

c) Если на цели An-1 стояла метка М7, то с соответствующей вц-формулы
снимается метка М7. Переход к 2.

12. Применяем процедуру 3*.

12.1. Если в ПВ имеются сложные формулы, не отмеченные метками МО
или М7, то к ним применяются следующие процедуры:

a) Если в выводе имеется формула вида A; з Aj, то в качестве текущей цели
берется A;. Формула A; з Aj и текущая цель A; помечаются меткой М7. Переход к 3.

/Имея в выводе формулу вида A; з Aj, алгоритм пытается вывести A; для того, чтобы в случае успеха применить зи./

b) Если в выводе имеется формула вида A; v Aj, то в качестве текущей цели берется —A;. Формула A; v Aj и цель —A; помечаются меткой М7. Переход к 3. /Имея в выводе формулу вида A; v Aj, алгоритм пытается вывести —A; для того, чтобы в случае успеха применить v^/

c) Если в выводе встречается формула —A;, где A; не имеет вида An v Ak, ЗаА, то в качестве текущей цели берется A;. Формула —A; и цель A; помечаются меткой М7. Переход к 3. /К формулам вида —(A_n v A_k), —ЗаА применяются, соответственно, правила исключения —v^ —З_и. К остальным формулам вида — A; алгоритм применяет вц-правила для того, чтобы получить цель противоречие./

12.2. Если все сложные формулы в ПВ отмечены МО или М7, то 13.

13. Завершение алгоритма.

13.1. Если ПВ не содержит формул, отмеченных М1, то выход из
алгоритма: ПВ содержит конечный контрпример. /Если в выводе нет формул вида
VаA(а), то ПВ содержит конечный контрпример (опровержение) для данной
выводимости./

13.2. В противном случае переход к 14.

14. Применение процедуры 4*. /Применение Vm,./

Квантор общности снимается по правилу V_H с каждой неисключенной формулы вида Vo^ из ПВ по некоторым определенным термам из ПВ. Со всех формул вида VoA снимается метка М1. Переход к 10.

Конец описания.

Приведем пример работы алгоритма. (Курсивом мы будем обозначать текущую цель.)

Пусть необходимо обосновать в алгоритме вывод формулы VxP(x) & VxQ(x) из формулы Vx(P(x) & Q(x)).

Согласно пункту 1 описания алгоритма, формула VxP(x) & VxQ(x) помещается в ПЦ в качестве главной цели, а последняя формула Vx(P(x) & Q(x)) помещается в ПВ в качестве начальной посылки. Алгоритм переходит к проверке достижимости текущей цели.

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x)) - посылка VcP(x) & VxQ(x)

Т.к. текущая цель не достижима, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Согласно пункту 3, текущей целью становится левый конъюнкт, на который ставится метка М3.

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x)) - посылка VxP(x) & VxQ(x)

VcP(x)^M3

Т. к. текущая цель не достигнута, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Согласно пункту 3, текущей целью становится формула P(x/y₁), где y₁ - это новая абсолютная переменная в ПВ и ПЦ.

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x)) - посылка VxP(x) & VxQ(x)

VxP(x)^M3

P(yi), y₁ новая абсолютная переменная Т. к. текущая цель не достигнута, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Поскольку текущая цель - это элементарная формула, то,

согласно пункту 3, формула — P(yi) помещается в ПВ в качестве последней посылки, а текущей целью становится

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x)) - посылка VxP(x) & VxQ(x)

2. —P(yi) - пос. VxP(x)^M3

P(y₁), y₁ новая абсолютная переменная 1

Т.к. текущая цель не достигнута, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Поскольку текущая цель - это 1, то, согласно пункту 2, алгоритм ищет возможность применения правил исключения в ПВ. К формуле Vx(P(x) & Q(x)) применяется правило V _и по новой неабсолютной переменной из ПВ и ПЦ, т.е. по переменной x₁. На формулу Vx(P(x) & Q(x)) ставится метка М1. На формулу P(x₁) & Q(x₁) ставится метка М0.

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x))^M1 - посылка VxP(x) & VxQ(x)

2. —P(y₁) - пос. VxP(x)^M3

3. P(x₁) & Q(x₁)^M0 - V_j: 1 P(y₁), y₁ новая абсолютная переменная

Согласно пункту 2, алгоритм делает все возможные заключения по правилам исключения и применяет правило &_и.

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x))^M1 - посылка VxP(x) & VxQ(x)

2. —P(y1) - пос. VxP(x)^M3

3. P(x₁) & Q(x₁)^M0 - V_j: 1 P(y₁), y₁ новая абсолютная переменная

4. P(x1)^M2- &и: 3 1

5. Q(x1)^M2- &и: 3

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

—P(yi) и P(xi), для которых существует унификатор {xi/yi}), то, согласно пункту 10.1, применяется глобальная подстановка {x₁/y₁} в ПВ и ПЦ. Цель _1_ помечается как достигнутая и устраняется из ПЦ, а текущей целью становится P(y₁). В ПВ применяется правило —_в к формулам 2, 4 и из ПВ исключаются формулы 2-5. Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x))^M1 - посылка VxP(x) & VxQ(x)

Г2. —P(y1) - пос. VxP(x)^M3

I 3. P(y₁) & Q(y₁)^M0 - V_и: 1 P(yi), y₁ новая абсолютная переменная
I 4. P(y1)^M2- &и: 3
L5. Q(y1)^M2- &и: 3
6. P(y1) - —в: 2, 4

После применения —_и к формуле 6 вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x))^M1 - посылка VxP(x) & VxQ(x)

Г2. —P(y1) - пос. VxP(x)^M3

I 3. P(y₁) & Q(y₁)^M0 - Vj,: 1 P(y₁), y₁ новая абсолютная переменная

I 4. P(y1)^M2- &и: 3 L5. Q(y1)^M2- &и: 3

6. P(y1)^M0 - —в: 2, 4

7. P(y1)^M2- —и: 6

Поскольку текущая цель достигнута, то, согласно пункту 10.1, цель P(y1) помечается как достигнутая и устраняется из ПЦ, а текущей целью становится VxP(x). Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x))^M1 - посылка VxP(x) & VxQ(x)

Г2. —P(y₁) - пос. VxP(x)^M3

I 3. P(y1) & Q(y1)^M0 - 1 I 4. P(y1)^M2- &и: 3

L5. Q(y1)^M2- &и: 3

6. P(yi)^M0 - -в: 2, 4

7. P(yi)^M2- -и: 6

Поскольку текущая цель является подцелью достигнутой цели, то она также является достигнутой, согласно пункту 11.2. К формуле P(y₁) из ПВ применяется правило V„, в ПВ помещается формула VxP(x), цель VxP(x) помечается как достигнутая и устраняется из ПЦ, метка М3 снимается, а текущей целью становится VxP(x) & VxQ(x).

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x))^M1 - посылка VxP(x) & VxQ(x)

Г2. -.P(yO - пос.

|3. P(y1) & Q(y1)^M0 - 1

I 4. P(y1)^M2- &и: 3

L5. Q(y1)^M2- &и: 3

6. --P(y1)^M0 - -в: 2, 4

7. P(y1)^M2- -и: 6

8. VxP(x) - V,,: 4; y₁ - абс. огр.

Поскольку текущая цель является подцелью достигнутой цели, отмеченной меткой М3, то текущей целью становится VxQ(x).

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x))^M1 - посылка VxP(x) & VxQ(x)

Г2. -P(y1) - пос. VxQ(x)

I 3. P(y1) & Q(y1)^M0 - 1 I 4. P(y1)^M2 - &и: 3 L5. Q(y1)^M2 - &и: 3

6. --P(y1)^M0 - -в: 2, 4

7. P(y1)^M2 - -и: 6

8. VxP(x) - Vв: 4; y1 - абс. огр.

Т. к. в ПВ нет формулы, которая унифицируется с VxQ(x), то, согласно пункту 3, текущей целью становится Q(y₂), где y₂ новая абсолютная переменная в выводе.

НГ3. p - пос. p з q

I I I [4. -q - пос. Q

I I I 5. q - -в: 2, 3 1

I I L6. q - -и: 5

I I 7. p з q - Зв: 6

I L8. p - зи: 1, 7

I 9. p - -в: 2, 8

L10. p - -и: 9

^11. ((p з q) з p) з p - зв: 10

Комментарий. Помещаем исходную формулу в качестве главной цели в последовательность целей (ПЦ). При этом последовательность вывода (ПВ) пуста. Применяя к главной цели ц-правило з_ц, получаем подцель p и добавляем в ПВ формулу (p з q) з p в качестве последней посылки. Поскольку ни одно правило исключения в ПВ неприменимо, продолжаем работать с текущей целью p. Применяем к ней правило -_ц, получаем новую подцель 1 (противоречие) и добавляем в ПВ формулу -p в качестве последней посылки. Поскольку ни одно правило исключения в ПВ

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

неприменимо, алгоритм осуществляет поиск формул из ПВ, к которым можно применить вц-правила. Т.е. алгоритм ищет сложные формулы из ПВ, к которым не применялись правила исключения. В данном случае имеется одна такая формула (p з q) з p. Таким образом, мы применяем к ней вц-правило з_вц и начинаем строить новый блок №2. При этом формулы (p з q) з p и —p из ПВ, а также цели ((p з q) з p) з p, p и _1_ из ПЦ образуют блок №1.

Итак, по вц-правилу з_вц, примененному к формуле (p з q) з p, мы получаем первую цель блока №2 - формулу (p з q). Применяя ц-правило зц к ней, получаем подцель q и добавляем в ПВ формулу p в качестве последней посылки. Т. к. текущая цель - формула q - недостижима, применяем к ней ц-правило —ц, получаем подцель _ и добавляем в ПВ формулу —q в качестве последней посылки. Далее действуем согласно правилам системы BMV и целям алгоритма. При этом формулы 3-11, а также цели p з q, q и _ , находящиеся ниже вертикальной черты, образуют блок №2.

§ 4.2. Свойства алгоритма

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

Леммой 4.2.1. В произвольном алго-выводе каждый блок конечен.

Доказательство: полная индукция по порядковому номеру блока в алго-

выводе формулы А.

Базис: n = 1.

Первой целью блока а₁ является А - главная цель алго-вывода.

Последовательность целей в а₁ конечна (свойство ц-правил). Конечная последовательность целей в а1 порождает конечное множество посылок в последовательности вывода. Количество применений правила Vj, в одном блоке конечно. Значит, количество применений правил исключения среди конечного множества посылок вывода конечно (свойство BMV-правил).

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

Если же ни одна из целей не достигнута, то, в силу конечности последовательности вывода и последовательности целей в а1, конечен и сам а1, завершаясь целью _ .

Индуктивное предположение: допустим, лемма верна для i < n.

Индуктивный шаг: покажем, что лемма верна для i = n.

Пусть Х_п-1 обозначает множество неисключённых формул в алго-выводе для формулы А, где an-1 - последний блок с последней целью противоречие. По индуктивному предположению, a₁,^, a_n-1 суть конечные блоки, а значит, Х_п-1 конечно.

Рассмотрим 2 случая в зависимости от вц-правила, по которому был получен блок a_n: 1) блок a_n получен по вц-правилам v^, з_вц и —_вц; 2) блок a_n получен по вц-правилу V^.

Случай 1. Пусть формула Y является первой целью в блоке a_n и формула Y получена по вц-правилам Vm,, з_вц и —_вц. Последовательность целей в a_n конечна (свойство ц-правил). Конечная последовательность целей в a_n порождает конечное множество посылок вывода. Количество применений правила V_и в одном блоке конечно. Значит, конечно количество применений правил исключения среди конечного множества посылок вывода (по индуктивному предположению, X_n-1 конечно плюс свойство правил исключения).

При этом, если хотя бы одна из подцелей блока an достигнута, то обязательно достигается первая цель Y. Тем самым a_n конечен, завершаясь выводом Y.

Если же ни одна из целей не достигнута, то, в силу конечности последовательности вывода и последовательности целей в an, конечен и сам an, завершаясь целью _L

Случай 2. Пусть формула Y является первой формулой вывода в an и формула Y получена по вц-правилу V^. Последовательность целей в a_n пуста, т.к. по вц-правилу в последовательность целей не добавляются новые цели. Значит, в последовательность вывода не вводятся новые посылки. Количество применений правил исключения в блоке a_n конечно (по индуктивному предположению, X_n-1 конечно; свойство правил исключения; количество применений правила V_и в одном блоке конечно).

Отметим, что последней целью в последовательности целей является последняя цель блока an-1, т.е. противоречие.

Пусть формула Z является последней неисключенной посылкой в последовательности вывода при применении V^, т.е. при порождении блока a_n. Если цель противоречие достижима, то в последовательности вывода происходит применение BMV-правила -_в, появляется формула -Z и все формулы, начиная с формулы Z и заканчивая формулой -Z, исключаются из последовательности вывода. Значит, из последовательности вывода исключается также формула Y, которая в последовательности вывода находится ниже, чем формула Z. Таким образом, данный блок конечен.

Если же ни одна из целей не достигнута, то, в силу конечности множества вывода и пустоты множества целей в a_n, конечен и сам a_n, завершаясь целью _L

Доказано.

Разбив алго-вывод на последовательность блоков, перейдем к анализу блоков. Определение 4.2.2. Если блок a получен в результате применения -_вц, з_вц и v^, то a является достигнутым (д-блоком), если a - последний блок алго-вывода и последняя цель в a достигнута. Если блок a получен в результате применения V^, то a является достигнутым (д-блоком), если a - последний блок алго-вывода и первая формула в a исключена.

В противном случае блок является недостигнутым. Определение 4.2.3. Блок a_n непосредственно следует за блоком a_k (k < n), если при порождении a_n последним недостигнутым блоком является a_k.

Если блок a_n получен по -_вц, то a_n сильно непосредственно следует за a_k. Если блок a_n получен по з_вц, v^, то a_n слабо непосредственно следует за a_k.

Различение слабого и сильного непосредственного следования связано с тем, что если an - д-блок и имеет место сильное непосредственное следование an за ak, то ak также является д-блоком.

Дело в том, что в этом случае достижение первой цели a_n, полученной по -_вц, означает, что в последовательности формул вывода имеются формулы А (первая цель an) и - A (посылка правила - вц), а это автоматически ведет к достижению последней цели _ в блоке ak. (Правило - вц применяется только, если последней целью в ak является _L) При этом достижение последней цели в a_k влечет достижение первой цели в ak. Значит, ak - д-блок.

Что касается V^,, то, по определению д-блока, a_n достижим, если из последовательности вывода исключена первая формула А из an. Исключение формулы А возможно только при применении -_в, з_в; причем, формула С (последняя неисключенная посылка в последовательности вывода), исключаемая в результате применения правил -_в, з_в, находится выше, чем формула А. Т.к. применение правил введения детерминируется целями, в выводе достигнута последняя цель 1 блока а_к. Значит, а_к - д-блок.

Если имеет место слабое непосредственное следование а_п за а_к и а_п станет д-блоком, то а_к может не стать д-блоком.

Зададим формальное понятие поискового дерева (П-дерева) для алго-вывода. Определение 4.2.4. Поисковым деревом является частично упорядоченное множество {а₁, а₂,...} блоков, распределенных по непересекающимся «уровням» следующим образом:

1. Нулевой уровень состоит из единственного блока а₁, называемого начальным блоком;

2. Каждый блок i+1-го уровня соединён отрезком в точности с одним блоком i-го уровня;

3. Каждый блок а i-го уровня либо не соединён ни с одним блоком i+1-го уровня, либо соединён отрезками с несколькими блоками i+1-го уровня (эти блоки

го уровня называются непосредственно следующими за блоком а);

4. Блок i-го уровня, не соединённый ни с какими блоками i+1-го уровня,
называется заключительным блоком.

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

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

Приведем некоторые П-деревья и соответствующие им алго-выводы.

Пример 1.

f №1 1

№2

В данном П-дереве блок №2 непосредственно следует из блока №1.
Такому П-дереву соответствует, например, следующий алго-вывод
(вертикальная черта обозначает границу между блоком №1 и блоком №2):
1. p v q^M7 - пос. q з r

2.q - пос. r

3. —r - пос. 1

4. p - пос. —p^M7

Пример 2.

№1

№2

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

Пример 5.

№1

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

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

Ситуация в первопорядковой логике сложнее. В силу результата А. Черча о неразрешимости классической логики предикатов, в общем случае процесс поиска вывода не может быть остановлен: мы не можем за конечное число шагов определить, доказуема ли произвольная формула или нет [Church], [Churchl].

С другой стороны, Ж. Эрбран показал, что любая общезначимая формула логики предикатов доказуема за конечное число шагов [Минц], [Li]. В такой ситуации встает проблема выбора стратегии, позволяющей за конечное число шагов вывести произвольную общезначимую формулу классической логики предикатов. Такие стратегии известны: метод резолюции, метод аналитических таблиц, секвенциальные исчисления, метод семантических таблиц и др.

Анализируя данную ситуацию, Ч. Чень и Р. Ли пишут: «Тем не менее существуют алгоритмы поиска доказательства, которые могут подтвердить, что формула общезначима, если она на самом деле общезначима. Для необщезначимых формул эти алгоритмы, вообще говоря, не заканчивают свою работу. Принимая во внимание результат Черча и Тьюринга, это лучшее, что мы можем ожидать от алгоритма поиска доказательства» [Чень и Ли, с. 52]. Обратной стороной таких техник является «уход в бесконечность» в некоторых случаях, когда формула необщезначима.

Вообще, с точки зрения прикладной логики, доказательство полноты прувера -дело «неблагодарное». Распространена точка зрения, что пруверы (в том числе для поиска натурального вывода) создаются под решение каких-то отдельных прикладных проблем.¹⁵ Поэтому проблема полноты для них не ставится.

В Главе 2 мы уже касались этого вопроса. Здесь подчеркнем, что процедура поиска вывода должна задаваться таким образом, чтобы гарантировать построение контрпримера (множества Хинтикки) даже в случае «ухода в бесконечность» [Hintikka1], [Sieg].

Определение 4.2.5. Линейно упорядоченная последовательность блоков а₁, а₂, ... называется нитью данного П-дерева, если: 1) а₁ - начальный блок и 2) Уа_п (п > 1 и а_п непосредственно следует за ап-1).

С помощью программы ANDP Д. Ли дал первое машинное доказательство проблемы остановки машины Тьюринга [Li]. Д. Пеллетье с помощью программы THINKER предложил доказательства теорем теории множеств [Pelletier]. Предложенная Д. Поллоком с целью продемонстрировать преимущества натурального вывода перед другими логическими системами программа OSCAR оказалась в 40 раз быстрее, чем программа OTTER, основанная на методе резолюции [Pollock].

Напомним, что интуитивно алго-вывод представляется как последовательность блоков, полученных по одному из вц-правил. В такой ситуации большую роль играют формулы вывода, к которым применимы вц-правила (вц-формулы). Такими формулами являются формулы вида -А, А з В, А v В, не отмеченные меткой М0, т.е. к ним не применялись правила исключения, и формулы вида VaA(a). К этим и только этим формулам применяются вц-правила.

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

Поэтому нижеследующее определение выделяет роль таких формул в процессе поиска вывода.

Определение 4.2.6. Пусть при построении П-дерева a_n является последним недостигнутым блоком и j - количество нитей, построенных ранее, следующих из блока a_n и содержащих только д-блоки. Тогда E^j_n = {G₁, G₂,..., G_s, H₁, H₂,..., H_t}, s > 0, t > 0, назовем порождающим множеством формул блока a_n нити где G₁, G₂,..., G_s, H1, H2,., Ht - все такие вц-формулы; причем, G1, G2,., Gs - формулы вида —А, А з В, A v В, к которым не применялись правила исключения, и H₁, H₂,.., H_t - формулы вида VaA(a), к которым применимо правило V^,.

Множество E^jn конечно для любых конечных j, n, т. к. все блоки П-дерева конечны (лемма 4.2.1).

В свою очередь, конечность множества E^jn позволяет эффективно определять формулу (формулы, если их несколько) наибольшей степени из E^jn.

Тогда степень множества E^J_n (обозначается «g(E^J_n)») есть степень формулы наибольшей степени из E^jn.

Используя понятие П-дерева, опишем процесс поиска алго-вывода для произвольной формулы А:

1. Строим a1.

Если a1 не является д-блоком, то 2;

Если a1 является д-блоком, то алго-вывод для формулы А построен;

Исключение: переход от A v B к —А по если B - элементарная формула. Тогда g(A v B) = g(—A).

2. Рассматриваем множество E⁰₁ = {G₁, G₂,..., G_s, H₁, H₂,.., H_t},
Если s = 0, то:

если t = 0, то А недоказуема. Выход из алгоритма: последовательность формул вывода содержит конечный контрпример.

если t ^ 0, то переход к 4. Если s ^ 0, то переход к 3.

3. По формуле G₁ из множества E⁰₁ строится новый блок a₂; переход к 5.

4. По формуле H₁ из множества E⁰₁ строится новый блок a₂; переход к 5.

5. Проверяется, является ли a2 д-блоком. Если да, то возвращаемся к a1.

Если нет, то рассматривается множество Е⁰₂ = {G'₁, G'₂,..., G'_s, H'₁, H'₂,.., H'_t}. Mножество Е⁰₂ отличается от множества E⁰₁ = {G₁, G₂,..., G_s, H₁, H₂,.., H_t} тем, что, с одной стороны, некоторые формулы, которые входили в E⁰1 и были вц-формулами, таковыми не являются, а, с другой стороны, в последовательности вывода могут появиться новые вц-формулы, которые и войдут в Е⁰2. И т.д.

Грубо говоря, мы начинаем работать с самой левой нити в П-дереве.

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

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

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

Ветвление в П-дереве образуется следующим образом. Пусть из блока №1 следует блок №2 и блок №2 является д-блоком, тогда, по определению П-дерева, мы возвращаемся (бэктрэкинг) к блоку №1. При этом порождающее множество блока №1 непусто и сам блок №1 не является д-блоком. Значит, мы строим блок №3, который также непосредственно следует за блоком №1. Таким образом, в данном П-дереве из блока №1 непосредственно следуют два блока - блок №2 и блок №3, т.е. имеет место ветвление.

Далее мы покажем, что в П-дереве имеет место только конечное ветвление, т.е. в П-дереве не существует блока, из которого непосредственно следует бесконечное количество блоков. Таким образом, алгоритм по очереди (слева направо) просматривает все нити П-дерева.

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

Леммой 4.2.7. Пусть a_n непосредственно следует за a_k, k<n, и E_n, E_k -соответственно, порождающие множества из a_n и a_k, тогда g(E_n) < g(E_k).

Доказательство: возвратная индукция по количеству n блоков, непосредственно следующих за ak.

Индуктивное предположение: допустим, лемма верна для i < n.

Индуктивный шаг: покажем, что лемма верна для i = n.

Рассмотрим E_k и E_n. E_n (возможно) отличается от E_k новыми формулами, которые добавляются в последовательность вывода либо 1) по некоторому правилу введения, либо 2) по некоторому правилу исключения.

Рассмотрим случай 1. Пусть G е E_k - формула, к которой применяется некоторое вц-правило при порождении a_n и М - первая цель (формула) в a_n. Значит, по свойству вц-правил, g(M) < g(G). По свойству ц-правил, g(M') < g(M), где M' -произвольная (не первая) подцель из a_n. Значит, g(M') < g(G).

Поскольку применение правил введения в an детерминируется целями этого блока, g(Y) < g(M), где Y - произвольная формула, полученная по правилам введения в an. Из g(Y) < g(M) и g(M) < g(G) следует g(Y) < g(G).

Рассмотрим случай 2. Если формула Y получена по некоторому правилу исключения, то g(Y) < g(X), где X - (большая) посылка этого правила и X е E_k.¹⁷

Итак, добавленные к E_k новые формулы (образующие Е_п) имеют степень меньшую, чем степень формул из E_k. С другой стороны, из E_k в Е_п перешли все формулы вида УаА(а). Отсюда, gQEi) < g(E_k).

По индуктивному предположению, лемма верна для всех порождающих множеств из предыдущих блоков. Значит, g(E_n) < g(E_k), для любых п, k.

Доказано.

§ 4.3. Семантическая полнота алгоритма

Доказательство теоремы о семантической полноте алгоритма состоит из

следующих этапов.

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

- Конечность ветвления в произвольном П-дереве позволяет применить к П-дереву лемму Кенига [Komg] для определения бесконечной нити в П-дереве.

- Данная бесконечная нить создается канонически: в этой нити возможно построение модельного множества [Hmtikka1].

Рассматривая П-дерево отметим, прежде всего, что в общем случае для логики предикатов оно не будет конечным, как для логики высказываний [Шангин], [Шангин1].

Лемма 4.3.1. В произвольном П-дереве за каждым блоком непосредственно следует только конечное число блоков.

Доказательство: полная индукция по степени g порождающего множества E_kиз произвольного блока аь

Мы допускаем, что за блоком следует бесконечное число блоков.

Базис: g = 0.

Если g = 0, то порождающее множество в пусто и построение новых блоков, непосредственно следующих за невозможно.

¹⁷ Если правило исключения двухпосылочно, то X - большая посылка.

Допущение неверно. Значит, за блоком следует конечное число блоков. Индуктивное предположение: лемма верна для произвольного g < п.

Индуктивный шаг: лемма верна для g = n.

В П-дереве имеем блок ak, из которого непосредственно следует бесконечное количество блоков.

Согласно свойствам П-дерева, из этого факта вытекает следующее:

(1) блок с такими свойствами единственен в данном П-дереве;¹⁸

(2) все следующие в П-дереве за ak блоки суть д-блоки, но сам ak не является д-блоком.¹⁹

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

Более того, т.к. a_k остается не достигнутым блоком и все непосредственно следующие за ak блоки суть д-блоки, то между этими блоками и ak имеет место только слабое непосредственное следование,²⁰ т.е. для любого j, VaА(a) g E^J_k, —A g E^J_k, A v B g E^j_k, A з B g E^j_k. Таким образом, для любого j, E^j_k состоит только из формул вида A v B, A з B.

Пусть в E¹k имеется, скажем, t формул вида A v B, A з B. Допустим, что ко всем этим формулам алгоритм применяет вц-правила, порождая, таким образом, в П-дереве t блоков, которые непосредственно следуют из блока a_k. Тогда в E^t+1_k не входят формулы из E¹k.

По лемме 3.3.7, g(E_k+₁) < g(E_k), если в E_k входят формулы вида VaА(a) или некоторые формулы максимальной степени из Ek перешли в Ek+1. Т.к. для любого j, VaА(a) g E^jk, то VaА(a) g E^tk.

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

¹⁹ Автомат порождает блоки, следующие из данного блока, затем посредством бэктрэкинга опять
возвращается к a_k и т.д., т.е. алгоритм «зацикливается» на блоке a_k.

²⁰ В противном случае достижимость этих блоков привела бы к достижимости a_k.

С другой стороны, мы показали, что в E^t+1k не входят формулы из E¹k. Отсюда g(E^t+¹_k) < g(E¹_k), т.е. добавленные в порожденное множество блока a_k формулы из блоков, следующих за ak, имеет степень меньшую, чем формулы, входящие в E¹k.

Поскольку для любого j, E^j_k конечно, алгоритм в конце концов исчерпает E^j_k, скажем, на шаге h, t < h. Тогда g(E^h_k) = 0, что противоречит условию о бесконечном ветвлении блока a_k.

Доказано.

Прежде чем перейти к доказательству теоремы о семантической полноте алгоритма, зададим некоторые определения [Непейвода].

Определение 4.3.2. П-дерево является достигнутым, если все блоки этого П-дерева суть д-блоки.

Если все блоки П-дерева суть д-блоки, значит, П-дерево конечно. Таким образом, некоторому достигнутому П-дереву соответствует счетное множество конечных алго-выводов.

Поскольку все конечные алго-выводы суть завершенные BMV-выводы (теорема 4.1.2), каждому достигнутому П-дереву соответствует бесконечное множество завершенных BMV-выводов.

Теперь нужно ответить на вопрос, множество каких алго-выводов соответствует недостигнутому П-дереву.

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

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

Определение 4.3.4. П-дерево является недостигнутым, если оно содержит незапертую нить.

После того, как мы установили конечность ветвления в произвольном П-дереве (лемма 4.3.1), можно применить лемму Кенига, согласно которой бесконечное П-дерево с конечным ветвлением содержит бесконечную нить [Konig], [Непейвода].

Напомним, что в П-дереве бесконечная нить, если она существует, единственна. Поэтому зададим построение этой нити так, чтобы она всегда содержала опровергающую модель. Т. е. множество формул, принадлежащих этой нити, должно образовывать множество Хинтикки [Hintikka], [Hintikka1].

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

Лемма 4.3.5. Для любых формул А и В из £ верно:

1. (а) A е £ == -A g £, (б) -A е £ == A g £,

2. —-A е £ == A е £,

3. A & B е £ == Aе £ и B е £,

4. -(A & B) е £ == -Aе £ или -B е £,

5. A v B е £ == Aе £ или B е £,

6. -(A v B) е £ == -Aе £ и -B е £,

7. A з B е £ == -Aе £ или B е £,

8. -(A з B) е £ == Aе £ и -B е £,

9. VaA(a) е £ => A(a/t) е £, для всех t из T(£),

10. -VaA(a) е £ => -A(a/t) е £, для некоторого t из T(£),

11. 3aA(a) е £ == A(a/t) е £, для некоторого t из T(£),

12. -3aA(a) е £ == -A(a/t) е £, для всех t из T(£).
Доказательство.

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

(1 б) Аналогично (1 а).

(2) По BMV-правилу -и.

(3) По BMV-правилу &и.

(4) Если -(А & В) е £, то по правилу -_вц текущей целью становится формула А & В. Разбиваем эту цель на подцели А и В, начиная работать с первой. Если А недостижима, то в £ вводится - А в качестве посылки. Если А достижима, то в качестве посылки в £ вводится - В. (Один из этих случаев должен иметь место, т. к. А & В недостижима и ф незаперта.)

(5) Если А v В е £ и -А е £, то формула В выводима по Vu. Если А v В е £ и -А g £, то возможно два подслучая. (а) Либо к формуле А v В применяется вц-правило

Vm, и текущей целью становится формула -А. Из нее по правилу -_ц вводим формулу -- А в качестве посылки в множество £. Из -- А по -_и получаем А. (б) Либо формула А v В получена по Vn из формулы А (В).

(6) По BMV-правилу -v^

(7) Если А з В е £ и А е £, то формула В выводима по з_и. Если А з В е £ и А £ £, то к формуле А з В применяется вц-правило з_вц и текущей целью становится формула А. Из нее по правилу -_ц вводим формулу -А в качестве посылки в £.

(8) Аналогично (4).

(9) Если УаА(а) е £, то квантор общности снимается по новой неабсолютной переменной x; в алго-выводе появляется формула A(x) и на формулу УаА(а) ставится метка М1, запрещающая применение к этой формуле правила У_и. Данная метка в дальнейшем снимается, если: (а) все формулы вида УаА(а) из множества £ отмечены М1 и (б) все иные формулы из множества £ отмечены М0, т.е. к ним применены те или иные правила алгоритма. В такой ситуации к каждой формуле вида УаА(а) из множества £ применяется правило У_вц. Согласно формулировке этого правила, квантор общности снимается по некоторым определенным термам из множества £, т. е. по всем термам из Л(£), по которым квантор общности еще не снимался.

(10) Если -УаА(а) е £, то по правилу -_вц текущей целью становится формула УаА(а). Применяем к этой цели правило У_ц и получаем формулу А(у), где y - новая абсолютная переменная. Т.к. А(у) недостижима, то применяем к ней правило -_ц и в множество £ вводится -А(у) в качестве посылки. При этом на формулу -УаА(а) ставится метка М5, не позволяющая еще раз применить к ней правило -вц.

(11) Если ЗаА(а) е £, то по правилу З_и получаем формулу А(у), где у - новая абсолютная переменная. При этом на формулу ЗаА(а) ставится метка М0, не позволяющая еще раз применить к ней правило З_и. Если на формуле ЗаА(а) уже стоит метка М0, таким образом, ЗаА(а) получена по З_в из формулы А(1), для некоторого терма t.

(12) Аналогично (9): к формуле -ЗаА(а) применяется правило -Зи и
выводится формула Уа-А(а).

Доказано.

• [Andrews] Andrews, P. Transforming matings into natural deduction proofs // 5^th Conference on Automated Deduction, 1980.

• [Basin et al] Basin, D., Matthews, S. and L. Vigano. Natural deduction for non-classical logics // Studia Logica, vol. 60, №1, 1998.

• [Bocharov et al] Bocharov, V., Bolotov, A., Gorchakov, A. and V. Shangin. Proof-searching algorithm in first order classical natural deduction calculus // 12th International Congress of Logic, Methodology and Philosophy of Science. Oviedo (Spain),

• [Bochmann] Bochmann, G. Hardware specification with temporal logic: an example // IEEE Transactions on computers, vol. C-31, №3, 1982.

• [Bolotov & Fisher] Bolotov, A. and M. Fisher. A resolution method for computational tree branching time temporal logic // IV International workshop on temporal representation and reasoning (TIME'97). Florida, 1997.

• [Hintikka] Hintikka, J. A new approach to sentential logic // Societas Scientarium Fennica Commentationes Physico-Mathematicae XVII, 2, 1957.

• [Hintikkai] Hintikka, J. Notes on the quantification theory // Societas Scientarium Fennica Commentationes Physico-Mathematicae XVII, 11, 1957.

• [Jaskowski] Jaskowski, S. On the rules of suppositions in formal logic // Studia Logica, №1, 1934.

• [Kalish] Kalish, D. Review of Copi: Symbolic logic. 3^rd ed. New-York, London, 1967 // The Journal of Symbolic Logic, vol. 39, №1, 1974.

• [Konig] Konig, D. Theorie der endlichen und unendlichen graphen, Akademische Verlagsgesellschaft M.B.H., Leipzig, 1936.

• [Li] Li, D. Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving // Journal of Automated Reasoning, vol. 18, №1, 1997.

• [Pelletier] Pelletier, F.J. Automated natural deduction in THINKER // StudiaLogica, vol. 60, №1, 1998, доступна по адресу: http://www.cs.ualberta.ca/~jeffp/.

• [Pelletier1] Pelletier, F.J. A brief history of natural deduction // History and Philosophy of Logic, vol. 20, 1999, доступна по адресу: http://www.cs.ualberta.ca/~jeffp/.

• [Pelletier2] Pelletier, F.J. Seventy-five graduated problems for testing automatic theorem provers // Journal of Automated Reasoning, 1986.

• [Pelletier3] Pelletier, F.J. Errata for 75 problems // Journal of Automated Reasoning, № 4, 1988.

• [Portoraro] Portoraro, F. Strategic constructions of Fitch-style proofs // Studia Logica, vol. 60, №1, 1998.

• [Quine] Quine, W. On natural deduction // The Journal of Symbolic Logic, vol. 15, №2, 1950.

• [Robinson] Robinson, J. A machine-oriented logic based on the resolution principle // Journal of the ACM, vol. 12, №1, 1965.

• [Sieg] Sieg, W. Mechanism and search: aspects of proof theory. Pittsburgh, 1992.

• [Sieg & Byrnes] Sieg, W. and J. Byrnes. Normal natural deduction proofs (in classical logic) // Studia Logica, vol. 60, №1, 1998.

• [Анисов] Анисов А.М. Современная логика. М., ИФРАН, 2003.

• [Болотов и др.] Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической логике предикатов // Логические исследования. Вып. 5. М.,

• [Болотов и др.1] Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической пропозициональной логике // Труды научно-исследовательского семинара логического центра Института философии РАН. М., ИФРАН, 1996.

• [Болотов и др.2] Болотов А.Е., Бочаров В.А., Горчаков А.Е., Макаров В.В., Шангин В.О. Пусть докажет компьютер // Логика и компьютер. Вып. 5. М., Наука, 2004. (Серия «Кибернетика - неограниченные возможности и возможные ограничения».)

• [Бочаров и Маркин] Бочаров В.А., Маркин В.И. Основы логики. М., Космополис, 1994.

• [Бочаров] Бочаров В.А. Исчисление предикатов с универсалиями (II. Семантика) // Логические методы в компьютерных науках. (Труды научно-исслед. семинара по логике Ин-та философии АН СССР); Сб. ст. / Редкол.: Смирнов В.А. (отв. ред.) и др. М., ИФАН, 1991.

• [Братко] Братко И. Программирование на языке Пролог для искусственного интеллекта: Пер. А.И. Лупенко, А.М. Степанова / под ред. А.М. Степанова. М., Мир, 1990.

• [Войшвилло] Войшвилло Е.К. Понятие. М., Изд-во МГУ, 1967.

• [Войшвилло 1] Войшвилло Е.К. Процедура поиска доказательства для формул системы Е // Войшвилло Е.К. Философско-методологические аспекты релевантной логики. М., МГУ, 1989.

• [Генцен] Генцен Г. Исследования логических выводов // Математическая теория логического вывода: Пер. с англ. А.В. Идельсона / Под ред. А. В. Идельсона и Г. Е. Минца. М., Наука, 1967.

• [Ивлев] Ивлев Ю.В. Логика: Учебник для высших учебных заведений. 2-е изд., перераб. и доп. М., Логос, 1997.

• [Макаров] Макаров В.В. Алгоритм поиска натурального вывода для интуиционистской логики высказываний // Автореферат диссертации на соиск. учен. степ. канд. филос. наук. М., Соцветие красок, 2002.

• [Мендельсон] Мендельсон Э. Введение в математическую логику: Пер. с англ. Ф.А. Кабакова / Под ред. С.И. Адяна. 2-е изд., испр. М., Наука, 1976.

• [Минц] Минц Г.Е. Теорема Эрбрана // Математическая теория логического вывода: Под ред. А.В. Идельсона и Г.Е. Минца. М., Наука, 1967.

• [Непейвода] Непейвода Н.Н. Прикладная логика: Учебное пособие. 2-е изд., испр. и доп. Новосибирск, Изд-во Новосиб. ун-та, 2000.

• [Смирнов] Смирнов В.А. Теория логического вывода. М., РОССПЭН,

• [Смирнов и др.] Смирнов В.А., Маркин В.И., Новодворский А.Е., Смирнов А.В. Доказательство и его поиск (курс логики и компьютерный практикум) // Логика и компьютер. Вып. 3. М., Наука, 1996. (Серия «Кибернетика - неограниченные возможности и возможные ограничения».)

• [Смирнов-мл.] Смирнов А.В. Система интерактивного доказательства теорем // Логические исследования. Вып. 2. М., Наука, 1993.

• [Смирнов-мл.1] Смирнов А.В. Язык описания логических систем для автоматического поиска доказательства // Автореферат диссертации в виде научного доклада на соиск. учен. степ. канд. филос. наук. М., 1998.

• [Чень и Ли] Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. Пер. с англ. / Под ред. С.Ю. Маслова. М., Наука, 1983.

• [Шангин] Шангин В. О. Теорема корректности для алгоритма поиска вывода в классической пропозициональной логике // Материалы VI Международной научной конференции «Современная логика: проблемы теории, истории и применения в науке». СПб., СПбГУ, 2000.

• [Шангин 1] Шангин В. О. Автоматический поиск натурального вывода в интуиционистской логике и проблема дубликации // Материалы VII Международной научной конференции «Современная логика: проблемы теории, истории и применения в науке». СПб., СПбГУ, 2002.

• [Шангин2] Шангин В.О. Метатеоретические свойства натурального вывода // Материалы IV Международной конференции «Смирновские чтения». М., ИФРАН, 2003.

• [Шангин3] Шангин В. О. Автоматический поиск натурального вывода в интуиционистской логике и проблема дубликации // Аспекты, Том 2. М., Современные тетради, 2003.

• [Шанин] Шанин Н.А., Давыдов Г.В., Маслов С.Ю., Минц Г.Е., Оревков В.П., Слисенко А.О. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний. Л., Наука, 1964.


	На главную \| В открытую библиотеку

-Переход в полный каталог почтовой службы рассылки диссертаций-