Comparison of several proof systems of intuitionistic propositional logic

Построен некий фрагмент иерархии по сложности выводов одних и тех же формул для ряда традиционных систем доказательств интуиционистской логики: системы резолюций, а также натуральных, гильбертовских и секвенциальных. Полученные соотношения идентичны соотношениям между одноименными системами классической логики.