On Sizes of Linear and Tree-Like Proofs for any Formulae Families in Some Systems of Propositional Calculus


  • Levon A. Apinyan Russian-Armenian University
  • Anahit A. Chubaryan Yerevan State University




The varieties of propositional sequent systems, The generalization splitting system, The proof size and number of proof steps, Exponential speed-up


The sizes of linear and tree-like proofs for any formulae families are investigated in some systems of propositional calculus: in different sequent systems (with quantifier rules, with the substitution rule, with the cut rule, without the cut rule, monotone) and in the generalization splitting system. The comparison of results obtained here with the bounds obtained formerly for the steps of proofs for the same formulas in the mentioned systems shows the importance of the size of proof among the other characteristics of proof complexities.


S. A. Cook and A. R. Reckhow, “The relative efficiency of propositional proof systems”, Symbolic Logic, vol. 44, pp. 36-50, 1979.

A. Carbone, “Quantified propositional logic and the number of lines of tree-like proofs”, Studia Logica, vol. 64, pp. 315-321, 2000.

А. A. Тамазян, А. A. Чубарян, “Об отношениях сложностей выводов в ряде систем исчисления высказываний”, Математические вопросы кибернетики и вычислстельной техники, vol. 54, pp. 138-146, 2020.

Ан. А. Чубарян, Арм. А. Чубарян, “Оценки некоторых сложностных характеристик выводов в системе обобщенных расщеплений”, НАУ, Отечественная наука в эпоху изменений: постулаты прошлого и теории нового времени, часть 10, 2(7), стр.11-14, 2015.

Г. Цейтин, Ан. Чубарян, “Некоторые оценки длин логических выводов в классическом исчислении высказываний”, ДАН Арм. ССР, том 55, но.1, стр. 10-12, 1972.




How to Cite

Apinyan, L. A., & Chubaryan, A. A. (2022). On Sizes of Linear and Tree-Like Proofs for any Formulae Families in Some Systems of Propositional Calculus. Mathematical Problems of Computer Science, 57, 47–55. https://doi.org/10.51408/1963-0086