<<
>>

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

У. Сиг вместе с Дж. Бернсом [Sieg], [Sieg &Byrnes] предложили программу автоматического поиска натурального вывода CMU PT в классической логике (авторы

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

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

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

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

В значительной степени на работы группы под руководством Н.А. Шанина опирается У. Сиг.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

Еще по теме Введение:

  1. Введение
  2. Введение
  3. ВВЕДЕНИЕ
  4. ВВЕДЕНИЕ
  5. Оглавление
  6. Курс наук н философское познание в афинской школе.
  7. СОДЕРЖАНИЕ
  8. Оглавление
  9. ОГЛАВЛЕНИЕ
  10. Акусмы как мыслительный феномен
  11. БИБЛИОГРАФИЯ
  12. 1.1. Жизнеописание Прокла у античных авторов.
  13. Пребывание — исхождение — возвращение (μονή ~~ πρόοδος* — Επιστροφή).