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

• Автор: Шангин, Василий Олегович
• Шифр специальности: 09.00.07
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Москва
• Количество страниц: 109 с.

ОГЛАВЛЕНИЕ
Введение.

Глава 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. Семантическая полнота алгоритма.
Заключение.
Литература


Представить содержательное описание алгоритма поиска вывода в виде формальных правил поиска вывода. Опираясь на вышеупомянутый результат, доказать теорему о семантической непротиворечивости алгоритма поиска вывода в данном исчислении. Разработать представление линейного алгоритмического вывода в натуральных исчислениях типа Куайна в виде древовидной структуры, узлами которой являются не формулы вывода, а особенные конечные последовательности формул вывода блоки, переход между которыми осуществляется с помощью формальных правил поиска вывода алгоритма. Показать с помощью представления алгоритмического вывода в виде древовидной структуры конечность ветвления в произвольном блоке. Обосновать возможность прямого т. Методологические основы и источники исследовании. При решении поставленных задач автор опирался на современный аппарат символической логики. В диссертационной работе использовались формулировки систем натурального вывода, предложенные В. Л. Бочаровым, Е. К. Войшвилло, Г. Генценом, Ф. Пеллетье, Дж. Поллоком, В. Л. Смирновым и др. В основе описанного в диссертационном исследовании алгоритма поиска вывода лежит алгоритм поиска вывода в классической логике предикатов, предложенный Л. Е. Болотовым, В. Л. Бочаровым и Л. Е. Горчаковым. В процессе использования написанной этими авторами программы возникла необходимость модифицировать данный алгоритм, определенным образом упростить процедуру поиска натурального вывода и четко сформулировать процедуру унификации. Научная новизна исследования. В диссертационном исследовании предложен метод доказательства теоремы о семантической непротиворечивости для натурального исчисления типа Куайна. Показана гибкость данного метода, позволяющая применять его и к другим натуральным исчислениям этого типа, отличительными свойствами которых являются наличие прямого правила удаления квантора существования и использование в выводе абсолютно и относительно ограниченных переменных. Предложено оригинальное доказательство теоремы о семантической непротиворечивости для натурального исчисления типа Куайна с абсолютно и относительно ограниченными переменными. Модифицирован стандартный алгоритм унификации дтя временных переменных и сколемовских функций с целью работы с абсолютно и относительно ограниченными переменными. Предложено оригинальное представление алгоритмического вывода в виде древовидной структуры поисковое дерево, узлами которого являются непустые, конечные последовательности формул блоки. Обоснован прямой метод доказательства теоремы о семантической полноте алгоритма поиска натурального вывода. С помощью данного метода предлагается оригинальное доказательство теоремы о семантической полноте для алгоритма поиска натурального вывода в исчислениях типа Куайна. Предложено оригинальное доказательство теоремы о семантической полноте для системы натурального вывода тина Куайна, следующее из теоремы о семантической полноте для алгоритма поиска вывода в данной системе. Практическая значимость. Разработанный алгоритм поиска натурального вывода в исчислениях типа Куайна может служить основой для создания компьютерных реализаций, которые, в свою очередь, могут использоваться в псдагошческой практике, облегчая усвоение основ дедукции. Содержание диссертационного исследования может быть использован для разработки специального курса по автоматическому поиску логаческого вывода. Апробация работы. Основные положения и результаты диссертационного исследования докладывались на VI и VII Международных научных конференциях Современная логика проблемы теории, истории и применения в науке СанктПетербург, и , IV Международной конференции Смирновские чтения Москва, и XII Международном конгрессе по логике, философии и методологии науки Овьедо, . Струстура диссертации. Диссергация состоит из Введения, 4х глав Автоматический поиск натурального вывода история вопроса, Анализ системы натурального вывода V, Алгоритм поиска вывода в системе ВМУ и Анализ алгоритма поиска вывода в системе V, Заключения и Литературы.