Поиск доказательств в натуральном интуиционистском исчислении предикатов с $\varepsilon$- символом и предикатом существования.

##plugins.themes.bootstrap3.article.main##

A .V . Smirnov

Abstract

Существуют два типа систем натурального вывода: с прямым и непрямым правилом удаления квантора существования. Прямое правило удаления квантора существования формулируется с использованием языка с эпсилон-символом. Классическое исчисление предикатов с прямым правилом удаления квантора существования элегантно и является хорошей основой для организации систематической процедуры поиска доказательств. Мною была предложена процедура поиска доказательств для классического исчисления предикатов с прямым правилом удаления квантора существования [7]. А.В. Смирнов и А.Е. Новодворский [3] реализовали ее на компьютере. Хотелось бы построить интуиционистское исчисление предикатов с прямым правилом удаления квантора существования и на этой основе сформулировать алгоритм поиска доказательств.

##plugins.generic.usageStats.downloads##

##plugins.generic.usageStats.noStats##

##plugins.themes.bootstrap3.article.details##

Section
Papers

References

Драгалин А.Г.. Интуиционистская логика и е-символ Гильберта.// История и методология естественных наук. М.,МГУ,1979.
Клини С.К.. Перестановочность применений правил в генценовских исчислениях LK и LI.// Математическая теория логического вывода. М., Наука, 1967.
Смирнов А.В., Новодворский А.Е.. Язык описания логических систем.//Логические исследования вып.З, М.1995.
Смирнов А.В.. Система интерактивного доказательства теорем.// Логические исследования вып.2, М., Наука, 1993.
Смирнов В.А.. Формальный вывод и логические исчисления.М., Наука, 1972.
Smirnov VA.. Theory of Quantification and e-calculi// Essays on mathematical and philosophical logic. Synthese Library vol.122, D. Reidel P.C.1979.
Смирнов В.А.. Поиск доказательств// Логика и компьютер.М., Наука, 1990.

##plugins.generic.recommendByAuthor.heading##