Abstract:
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.
Fulltext:
PDF file (273 kB)