Geodesic
On normal deduction proofs in intuitionistic natural predicate calculus
Trudy Instituta matematiki i mehaniki, Trudy Instituta Matematiki i Mekhaniki UrO RAN, Tome 30 (2024) no. 4, pp. 188-206 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

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. 
@article{TIMM_2024_30_4_a14,
     author = {O. A. Okhotnikov},
     title = {On normal deduction proofs in intuitionistic natural predicate calculus},
     journal = {Trudy Instituta matematiki i mehaniki},
     pages = {188--206},
     year = {2024},
     volume = {30},
     number = {4},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/TIMM_2024_30_4_a14/}
}
TY  - JOUR
AU  - O. A. Okhotnikov
TI  - On normal deduction proofs in intuitionistic natural predicate calculus
JO  - Trudy Instituta matematiki i mehaniki
PY  - 2024
SP  - 188
EP  - 206
VL  - 30
IS  - 4
UR  - http://geodesic.mathdoc.fr/item/TIMM_2024_30_4_a14/
LA  - ru
ID  - TIMM_2024_30_4_a14
ER  - 
%0 Journal Article
%A O. A. Okhotnikov
%T On normal deduction proofs in intuitionistic natural predicate calculus
%J Trudy Instituta matematiki i mehaniki
%D 2024
%P 188-206
%V 30
%N 4
%U http://geodesic.mathdoc.fr/item/TIMM_2024_30_4_a14/
%G ru
%F TIMM_2024_30_4_a14
O. A. Okhotnikov. On normal deduction proofs in intuitionistic natural predicate calculus. Trudy Instituta matematiki i mehaniki, Trudy Instituta Matematiki i Mekhaniki UrO RAN, Tome 30 (2024) no. 4, pp. 188-206. http://geodesic.mathdoc.fr/item/TIMM_2024_30_4_a14/

[1] Smirnov V.A., Logicheskie metody analiza nauchnogo znaniya, Editorial URSS, M., 2002, 220 pp.

[2] Smirnov V.A., Markin V.I., Novodvorskii A.E., Smirnov A.V., Dokazatelstvo i ego poisk. Kurs logiki i kompyuternyi praktikum, Logika i kompyuter, no. 3, Nauka, M., 1996, 254 pp.

[3] Troelstra A., Schwichtenberg H., Basic proof theory, Second Edt., Cambridge Univ. Press, Cambridge, 2000, 417 pp. | DOI | MR | Zbl

[4] Pelletier F.J. and Hazen A., “Natural deduction systems in logic”, The Stanford Encyclopedia of Philosophy, 2021

[5] Vtorushin Yu.I., “O poiske vyvoda v sisteme naturalnoi deduktsii logiki predikatov”, Intellektualnye sistemy, 13 (2009), 263–288 | MR

[6] Portoraro F., “Automated Reasoning”, The Stanford Encyclopedia of Philosophy, 2024

[7] Negri S., von Plato J., Structural proof theory, Cambridge University Press, Cambridge, 2001, 274 pp. | DOI | MR | Zbl

[8] Negri S., von Plato J., Proof analysis. A Contribution to Hilbert's last problem, Cambridge University Press, Cambridge, 2011, 278 pp. | DOI | MR

[9] Thiele R., “Hilbert's twenty-fourth problem”, American Mathematical Monthly, 110:1 (2003), 1–24 | DOI | MR | Zbl

[10] Sieg W., Byrnes J., “Normal natural deduction proofs (in classical logic)”, Studia Logica, 60:1 (1998), 67–106 | DOI | MR | Zbl

[11] Sieg W., Cittadini S., “Normal natural deduction proofs (in non-classical logic)”, Mechanizing Mathematical Resoning, Ser. Springer Lecture Notes in Artificial Intelligence, 2605, 2005, 169–191 | DOI | MR | Zbl

[12] Serebryannikov O.F., “Normalnye formy logicheskikh dokazatelstv i problemy teoreticheskoi evristiki”, Voprosy gnoseologii, logiki i metodologii nauchnogo issledovaniya, no. 3, Leningrad, 1972, 89–106

[13] Pravits D., Naturalnyi vyvod, LORI, M., 1997, 108 pp.

[14] Serebryannikov O.F., “Normalnye formy logicheskikh dokazatelstv”, Logicheskii vyvod, Nauka, M., 1979, 267–273 | MR

[15] Okhotnikov O., “About proof-search in intuitionistic natural deduction calculus using partial Skolemization”, J. Phys.: Conf. Ser, 1680 (2020), 012038, 1–7 | DOI

[16] Okhotnikov O., “A new sequent calculus for automated proof search”, Appl. Math. Sci., 8:100 (2014), 4977–4984 | DOI

[17] Dopolnitelnye materialy k state: O. A. Okhotnikov “O normalnykh vyvodakh v intuitsionistskom naturalnom ischislenii predikatov”, Onlain-versiya soderzhit dopolnitelnye materialy (PDF), URL: http://journal.imm.uran.ru/sites/default/files/content/30_4/Suppl_inf_2024-v.30-4_proof.pdf