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

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

Автор: Шангин, Василий Олегович

Шифр специальности: 09.00.07

Научная степень: Кандидатская

Год защиты: 2004

Место защиты: Москва

Количество страниц: 109 с.

Артикул: 2741884

Автор: Шангин, Василий Олегович

Стоимость: 250 руб.

ОГЛАВЛЕНИЕ
Введение.
Глава 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, Заключения и Литературы.

Рекомендуемые диссертации данного раздела

28.06.2016

+ 100 бесплатных диссертаций

Дорогие друзья, в раздел "Бесплатные диссертации" добавлено 100 новых диссертаций. Желаем новых научных ...

15.02.2015

Добавлено 41611 диссертаций РГБ

В каталог сайта http://new-disser.ru добавлено новые диссертации РГБ 2013-2014 года. Желаем новых научных ...


Все новости

Время генерации: 0.175, запросов: 111