Skip to main content
SpringerLink
Log in

Focussing, \(\mathsf {MALL}\) and the Polynomial Hierarchy

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10900))

Included in the following conference series:

Abstract

We investigate how to extract alternating time bounds from ‘focussed’ proofs, treating non-invertible rule phases as nondeterministic computation and invertible rule phases as co-nondeterministic computation. We refine the usual presentation of focussing to account for deterministic computations in proof search, which correspond to invertible rules that do not branch, more faithfully associating phases of focussed proof search to their alternating time complexity.

As our main result, we give a focussed system for \(\mathsf {MALL}\mathsf {w}\) (\(\mathsf {MALL}\) with weakening) with encodings to and from true quantified Boolean formulas (QBFs): in one direction we encode QBF satisfiability and in the other we encode focussed proof search. Moreover we show that the composition of the two encodings preserves quantifier alternation, yielding natural fragments of \(\mathsf {MALL}\mathsf {w}\) complete for each level of the polynomial hierarchy. This refines the well-known result that \(\mathsf {MALL}\mathsf {w}\) is \(\mathbf {PSPACE}\)-complete.

While conducting this research, the author was supported by a Marie Skłodowska-Curie fellowship, ERC project 753431.

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 EPUB and 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

Notes

  1. 1.

    \(\mathsf {MALL}\mathsf {w}\) is also \(\mathbf {PSPACE}\)-complete, a folklore result subsumed by this work.

  2. 2.

    In fact the same phenomenon presents in this work, cf. Fig. 3.

  3. 3.

    Notice that, by definition of satisfaction these two notions coincide for closed QBFs.

  4. 4.

    In fact, quantifier-free Boolean formula evaluation is known to be \(\mathbf {NC}^{1}\)-complete [2].

  5. 5.

    Note that, for the derivations for the innermost quantifier (\(\exists \) or \(\forall \)), the topmost \(R\) or \(\bar{R}\) step of Figs. 3 or 4 (resp.) does not occur.

  6. 6.

    This is actually exemplary of the more general phenomenon that invertible phases of rules are ‘confluent’.

References

  1. Andreoli, J.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)

    Article  MathSciNet  Google Scholar 

  2. Buss, S.R.: The Boolean formula value problem is in ALOGTIME. In: Proceedings of the 19th Annual ACM Symposium on Theory of Computing (STOC) (1987)

    Google Scholar 

  3. Buss, S.R., Iemhoff, R.: The depth of intuitionistic cut free proofs (2003). http://www.phil.uu.nl/~iemhoff/Mijn/Papers/dpthIPC.pdf

  4. Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)

    Article  MathSciNet  Google Scholar 

  5. Chaudhuri, K., Miller, D., Saurin, A.: Canonical sequent proofs via multi-focusing. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) TCS 2008. IIFIP, vol. 273, pp. 383–396. Springer, Boston, MA (2008). https://doi.org/10.1007/978-0-387-09680-3_26

    Chapter  Google Scholar 

  6. Cook, S., Nguyen, P.: Logical Foundations of Proof Complexity, 1st edn. Cambridge University Press, New York (2010)

    Book  Google Scholar 

  7. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)

    Article  MathSciNet  Google Scholar 

  8. Das, A.: Alternating time bounds from variants of focussed proof systems (2017, submitted). http://anupamdas.com/alt-time-bnds-var-foc-sys.pdf

  9. Delande, O., Miller, D., Saurin, A.: Proof and refutation in MALL as a game. Ann. Pure Appl. Logic 161(5), 654–672 (2010)

    Article  MathSciNet  Google Scholar 

  10. Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)

    Article  MathSciNet  Google Scholar 

  11. Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical propositional logics. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 210–225. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61208-4_14

    Chapter  Google Scholar 

  12. Krajíček, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press, New York (1995)

    Book  Google Scholar 

  13. Laurent, O.: A study of polarization in logic. Theses, Université de la Méditerranée - Aix-Marseille II (2002)

    Google Scholar 

  14. Letz, R.: Lemma and model caching in decision procedures for quantified Boolean formulas. In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX) (2002)

    MATH  Google Scholar 

  15. Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410(46), 4747–4768 (2009)

    Article  MathSciNet  Google Scholar 

  16. Lincoln, P., Mitchell, J.C., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. In: 31st Annual Symposium on Foundations of Computer Science (FOCS) (1990)

    Google Scholar 

  17. Lincoln, P., Mitchell, J.C., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. Ann. Pure Appl. Log. 56(1–3), 239–311 (1992)

    Article  MathSciNet  Google Scholar 

  18. Marin, S., Miller, D., Volpe, M.: A focused framework for emulating modal proof systems. In: 11th Conference on Advances in Modal Logic, pp. 469–488 (2016)

    Google Scholar 

  19. Miller, D., Volpe, M.: Focused labeled proof systems for modal logic. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 266–280. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_19

    Chapter  MATH  Google Scholar 

  20. Negri, S., Von Plato, J., Ranta, A.: Structural Proof Theory. Cambridge University Press, Cambridge (2008)

    Google Scholar 

  21. Nigam, V.: Investigating the use of lemmas (2007, preprint)

    Google Scholar 

  22. Ono, H.: Proof-Theoretic Methods in Nonclassical Logic – An Introduction. MSJ Memoirs, vol. 2, pp. 207–254. The Mathematical Society of Japan, Tokyo (1998)

    Google Scholar 

  23. Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Boston (1994)

    MATH  Google Scholar 

  24. Statman, R.: Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 9, 67–72 (1979)

    Article  MathSciNet  Google Scholar 

  25. Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 1–22 (1976)

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

Download references

Acknowledgements

I would like to thank Taus Brock-Nannestad, Kaustuv Chaudhuri, Sonia Marin and Dale Miller for many fruitful discussions about focussing, in particular on the presentation of it herein.

Author information

Authors and Affiliations

  1. University of Copenhagen, Copenhagen, Denmark

    Anupam Das

Authors
  1. Anupam Das
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Anupam Das .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Das, A. (2018). Focussing, \(\mathsf {MALL}\) and the Polynomial Hierarchy. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_45

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_45

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation