On Sizes of Linear and Tree-Like Proofs for any Formulae Families in Some Systems of Propositional Calculus
DOI:
https://doi.org/10.51408/1963-0086Keywords:
The varieties of propositional sequent systems, The generalization splitting system, The proof size and number of proof steps, Exponential speed-upAbstract
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.
References
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.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2022 Levon A. Apinyan, Anahit A. Chubaryan
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
