Skip to main content
SpringerLink
Log in

Algebraic Proofs over Noncommutative Formulas

  • Conference paper
Theory and Applications of Models of Computation (TAMC 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6108))

  • 777 Accesses

Abstract

We study possible formulations of algebraic propositional proofs operating with noncommutative polynomials written as algebraic noncommutative formulas. First, we observe that a simple formulation of such proof systems gives rise to systems at least as strong as Frege—yielding also a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic variant of Frege proofs, different from that given before in [8,11]. We then turn to an apparently weaker system, namely, Polynomial Calculus (PC) where polynomials are written as ordered formulas (PC over ordered formulas, for short). This is an algebraic propositional proof system that operates with noncommutative polynomials in which the order of products in all monomials respects a fixed linear ordering on the variables, and where proof-lines are written as noncommutative formulas. We show that the latter proof system is strictly stronger than resolution, polynomial calculus and polynomial calculus with resolution (PCR) and admits polynomial-size refutations for the pigeonhole principle and the Tseitin’s formulas. We conclude by proposing an approach for establishing lower bounds on PC over ordered formulas proofs, and related systems, based on properties of lower bounds on noncommutative formulas.

The motivation behind this work is developing techniques incorporating rank arguments (similar to those used in algebraic circuit complexity) for establishing lower bounds on propositional proofs.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ajtai, M.: The complexity of the pigeonhole principle. In: Proceedings of the IEEE 29th Ann. Symp. on Found. of Comp. Sci, pp. 346–355 (1988)

    Google Scholar 

  2. Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Space complexity in propositional calculus. SIAM J. Comput. 31(4), 1184–1211 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  3. Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Pseudorandom generators in propositional proof complexity. SIAM J. Comput. 34(1), 67–88 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  4. Atserias, A., Galesi, N., Pudlák, P.: Monotone simulations of non-monotone proofs. J. Comput. System Sci. 65(4), 626–638 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  5. Atserias, A., Kolaitis, P.G., Vardi, M.Y.: Constraint propagation as a proof system. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 77–91. Springer, Heidelberg (2004)

    Google Scholar 

  6. Ben-Sasson, E., Impagliazzo, R.: Random CNF’s are hard for the polynomial calculus. In: Proceedings of the IEEE 40th Annual Symposium on Foundations of Computer Science, New York, pp. 415–421. IEEE, Los Alamitos (1999)

    Google Scholar 

  7. Buss, S.R., Grigoriev, D., Impagliazzo, R., Pitassi, T.: Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. System Sci. 62(2), 267–289 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  8. Buss, S.R., Impagliazzo, R., Krajíček, J., Pudlák, P., Razborov, A.A., Sgall, J.: Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Comput. Complex. 6(3), 256–298 (1996/1997)

    Google Scholar 

  9. Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proceedings of the 28th Ann. ACM Symp. on the Theory of Comput, pp. 174–183 (1996)

    Google Scholar 

  10. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic 44(1), 36–50 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  11. Grigoriev, D., Hirsch, E.A.: Algebraic proof systems over formulas. Theoret. Comput. Sci. 303(1), 83–102 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  12. Krajíček, J.: An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. J. Symbolic Logic 73(1), 227–237 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  13. Krajíček, J., Pudlák, P., Woods, A.: An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures Algorithms 7(1), 15–39 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  14. Nisan, N.: Lower bounds for non-commutative computation. In: Proceedings of the 23th Annual ACM Symposium on the Theory of Computing, pp. 410–418 (1991)

    Google Scholar 

  15. Pitassi, T.: Algebraic propositional proof systems. In: Descriptive complexity and finite models. DIMACS Ser. Discrete Math. Theoret. Comput. Sci, vol. 31, pp. 215–244. AMS, Providence (1997)

    Google Scholar 

  16. Pitassi, T., Beame, P., Impagliazzo, R.: Exponential lower bounds for the pigeonhole principle. Comput. Complexity 3(2), 97–140 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  17. Pudlák, P.: On the complexity of the propositional calculus. In: Sets and proofs. London Math. Soc. Lecture Note Ser., vol. 258, pp. 197–218. Cambridge Univ. Press, Cambridge (Leeds 1997)

    Google Scholar 

  18. Raz, R.: Separation of multilinear circuit and formula size. Theory of Computing 2, article 6 (2006)

    Google Scholar 

  19. Raz, R.: Multi-linear formulas for permanent and determinant are of super-polynomial size. J. ACM 56(2) (2009)

    Google Scholar 

  20. Raz, R., Shpilka, A.: Deterministic polynomial identity testing in non commutative models. Computational Complexity 14(1), 1–19 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  21. Raz, R., Tzameret, I.: Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Logic 155(3), 194–224 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  22. Raz, R., Tzameret, I.: The strength of multilinear proofs. Computational Complexity 17(3), 407–457 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  23. Segerlind, N.: Nearly-exponential size lower bounds for symbolic quantifier elimination algorithms and OBDD-based proofs of unsatisfiability. Electronic Colloquium on Computational Complexity, TR07-009 (January 2007)

    Google Scholar 

  24. Tzameret, I.: Studies in Algebraic and Propsitional Proof Complexity. PhD thesis, Tel Aviv University (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematical Institute, Academy of Sciences of the Czech Republic, Žitná 25, 115 67, Prague 1, Czech Rep.

    Iddo Tzameret

Authors
  1. Iddo Tzameret
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Charles University, Malostranske nam 25, 11800, Praha 1, Czech Republic

    Jan Kratochvíl , Jiří Fiala  & Petr Kolman ,  & 

  2. State Key Lab. of Computer Science, Institute of Software,, Chinese Academy of Sciences, 100190, Beijing, P.R. China

    Angsheng Li

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tzameret, I. (2010). Algebraic Proofs over Noncommutative Formulas. In: Kratochvíl, J., Li, A., Fiala, J., Kolman, P. (eds) Theory and Applications of Models of Computation. TAMC 2010. Lecture Notes in Computer Science, vol 6108. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13562-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13562-0_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13561-3

  • Online ISBN: 978-3-642-13562-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation