Skip to main content
SpringerLink
Log in

Complexity of Deep Inference via Atomic Flows

  • Conference paper
Book cover How the World Computes (CiE 2012)

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

Included in the following conference series:

Abstract

We consider the fragment of deep inference free of compression mechanisms and compare its proof complexity to other systems, utilising ‘atomic flows’ to examine size of proofs. Results include a simulation of Resolution and dag-like cut-free Gentzen, as well as a separation from bounded-depth Frege.

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. Brünnler, K., Tiu, A.F.: A local system for classical logic (2001); preprint (WV-01-02) (2001)

    Google Scholar 

  2. Bruscoli, P., Guglielmi, A.: On the proof complexity of deep inference. ACM Transactions on Computational Logic 10(2), article 14, 1–34 (2009)

    Article  MathSciNet  Google Scholar 

  3. Bruscoli, P., Guglielmi, A., Gundersen, T., Parigot, M.: Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae (2009) (submitted)

    Google Scholar 

  4. Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic 52(4), 916–927 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  5. Clote, P., Kranakis, E.: Boolean Functions and Computation Models. Springer (2002)

    Google Scholar 

  6. D’Agostino, M.: Are tableaux an improvement on truth-tables? Journal of Logic, Language and Information 1, 235–252 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. Das, A.: On the Proof Complexity of Cut-Free Bounded Deep Inference. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 134–148. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Das, A.: Complexity of deep inference via atomic flows (2012)(preprint)

    Google Scholar 

  9. Guglielmi, A.: Resolution in the calculus of structures (2003) (preprint)

    Google Scholar 

  10. Guglielmi, A., Gundersen, T.: Normalisation control in deep inference via atomic flows II (2008) (preprint)

    Google Scholar 

  11. Gundersen, T.: A General View of Normalisation Through Atomic Flows. Ph.D. thesis, University of Bath (2009)

    Google Scholar 

  12. Jeřábek, E.: Proof complexity of the cut-free calculus of structures. Journal of Logic and Computation 19(2), 323–339 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  13. Krajíček, J.: On the weak pigeonhole principle (2001)

    Google Scholar 

  14. 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  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  16. Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Bath, Claverton Down, BA2 7AY, United Kingdom

    Anupam Das

Authors
  1. Anupam Das
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Mathematics, University of Leeds, LS2 9JT, Leeds, UK

    S. Barry Cooper

  2. Computer Laboratory, University of Cambridge, Willialm Gates Building, J.J. Thomson Avenue, CB3 0FD, Cambridge, UK

    Anuj Dawar

  3. Institute for Logic, Language and Computation, University of Amsterdam, 1090 GE, Amsterdam, The Netherlands

    Benedikt Löwe

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Das, A. (2012). Complexity of Deep Inference via Atomic Flows. In: Cooper, S.B., Dawar, A., Löwe, B. (eds) How the World Computes. CiE 2012. Lecture Notes in Computer Science, vol 7318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30870-3_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-30870-3_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-30869-7

  • Online ISBN: 978-3-642-30870-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation