Поиск доказательств в натуральном интуиционистском исчислении предикатов с $\varepsilon$- символом и предикатом существования.
Article Sidebar
Опубликован:
01.11.1995
Main Article Content
Аннотация
Существуют два типа систем натурального вывода: с прямым и непрямым правилом удаления квантора существования. Прямое правило удаления квантора существования формулируется с использованием языка с эпсилон-символом. Классическое исчисление предикатов с прямым правилом удаления квантора существования элегантно и является хорошей основой для организации систематической процедуры поиска доказательств. Мною была предложена процедура поиска доказательств для классического исчисления предикатов с прямым правилом удаления квантора существования [7]. А.В. Смирнов и А.Е. Новодворский [3] реализовали ее на компьютере. Хотелось бы построить интуиционистское исчисление предикатов с прямым правилом удаления квантора существования и на этой основе сформулировать алгоритм поиска доказательств.
Скачивания
Данные скачивания пока не доступны.
Article Details
Как цитировать
Смирнов В. Поиск доказательств в натуральном интуиционистском исчислении предикатов с $\varepsilon$- символом и предикатом существования. // Логические исследования / Logical Investigations. 1995. Т. 3. C. 163-173.
Выпуск
Раздел
Статьи
Литература
Драгалин А.Г.. Интуиционистская логика и е-символ Гильберта.// История и методология естественных наук. М.,МГУ,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.
Клини С.К.. Перестановочность применений правил в генценовских исчислениях 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.