On Proof Complexity of Some Type of Tautologies

Authors

  • Vahagn N. Altunyan Yerevan State University
  • Garik V. Petrosyan Yerevan State University

DOI:

https://doi.org/10.51408/1963-0080

Keywords:

Frege systems, Tautology, Sign-alternating tree, Proof complexity

Abstract

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.

References

A. Cook and A.R. Reckhow, “The relative efficiency of propositional proof systems", Journal of Symbolic logic, vol. 44, pp. 36-50, 1979.

L. Strasburger, “Extension without Cut", Annals of Pure and Applied Logic, vol. 163, no. 12, pp. 1995-2007, 2012.

A.A. Chubaryan and G.V. Petrosyan, “Some notes on proof complexities in Frege systems", Sciences of Europe, vol 1. #12 (12), Physics and Mathematics, pp. 31-34, 2017.

J. Nordstrom, “Narrow proofs maybe spacious: Separating space and width in resolution", SIAM Journal on Computing, vol. 39, no. 1, pp. 59-121, 2019.

Downloads

Published

2021-12-14

How to Cite

Altunyan, V. N., & Petrosyan, G. V. (2021). On Proof Complexity of Some Type of Tautologies. Mathematical Problems of Computer Science, 56, 65–72. https://doi.org/10.51408/1963-0080