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

Размещено на http://www.allbest.ru/

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

Содержание

Введение

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

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

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

Вывод

Список использованных источников и литературы

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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].

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

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

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

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

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

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

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

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

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

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

Например, Г. Генцен предложил следующее непрямое правило v„: из формулы A v В, подвывода С из посылки А и подвывода С из посылки В выводима формула С. Однако можно предложить прямое правило v_H: из A v В, А =э С, В z> С выводима формула С, или из A v В, -А выводима формула В.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

При этом требуется, чтобы ни одна переменная не была абсолютно ограничена в выводе более одного раза и чтобы ни одна переменная не ограничивала сама себя (непосредственно, т.е. у не входит в zi,..., z_n, или по транзитивности, т.е. если 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, х) zd VzA(y, z)). Данная формула ложна, если в качестве А взять отношение равенства на множестве натуральных чисел.

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

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

В данном параграфе мы даем краткий обзор истории создания систем автоматического поиска вывода. Поскольку неотъемлемой частью создания таких систем является наличие программируемых электронно-вычислительных устройств, в начале данного параграфа приводятся некоторые факты из истории создания ЭВМ.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В 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), которые были созданы под руководством Л. Уоса. Программа создана для поиска доказательств для классической логики предикатов первого порядка с равенством, написана на языке С, занимает примерно 180 Кб и способна оперировать большим количеством дизъюнктов (миллиардами), что показывает ее высокую эффективность.

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

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

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

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

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

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

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

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

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

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

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

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

программа ANDP (Automated Natural Deduction Prover), разработанная Д. Ли (D.Li) [Li];

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

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

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

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

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

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

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

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

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

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

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

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



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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Таким образом, мы вновь сталкиваемся с ситуацией, которая стимулировала развитие исследований именно по поиску натурального вывода: сначала вывод строится в другом исчислении (которое более благоприятно с точки зрения автоматического поиска вывода), а затем вывод в этом исчислении конструктивно перестраивается в натуральный вывод [Andrews]. Т.е. натуральный вывод в CMU РТ строится не в системе натурального вывода, а с помощью промежуточного исчисления. Что касается Prover, то программа строит натуральный вывод именно в системе натурального вывода. Таким образом, наша работа заполняет своеобразную лакуну, которая образовалась в области автоматического поиска НВ.

Вывод

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

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

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