Skip to main content
SpringerLink
Log in

The polynomial bounds of proof complexity in Frege systems

  • Published:
Siberian Mathematical Journal Aims and scope Submit manuscript

Abstract

The concept of a determinative set of variables for a propositional formula was introduced by one of the authors, which made it possible to distinguish the set of hard-determinable formulas. The proof complexity of a formula of this sort has exponential lower bounds in some proof systems of classical propositional calculus (cut-free sequent system, resolution system, analytic tableaux, cutting planes, and bounded Frege systems). In this paper we prove that the property of hard-determinability is insufficient for obtaining a superpolynomial lower bound of proof lines (sizes) in Frege systems: an example of a sequence of hard-determinable formulas is given whose proof complexities are polynomially bounded in every Frege system.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Cook S. A. and Reckhow A. R., “The relative efficiency of propositional proof systems,” J. Symbolic Logic, 44, 36–50 (1979).

    Article  MATH  MathSciNet  Google Scholar 

  2. Pudlák P., “The lengths of proofs,” in: Handbook of Proof Theory, North-Holland, Amsterdam, 1998, pp. 547–637.

    Chapter  Google Scholar 

  3. Buss S. R., “Polynomial size proofs of the propositional pigeonhole principle,” J. Symbolic Logic, 52, 916–927 (1987).

    Article  MATH  MathSciNet  Google Scholar 

  4. Razborov A., “Lower bounds for propositional proofs and independence results in bounded arithmetic,” in: Proceedings of the 23rd ICALP, Springer-Verlag, New York; Berlin, 1996, pp. 48–62.

    Google Scholar 

  5. Chubaryan A. A., “On proof complexity in some system of classical propositional logic,” Izv. NAN Armenii Mat., 34, No. 5, 16–26 (1999).

    MATH  MathSciNet  Google Scholar 

  6. Chubaryan A. A., “On proof complexity in several systems of classical propositional calculuses,” Mat. Voprosy Kibernet., 14, pp. 49–56 (2005).

    MATH  Google Scholar 

  7. Chubaryan A. A., “Relative efficiency of a proof system in classical propositional logic,” Izv. NAN Armenii Mat., 37, No. 5, 71–84 (2002).

    MATH  MathSciNet  Google Scholar 

  8. Aleksanyan S. and Chubaryan A., “On some properties of Frege proofs,” in: Proceedings of CSIT-2005, NAN RA, Yerevan, 2005, pp. 45–46.

    Google Scholar 

  9. Aleksanyan S. and Chubaryan A., “On determinative complexity of Frege proofs,” in: XIV International Conference on LPAR, Proceedings of the Short Papers Session, Yerevan, 2007, pp. 5–11.

Download references

Author information

Authors and Affiliations

  1. State Engineering University, Yerevan, Armenia

    S. R. Aleksanyan

  2. Yerevan State University, Yerevan, Armenia

    A. A. Chubaryan

Authors
  1. S. R. Aleksanyan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. A. Chubaryan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to S. R. Aleksanyan.

Additional information

Original Russian Text Copyright © 2009 Aleksanyan S. R. and Chubaryan A. A.

__________

Yerevan. Translated from Sibirskiĭ Matematicheskiĭ Zhurnal, Vol. 50, No. 2, pp. 243–249, March–April, 2009.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Aleksanyan, S.R., Chubaryan, A.A. The polynomial bounds of proof complexity in Frege systems. Sib Math J 50, 193–198 (2009). https://doi.org/10.1007/s11202-009-0022-7

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11202-009-0022-7

Keywords

Search

Navigation