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

Полный текст автореферата диссертации по теме "Автоматический поиск натурального вывода в классической логике предикатов"

Московский государственный университет им. М.В. Ломоносова Философский факультет

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

ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ

АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ

Автореферат

диссертации на соискание ученой степени кандидата философских наук Специальность 09.00.07 - Логика

Москва 2004

Работа выполнена на кафедре логики философского факультета Московского государственного университета им. М.В. Ломоносова

Научный руководитель:

Доктор философских наук, профессор Бочаров В.А Официальные оппоненты:

Доктор философских наук Бирюков Б.В.

Кандидат философских наук Макаров В.В.

Ведущая организация:

Институт философии РАН, сектор логики

Защита состоится_года в_часов на

заседании Диссертационного совета Д 501.001.48 по защите диссертаций на соискание ученой степени доктора философских наук в Московском государственном университете им. М.В. Ломоносова по адресу:

119899, Москва, Ленинские горы, 1-ый корпус гуманитарных факультетов МГУ, философский факультет, 11 этаж, ауд._.

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

Автореферат разослан_года.

Ученый секретарь Диссертационного совета

кандидат философских наук

ЗайцевД.В.

Общая характеристика работы

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

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

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

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

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

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

РОС. НАЦИОНАЛЬНАЯ БИБЛИОТЕКА

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

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

которое следует из теоремы Генцена об устранении сечения, существенно облегчает

i

поиск вывода в данных исчислениях.

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

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

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

Д. Пеллетье предложил программу поиска натурального вывода Thinker в классической логике предикатов первого порядка (а также в некоторых неклассических

1 Генцен Г. Исследования логических выводов // Математическая теория логического вывода: Пер. с англ. А.В. Идельсона / Под ред. А.В. Идельсона и Г.Е. Минца. М., Наука, 1967.

2 Pollock, J. Skolemization and unification in natural deduction, неопубликованная версия статьи доступна по адресу: http://oscarhome.soc-sci arizona edu/ftp/publications.html.

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

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

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

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

Группа отечественных исследователей под руководством Н.А.Шанина предложила процедуру поиска натурального вывода типа Генцена в классической

3 Pelletier, F.J. Automated natural deduction in THINKER // Studia Logica, vol. 60, № 1, 1998, доступна по адресу, http://www.cs.ualbeita.ca/~jeffp/.

4 Sieg, W. and J. Byrnes. Normal natural deduction proofs (in classical logic) // Studia Logica, vol. 60, №1, 1998.

5 Li, D. Unification algorithms for eliminating and introducing quantifiers in natural deduction automated

theorem proving //Journal of Automated Reasoning, vol. 18, №1,1997.

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

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

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

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

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

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

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

6 Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической логике предикатов // Логические исследования. Вып. 5. М., Наука, 1998.

Шанин Н.А., Давыдов Г.В., Маслов С.Ю., Минц Г.Е., Оревков В.П., Слисенко А.О. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний. Л., Наука, 1964.

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

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

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

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

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

• •' Насыщенностью (сверху вниз) множества формул, принадлежащих выделяемой таким образом нити, которая позволяет определить данное множество формул как множество Хинтикки.

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

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

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

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

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

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

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

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

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

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

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

Апробация работы. Основные положения и результаты диссертационного исследования докладывались на VI и VII Международных научных конференциях «Современная логика: проблемы теории, истории и применения в науке» (Санкт-Петербург, 2000 и 2002), IV Международной конференции «Смирновские чтения» (Москва, 2003) и XII Международном конгрессе по логике, философии и методологии науки (Овьедо, 2003).

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

Основное содержание работы

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

В первой главе - «Автоматический поиск натурального вывода: история вопроса» - дается исторический обзор исследованиям по автоматическому поиску вывода. Особенное внимание уделяется современному состоянию дел в области автоматического поиска натурального вывода. Глава состоит из 3 параграфов.

В параграфе 1.1 - «Натуральный вывод как тип логического вывода» -рассматривается история развития систем натурального вывода (НВ), идущая от вышедших в 1934 году работ Г. Генцена и С. Яськовского.8

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

8 Генцен Г. Исследования логических выводов // Математическая теория логического вывода: Пер. с англ. А.В. Идельсона / Под ред. А.В. Идельсона и Г.Е. Минца. М., Наука, 1967. Jaskowski, S. On the rules of suppositions in formal logic // Studia Logica, №1,1934.

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

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

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

Подробно рассматриваются классификации систем НВ, предложенные Д. Пеллетье и ВА. Смирновым.9

В параграфе 1.2 - «История создания систем автоматического поиска вывода»

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

В параграфе 1.3 - «Автоматический поиск вывода в натуральном исчислении»

- анализируются некоторые алгоритмы поиска НВ и выявляются их сильные и слабые стороны.

Анализ работ сведен в таблицу, в верхней строке которой перечислены следующие алгоритмы поиска НВ в классической первопорядковой логике: 1) THINKER, разработанный Д. Пеллетье; 2) OSCAR, разработанный Дж. Поллоком; 3) ANDP, разработанный Д. Ли; 4) CMU РТ, разработанный У. Сигом, Р. Шейнсом и Дж. Бернсом; 5) Symlog, разработанный Ф. Портораро; 6) Prover, разработанный

9 Pelletier, F.J. A brief history of natural déduction // History and Philosophy of Logic, vol. 20,1999, доступна по адресу: http://www.cs.ualberta.ca/~jeffp/. Смирнов В А Теория логического вывода. М., РОССПЭН, 2000.

В.А. Бочаровым, А.Е. Болотовым и А.Е. Горчаковым и модифицированный В.О. Шангиным.10

В первом столбце таблицы находятся признаки, по отсутствию или наличию которых анализируются данные алгоритмы поиска вывода: 1) алгоритм работает с предикатом равенства; 2) алгоритм работает с эквиваленцией; 3) алгоритм работает с неклассическими логиками; 4) множество используемых алгоритмом переменных ограничено; 5) для алгоритма доказываются теоремы о его свойствах (непротиворечивость, полнота и т.д.); 6) алгоритм использует сколемовские термы; 7) алгоритм имеет программную реализацию.

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

Thinker Oscar ANDP CMU PT Symlog Prover

1 - + - - - - -

2 - + - + - + -

3 Неклассика + + - + - +

4 Ограничение на переменные + - - - - -

5 Свойства - + - + - + - +

6 Явная сколемизация - + - + + -

7 Реализация + + + + + + -

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

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

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

10 Pelletier, D. Ibid, Pollock, J. Ibid, Li, D. Ibid, Sieg, W. Ibid, Portoraro, F. Strategic constructions of Fitch-style

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

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

В параграфе 2.1 - «Формулировка системы ВМУ» задаются алфавит (понятие терма и формулы) языка логики предикатов первого порядка без предиката равенства и основные понятия для системы натурального вывода ВМУ.

Правила системы натурального вывода ВМУ (ВМУ-правила):

proofs // Studia Logica, vol. 60, №1,1998. Бочаров В.А. Там же. "Бочаров В.А., Маркин В.И. Основы логики. М., Космополис, 1994.

В правилах V, И Зи запись «Р — абс.; у|,.,., Ун - огр.» означает, что р абсолютно ограничена в выводе и переменная Р относительно ограничивает каждую переменную из списка уь-.., уп, где уь..., у„ суть свободные переменные, входящие в посылки данных правил.

Определение 2.1.3. Выводом в системе БМУ (BMV-выводом) называется непустая конечная последовательность формул Сь Сг,..-» Сл (п > 1), удовлетворяющая следующим условиям:

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

2. при применении правил о, И все формулы, начиная с последней неисключенной посылки С| (1 > 1 £ п) и вплоть до результата применения данного правила С| О С) (1 > ] > п) ИЛИ —|С„ исключаются из дальнейших шагов вывода в том смысле, что к ним запрещено применять правила вывода;

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

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

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

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

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

В параграфе 2.2 - «Семантическая непротиворечивость системы БМУ» -приводится доказательство утверждения, что система БМУ семантически непротиворечива.

Существенную роль при доказательстве данной теоремы играет наличие в любом завершенном ВМУ-выводе пассивной переменной.

Определение 2.2.1. Переменная а называется активной (пассивной) в ВМУ-выводе, если а абсолютно ограничена в этом выводе и (не) существует абсолютно ограниченная в этом выводе переменная Р, которую относительно ограничивает переменная а.

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

Наличие любом завершенном ВМУ-выводе пассивной переменной устанавливается леммой 2.2.2.

Лемма 2.2.3. В произвольном завершенном ВМУ-выводе последняя формула этого вывода логически следует из множества неисключенных посылок Г.

Данная лемма доказывается методом двойной математической индукции по числу всех применений ВМУ-правил и по рангу (числу абсолютно ограниченных переменных) произвольного завершенного вывода. В обосновании данного метода мы следуем работе В.А. Смирнова.12

Для доказательства этой леммы достаточно доказать три утверждения: (А) лемма верна для всех завершенных выводов, ранг и число применений правил вывода в которых равны 0;

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

Смирнов В А. Теория логического вывода. М., РОССПЭН, 2000. С. 122-123.

Завершенный вывод Зх\/гА(х, г) из ЗхУуА(х, у):

1. ЭхУуА(х, у)

2.УуА(х,у)

3.А(х,у)

4. УгА(х, г)

5. ЗхУгА(х, г)

- 3,: 1; х - абс.

- V,: 3; у - абс., х - отн. -3,:4

-пос.

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

При доказательстве утверждения (А) анализируется тривиальный завершенный БМУ-вывод, в котором заключение входит в множество всех неисключенных посылок данного вывода.

При доказательстве утверждения (Б) анализируются все БМУ-правила, кроме правил V, И Зи. Показывается, что все БМУ-правила, кроме правЗдраняют общезначимость заключения при общезначимости посылок.

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

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

Из леммы 2.2.3 следует, что система БМУ семантически непротиворечива (теорема 2.2.4).

В третьей главе - «Алгоритм поиска вывода в системе БМУ» - для незначительно измененной формулировки системы БМУ детально описывается алгоритм поиска БМУ-вывода, эксплицируются правила поиска вывода в системе БМУ и задается процедура унификации. Глава состоит из 4 параграфов.

В параграфе 3.1 - «Изменение формулировки системы БМУ» - в целях эффективности автоматического поиска вывода к БМУ-правилам добавляются следующие производные правила исключения логических связок:

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

13 Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической пропозициональной логике // Труды научно-исследовательского семинара логического центра Института

Далее анализируются правила V, И Э„, т.е. правила системы, которые приводят к появлению в выводе абсолютных переменных.

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

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

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

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

Логический анализ отношения «индивидная переменная Р относительно ограничивает в BMV-выводе индивидную переменную у» показывает, что оно иррефлексивно (в выводе ни одна переменная не ограничивает сама себя) и транзитивно (если в выводе а ограничивает Р и Р ограничивает у, ТО а ограничивает у). Значит, отношение ограничения есть отношение строгого (частичного) порядка.

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

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

философии РАН. М., ИФРАН, 1996. Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической логике предикатов //Логические исследования. Вып. 5. М., Наука, 1998.

Показывается, что данный алгоритм унификации конечен и всегда находит наиболее общий унификатор для унифицируемого множества А (теорема 3.2.4).

В параграфе 3.3 - «Правила поиска вывода в системе БМУ» - подробным образом анализируются правила поиска БМУ-вывода.

Основная идея нижеследующего алгоритма - построение двух непустых последовательностей: последовательности формул вывода ПВ (собственно, БМУ-вывод) и последовательности формул целей ПЦ (данная последовательность не входит в БМУ-вывод).

Правила поиска вывода делятся в системе БМУ на две группы, что соответствует двум (синтетическому и аналитическому) направлениям, в которых осуществляется поиск вывода.

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

Все правила вывода системы БМУ рассматриваются как синтетические правила поиска вывода в этой системе и применяются только к ПВ.

Аналитические правила вывода делятся, в свою очередь, на ц-правила и вц-

правила.

Ц-правила применяются к ПЦ и сводят «задачи поиска некоторого вывода к одной или нескольким подзадачам по поиску вспомогательных выводов».15

" Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. Пер. с англ. / Под ред. СЮ. Маслова. М., Наука, 1983.

15 Смирнов В.А., Маркин В.И., Новодворские А.Е., Смирнов А.В. Доказательство и его поиск (курс логики и компьютерный практикум) // Логика и компьютер. Вып. 3. М., Наука, 1996. (Серия «Кибернетика - неограниченные возможности и возможные ограничения».) С. 4.

Задаются следующие ц-правила:

В правиле —1„ формула А может быть либо элементарной формулой Р(а), либо

-iC, либо С v D, либо ЭаС.

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

Задаются следующие вц-правила:

В правиле —1ВЦ формула А не имеет вида элементарной формулы Р(а), ИЛИ С V Э, или ЭаС. В правиле V,,, терм I не может быть неабсолютной переменной; при этом неисключенная формула А(аЛ) не находится выше в ПВ.

В параграфе 3.4 - «Описание алгоритма поиска вывода в системе БМУ» задаются основные процедуры алгоритма, описываются их особенности и порядок применения; подробно описывается механизм меток: объясняется, когда и на какие формулы и цели ставятся (снимаются) метки; завершается данный параграф пошаговым описанием алгоритма поиска вывода в системе БМУ и примером его работы.

К формулам из последовательности формул вывода (ПВ) применяются следующие процедуры:

Процедура 1 * определяет применение синтетических правил исключения.

Процедура 2* определяет применение синтетических правил введения.

Процедура 3* определяет применение всех вц-правил, кроме Увц.

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

К формулам из последовательности формул целей (ПЦ) применяется Процедура 5*, которая определяет применение ц-правил.

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

Процедура б* осуществляет глобальную подстановку - наиболее

общий унификатор.

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

В четвертой главе - «Анализ алгоритма поиска вывода в системе BMV» -исследуются свойства алгоритма поиска вывода в системе BMV. Глава состоит из 3 параграфов.

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

Алгоритмическим BMV-выводом (алго-выводом) называется пара <А, В>, где

(А) непустая последовательность формул вывода (ПВ), для которой верно:

(О Каждая формула в ПВ является или начальной посылкой, или посылкой, полученной по ц-правилам, или формулой, полученной из предыдущих по одному из BMV-правил;

(И) Если в ПВ применялись правила то все формулы, начиная с

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

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

(№) Ни одна переменная в результате унификации не ограничивает сама себя;

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

Алго-выводом формулы А из (возможно, пустого) множества посылок Г называется конечный алго-вывод, в котором

• Последовательность формул вывода есть ВМУ-вывод формулы А из Г;

• Формула А является главной целью и А достигнута.

Показывается, что последовательность формул вывода в алго-выводе А из Г есть завершенный ВМУ-вывод формулы А из Г (лемма 4.1.1).

Из леммы 4.1.1 и теоремы 2.2.4 следует, что в алго-выводе формулы А из (возможно, пустого) множества Г формула А семантически следует из Г (теорема 4.1.2).

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

Определение 4.1.3. Блоком а,, 5 6 N. является непустая последовательность формул вывода и (возможно, пустая) последовательность целей

(1) Если д\ есть главная цель алго-вывода, то в этом случае ! = 1; Если д\ получена

по одному из вц-правил, то в этом случае 1 > 1;

(И) Каждая цель, кроме д\, получена по ц-правилам;

(ш) Последней целью блока является либо X, либо формула из ПЦ, которая

унифицируется с некоторой формулой из ПВ.

(1у) Каждая формула из последовательности вывода в а, либо является начальной

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

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

Показывается, что в произвольном алго-выводе каждый блок конечен (лемма

4.2.1).

Для определения понятия «поисковое дерево» вводится ряд понятий. Определение 4.2.2. Если блок а получен в результате применения -1>ш гЭи, и Ущ, ТО а является достигнутым (ц-блоком), если (X — последний блок алго-вывода и последняя цель в а достигнута. Если блок а получен в результате применения ТО а является достигнутым (д-блоком), если а - последний блок алго-вывода и первая формула в а исключена.

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

Определение 4.2.3. Блок (Хц непосредственно следует за блоком (Хк (к < п), если при порождении последним недостигнутым блоком является

Определение 4.2.4. Поисковым деревом (П-деревом) для алго-вывода является частично упорядоченное множество {(Хь <Х;>,...} блоков, распределенных по непересекающимся «уровням» следующим образом:

1. Нулевой уровень состоит из единственного блока (XI, называемого начальным блоком;

2. Каждый блок 1+1-го уровня соединён отрезком в точности с одним блоком 1-го уровня;

3. Каждый блок а 1-ГО уровня либо не соединён ни с одним блоком 1+1-го уровня, либо соединён отрезками с несколькими блоками 1+1-го уровня (эти блоки 1+1-го уровня называются непосредственно следующими за блоком а);

4. Блок 1-го уровня, не соединённый ни с какими блоками 1+1-го уровня, называется заключительным блоком.

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

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

С помощью понятия П-дерева описывается процесс поиска алго-вывода.

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

1. pvq -пос.

2. Я -пос.

3. -я -пос.

4. Р -ПОС.

1

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

Ситуация в первопорядковой логике сложнее. В силу результата А. Черча о неразрешимости классической первопорядковой логики предикатов, невозможно за конечное число шагов определить, доказуема ли произвольная формула или нет.1

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

16 Шангин В.О. Автоматический поиск натурального вывода в интуиционистской логике и проблема дубликации // Аспекты, Том 2. М., Современные тетради, 2003.

"Church, A. A note on the Entscheidungsproblem // The Journal of Symbolic Logic, vol. 1, № 1,1936.

"Минц Г.Е. Теорема Эрбрана // Математическая теория логического вывода: Под ред. А В. Идельсона и Г.Е. Минца. М., Наука, 1967.

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

Анализируя данную ситуацию, Ч. Чень и Р. Ли пишут: «Тем не менее существуют алгоритмы поиска доказательства, которые могут подтвердить, что формула общезначима, если она на самом деле общезначима. Для необщезначимых формул эти алгоритмы, вообще говоря, не заканчивают свою работу. Принимая во внимание результат Черча и Тьюринга, это лучшее, что мы можем ожидать от алгоритма поиска доказательства».1'

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

Определение 4.2.5. Линейно упорядоченная последовательность блоков aj, Ct2> ... называется нитью данного П-дерева, если 1) ОЦ - начальный блок и 2) Van (n > 1 И Иц непосредственно следует за a„.i).

Интуитивно алго-вывод представляется как последовательность блоков, полученных по одному из вц-правил. В такой ситуации большую роль играют формулы вывода, к которым применимы вц-правила (вц-формулы). Такими формулами являются формулы -iA, А Э В, А V В, к которым не применялись правила исключения, и формулы VaA(a). К этим и только этим формулам применяются вц-правила.

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

Данное определение выделяет роль вц-формул в процессе поиска вывода.

19 Чень Ч., Ли Р. Цит. Соч. С. 52.

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

£ 0, назовем порождающим множеством формул блока Оц НИТИ где Оь все такие вц-формулы; причем, -формулы вида

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

к которым применимо правило

Множество конечно для любых конечных т.к. все блоки П-дерева конечны (лемма 4.2.1).

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

Тогда степень множества (обозначается есть степень формулы

наибольшей степени из

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

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

порождающих множеств не увеличивается (лемма 4.2.7).

В параграфе 4.3 - «Семантическая полнота алгоритма» - предлагается доказательство утверждения о конечности ветвления в произвольном П-дереве, доказательство утверждения о семантической полноте алгоритма поиска ВМУ-вывода и доказательство утверждения о семантической полноте системы натурального вывода ВМУ.

Показывается, что в произвольном П-дереве за каждым блоком непосредственно следует только конечное число блоков (лемма 4.3.1).

Определение 4.3.2. П-дерево является достигнутым, если все блоки этого П-дерева суть д-блоки.

Если все блоки П-дерева суть д-блоки, то П-дерево конечно. Таким образом, достигнутому П-дереву соответствует бесконечное множество конечных алго-выводов.

Поскольку все конечные алго-выводы суть завершенные ВМУ-выводы (теорема 4.1.2), каждому достигнутому П-дереву соответствует бесконечное множество завершенных ВМУ-выводов.

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

блока а_ пусто.

Определение 4.3.4. П-дерево является недостигнутым, если оно содержит незапертую нить.

Лемма 4.3.1 позволяет применить к недостигнутому П-дереву лемму Кенига для определения незапертой нити.20

Показывается, что множество неисключенных формул вывода, принадлежащих незапертой нити в недостигнутом П-дереве для алго-вывода формулы А из (возможно, пустого) множества посылок Г, является множеством Хинтикки (лемма 4.3.5).21

Из леммы 4.3.5 следует по контрапозиции, что если формула А семантически следует из Г, то существует алго-вывод А из Г (лемма 4.3.7).

Из леммы 4.3.7 следует, что система натурального вывода БМУ семантически полна (теорема 4.3.8).

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

• разработать прямое, а не косвенное доказательство теоремы о семантической полноте системы натурального вывода БМУ,

• обобщить предложенный алгоритм поиска вывода и прямой метод доказательства теоремы о семантической полноте алгоритма поиска вывода на неклассические логики предикатов,

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

20 König, D. Theorie der endlichen und unendlichen graphen, Akademische Verlagsgesellschaft M.B.H., Leipzig, 1936.

21 Hintikka, J. Notes on the quantification theory // Societas Scientarium Fennica Commentationes Physico-Mathematicae XVII, 11,1957.

Результаты диссертационной работы нашли отражение в следующих публикациях автора:

1. Болотов А.Е., Бочаров В.А., Горчаков А.Е., Макаров В.В., Шангин В.О. Пусть докажет компьютер // Логика и компьютер. Вып. 5. М., Наука, 2004. (Серия «Кибернетика - неограниченные возможности и возможные ограничения».) -13 п. л.

2. Шангин В.О. Автоматический поиск натурального вывода в интуиционистской логике и проблема дубликации II Аспекты, Том 2. М., Современные тетради, 2003. -1 п.л.

3. Шангин В.О. Теорема корректности для алгоритма поиска вывода в классической логике высказываний // Электронный журнал «Logical Studies», №4, 2000. ISBN 5-85593-140-4 http://www.logic.ru/Russian/LogStud/04/LS4.html -1 п.л.

4. Шангин В.О. Теорема корректности для алгоритма поиска вывода в классической пропозициональной логике // Материалы VI Международной научной конференции «Современная логика: проблемы теории, истории и применения в науке». СПб., СПбГУ, 2000.- 0,1 пл.

5. Шангин В.О. Автоматический поиск натурального вывода в интуиционистской логике и проблема дубликации // Материалы VII Междунеродной научной конференции «Современная логика: проблемы теории, истории и применения в науке». СПб., СПбГУ, 2002. - 0,1 пл.

6. Шангин В.О. Метатеоретические свойства натурального вывода // Материалы IV Международной конференции «Смирновские чтения». М., ИФРАН, 2003. - 0,1 п.л.

№2583$

Отпечатано в учебной типографии МГУ Москва, ГСП-2, Ленинские горы, МГУ, 1-й корпус гуманитарных факультетов Тираж 100 экз Подписано в печать 25.11.2004

Оглавление научной работы автор диссертации — кандидата философских наук Шангин, Василий Олегович

Введение.

Глава 1. Автоматический поиск натурального вывода: история вопроса. $ 1.1. Натуральный вывод как тип логического вывода. $ 1.2. История создания систем автоматического поиска вывода. $ 1.3. Автоматический поиск вывода в натуральном исчислении.

Глава 2. Анализ системы натурального вывода ВМУ. 2.1. Формулировка системы ВМУ. 2.2. Семантическая непротиворечивость системы ВМУ.

Глава 3. Алгоритм поиска вывода в системе ВМУ. $ 3.1. Изменение формулировки системы ВМУ.

§3 2. Унификация. 3.3. Правила поиска вывода в системе ВМУ.

§ 3.4. Описание алгоритма поиска вывода в системе ВМУ.

Глава 4. Анализ алгоритма поиска вывода в системе ВМУ. 4.1. Семантическая непротиворечивость алгоритма. 4.2. Свойства алгоритма. 4.3. Семантическая полнота алгоритма.

Введение диссертации2004 год, автореферат по философии, Шангин, Василий Олегович

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Апробация работы. Основные положения и результаты диссертационного исследования докладывались на VI и VII Международных научных конференциях «Современная логика: проблемы теории, истории и применения в науке» (Санкт-Петербург, 2000 и 2002), IV Международной конференции «Смирновские чтения» (Москва, 2003) и XII Международном конгрессе по логике, философии и методологии науки (Овьедо, 2003).

Структура диссертации. Диссертация состоит из Введения, 4-х глав: «Автоматический поиск натурального вывода: история вопроса», «Анализ системы натурального вывода BMV», «Алгоритм поиска вывода в системе BMV» и «Анализ алгоритма поиска вывода в системе ВМУ», Заключения и Литературы.

Заключение научной работыдиссертация на тему "Автоматический поиск натурального вывода в классической логике предикатов"

Заключение

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

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

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

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

Доказательство теоремы о семантической непротиворечивости системы опирается на предложенное У. Куайном доказательство теоремы о семантической непротиворечивости.

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

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

21 Определение 2.1.4.

В связи с этим вводится понятие пассивной переменной в ВМУ-выводе (доказательстве), т.е. такой абсолютно ограниченной переменной в ВМУ-выводе (доказательстве), которая не ограничивает относительно ни одну абсолютно ограниченную переменную данного ВМУ-вывода (доказательства).22

Показывается, что в произвольном алго-выводе всегда найдется пассивная переменная (Лемма 2.2.4).

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

С использованием теоремы о семантической непротиворечивости системы натурального вывода ВМУ показывается, что данный алгоритм обладает свойством семантической непротиворечивости, поскольку каждый вывод (доказательство), полученный алгоритмом, является выводом (доказательством) в системе ВМУ (Теорема 4.1.2).

Понятие вывода (доказательства) в системе ВМУ предполагает, что в выводе (доказательстве) ни одна переменная не ограничивает сама себя. Переменная ограничивает другую переменную согласно формулировкам правил \/в, Зи.

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

Таким образом, отношение ограничения, заданное на множестве переменных вывода (доказательства), является отношением строгого (частичного) порядка.

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

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

22 Определение 2.2.1.

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

Показывается конечность ветвления для произвольного блока в произвольном дереве поиска вывода (Лемма 4.3.1).

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

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

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

Поскольку всякий алгоритмический вывод есть вывод в системе ВМУ, из утверждения о семантической полноте алгоритма следует утверждение о семантической полноте системы ВМУ (Теорема 4.3.8).

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

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