УДК 510.66
MSC: 03F03, 03F05, 03F07
DOI: 10.21538/0134-4889-2024-30-4-188-206
Онлайн-версия статьи содержит дополнительные материалы
Построенная в статье теория включает формулировку двух натуральных исчислений предикатов первого порядка: интуиционистского и минимального. Для этих двух видов логики в статье определяется новое понятие нормального натурального вывода. Доказывается теорема о нормализации натуральных выводов в этих исчислениях.
Ключевые слова: система натуральной дедукции, интуиционистское натуральное исчисление предикатов, нормальный натуральный вывод, автоматическое доказательство теорем, поиск натурального логического вывода
СПИСОК ЛИТЕРАТУРЫ
1. Смирнов В.А. Логические методы анализа научного знания. М.: Эдиториал УРСС, 2002. 220 с.
2. Смирнов В.А., Маркин В.И., Новодворский А.Е., Смирнов А.В. Доказателство и его поиск. Курс логики и компьютерный практикум // Логика и компьютер. Вып. 3. М.: Наука, 1996. 254 с.
3. Troelstra A., Schwichtenberg H. Basic proof theory. Second Edt. Cambridge: Cambridge Univ. Press, 2000. 417 p. doi: 10.1017/CBO9781139168717
4. Pelletier F.J. and Hazen A. Natural deduction systems in logic // The Stanford Encyclopedia of Philosophy. 2021.
5. Вторушин Ю.И. О поиске вывода в системе натуральной дедукции логики предикатов // Интеллектуальные системы. 2009. Т. 13. С. 263–288.
6. Portoraro F. Automated Reasoning // The Stanford Encyclopedia of Philosophy. 2024.
7. Negri S., von Plato J. Structural proof theory. Cambridge: Cambridge University Press, 2001. 274 p. doi: 10.1017/CBO9780511527340
8. Negri S., von Plato J. Proof analysis. A Contribution to Hilbert’s last problem. Cambridge: Cambridge University Press, 2011. 278 p. doi: 10.1017/CBO9781139003513
9. Thiele R. Hilbert’s twenty-fourth problem // American Mathematical Monthly. Vol. 110, no. 1. P. 1–24. 2003. doi: 10.1080/00029890.2003.11919933
10. Sieg W., Byrnes J. Normal natural deduction proofs (in classical logic) // Studia Logica. Vol. 60, no. 1. 1998. P. 67–106. doi: 10.1023/A:1005091418752
11. Sieg W., Cittadini S. Normal natural deduction proofs (in non-classical logic) // Mechanizing Mathematical Resoning. 2005. P. 169–191. (Ser. Springer Lecture Notes in Artificial Intelligence; vol. 2605). doi: 10.1007/978-3-540-32254-2_11
12. Серебрянников О.Ф. Нормальные формы логических доказательств и проблемы теоретической эвристики // Вопросы гносеологии, логики и методологии научного исследования. Вып. 3. Ленинград, 1972. С. 89–106.
13. Правиц Д. Натуральный вывод. М.: ЛОРИ, 1997. 108 с.
14. Серебрянников О.Ф. Нормальные формы логических доказательств // Логический вывод. М.: Наука, 1979. С. 267–273.
15. Okhotnikov O. About proof-search in intuitionistic natural deduction calculus using partial Skolemization // J. Phys.: Conf. Ser. 2020. Vol. 1680. Art. 012038. P. 1–7. doi: 10.1088/1742-6596/1680/1/012038
16. Okhotnikov O. A new sequent calculus for automated proof search // Appl. Math. Sci. 2014. Vol. 8, no. 100. P. 4977–4984. doi: 10.12988/ams.2014.46497
17. Дополнительные материалы к статье: О. А. Охотников “О нормальных выводах в интуиционистском натуральном исчислении предикатов”. Онлайн-версия содержит дополнительные материалы (см. PDF) .
Поступила 20.09.2024
После доработки 15.10.2024
Принята к публикации 21.10.2024
Охотников Олег Алиевич
старший преподаватель
Уральский федеральный университет
г. Екатеринбург
e-mail: oleg.okhotnikov@gmail.com
Ссылка на статью: О.А. Охотников. О нормальных выводах в интуиционистском натуральном исчислении предикатов //Тр. Ин-та математики и механики УрО РАН. 2024. Т. 30, № 4. С. 188-206
English
O.A. Okhotnikov. On normal deduction proofs in intuitionistic natural predicate calculus
The theory constructed in the article includes the formulation of two natural first-order predicate calculi: intuitionistic and minimal. For these two types of logic, the article defines a new notion of normal natural deduction. A theorem on the normalization of natural deductions in these calculi is proved.
Keywords: system of natural deduction, intuitionistic natural predicate calculus, normal natural deduction, automated theorem proving, search for a natural logical proof.
Received September 20, 2024
Revised October 15, 2024
Accepted October 21, 2024
Oleg Alievich Okhotnikov, Ural Federal University, Yekaterinburg, 620000 Russia, e-mail: oleg.okhotnikov@gmail.com
Cite this article as: O.A. Okhotnikov. On normal deduction proofs in intuitionistic natural predicate calculus. Trudy Instituta Matematiki i Mekhaniki UrO RAN, 2024, vol. 30, no. 4, pp. 188–206.
[References -> on the "English" button bottom right]
