PhD Application Talk: An investigation of the proofs complexities in the systems of non- classical logics

The following proof systems are compared in the dissertation: Frege systems, sequence systems with and without cut rule, resolution system, natural deduction system.
Main results of the work are:
On the basis of the ö–descriptive set of literals and ö–descriptive disjunctive normal forms, polynomial equivalence of resolution and cut free sequent system for intuitionistic and minimal logic is proved.
By analogy with the description of intuitionistic Frege systems, minimal Frege systems are described based on the formal system ARm, which generates all the derivative rules of minimal logic. That system allows to prove polynomial equivalency of all minimal Frege systems, as well as the polynomial equivalency of them to the system of natural deduction and sequent system with cut rule for minimal logic.
It is proved that each of the examined proof system of classical logic has exponential speed-up over the same name system of intuitionistic logic, and the proof system of intuitionistic logic has exponential speed-up over the same name system of minimal logic.
Based on the well–known results as well as on the results obtained in the dissertation a hierarchy of different proof systems of classical and non-classical logics is constructed.