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

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

Содержание

Введение. Общая характеристика работы

Глава 1. Исторические предпосылки.

1.1. Предыстория создания формальных систем и исчислений

1.2. Предыстория создания вычислительных машнн

1.3. Первые системы автоматического вывода

1.4. Тематическая структура.

Глава 2. Секвенциальные системы генерирования доказательств теорем для

интуиционистской логики.

2.1. Секвенциальные исчисления.

2.2. Префиксные исчисления

Глава 3. Поиск доказательств теорем в натуральном исчислении
3.1. Поиск вывода в классической логике высказываний
3.2. Поиск вывода в интуиционистской лотке высказываний.
Глава 4. Алгоритм поиска доказательств теорем интуиционистской пропозициональной логики
4.1. Натуральное исчисление МН1
4.2. Алгоритм поиска вывода.
4.3. Адекватность алгоритма.
Заключение
Приложение 1. Ргооуег для натурального классического исчисления высказываний .
Библиография


В отечественной литературе можно отмстить работы Воробьева . ., Шанина . ., Смирнова В. А., Непейводы . . и других. Научная новизна исследования. Как было отмечено, создание и реализация на основе натурального исчисления алгоритмов автоматического поиска доказательств до сих пор является мало разработанной областью. Недостаток внимания, уделяемого натуральному выводу в области автоматического доказательств, обусловлен некоторым скептицизмом, порожденным именно фактом специфики этого метода доказательства как синтетической процедуры. Наличие правил введения логических связок рассматривается как камень преткновения на пути автоматизации натурального вывода. Заметное влияние на такое отношение к натуральным исчислениям оказала также тесная их связь с секвенциальными исчисления. Так, Бибель В. Характерно, что в англоязычной литературе часто под термином i полагаются не системы натурального вывода в нашем понимании, а как раз те или иные варианты секвенциального представления логики. В представленной диссертационной работе замечание Бибеля В. Болотовых А. Е., Бочаровым В. А. и Горчаковым А. Е., возможно описать односукиедентным секвенциальным исчислением. Однако в доказательстве, построенном таким алгоритмом, используются более традиционные правила, чем это имеет место в этом секвенциальном исчислении. . i i ii i. . i. . . 7. В интуиционистских секвенциальных исчислениях значительно увеличиваются трудности алгоритмизации поиска доказательств по сравнению с классической логикой. Так, например, появляется зацикливание поиска вывода, возникает большое количество несущественных вхождений формул в выводе, которые могут однако помешать построению доказательства, и прочее. Выявление путей создания алгоритма поиска доказательств для интуиционистской логики в натуральном исчислении, лишенного подобных негативных свойств, представляет собой научную новизну данного исследования. Цель и задачи исследования. Основная цель диссертационною исследования заключается в том, чтобы разработать и обосновать решение проблемы построения алгоритма поиска доказательств теорем для интуиционистской логики высказываний в натуральном исчислении, т. Автор опирается на современные данные, относящиеся к интуиционистской логике. МЫ. СИ, которая позволила отработать эти процедуры и алгоритм поиска вывода в целом в дальнейшем предстоит полностью реализовать данный алгоритм на вычислительных машинах. Практическая значимость исследования. Результаты исследования могут быть использованы в дальнейших разработках алгоритмов, как для интуиционистской логики предикатов, так и для иных логик они могут быть использованы также в научнонсслсдоватсльской работе как инструмент для проверки утверждений интуиционистской логики. Большое значение имеют полученные результаты и в педагогической практике при чтении курсов по интуиционистской логике И компьютерно 1КС. Апробация работы состоялась в ходе обсуждения результатов исследования на кафедре логики философского факультета МГУ им. М.В. Ломоносова. Результаты диссертационного исследования нашли также свое отражение в 4 научных работах автора и обсуждались на 5ой Общероссийской научной конференции Современная логика проблемы теории, истории и применения в науке СПб, , 3их Смирновских пениях по логике Москва, и на философском факультете университета Росток, Германия. Структура диссертации. Диссертация состоит из введения, 4 глав, заключения, приложения и библиографии. Автор диссертации выражает глубокую благодарность своим родителям Макарову В. А. и Макаровой . . за терпение и поддержку во время написания диссертации, профессору Бочарову В. А. за долголетнее научное руководство, плодотворные обсуждения исследовательских проблем, отзывчивость И внимательность, оказанные во время совместной работы, а также сотрудникам и аспирантам кафедры логики МГУ им. М.В. Ломоносова и сектора логики Института философии РАН за дружеское участие и оказанную помощь в подготовке диссертации.