Open AccessOn Proof Complexity of Some Type of Tautologies
Author(s) -
Vahagn N. Altunyan,
Garik V. Petrosyan
Publication year - 2021
Publication title -
mathematical problems of computer science
Language(s) - English
Resource type - Journals
eISSN - 2738-2788
pISSN - 2579-2784
DOI - 10.51408/1963-0080
Subject(s) - proof complexity , mathematics , type (biology) , direct proof , structural proof theory , sign (mathematics) , discrete mathematics , type theory , proof theory , mathematical proof , ecology , mathematical analysis , geometry , biology
In this paper, we investigate the proof complexities of a special type of tautologies, which are described as tautologies consisting of implications and literals. In particular, we prove that the proof of this kind of tautologies can be polynomially reduced to the proof of tautologies consisting of formulas that are described by sign-alternating trees.