Top

Published in:

2018 | OriginalPaper | Chapter

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

Author : Anupam Das

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Efficient Model Construction for Horn Logic with VLog

next chapter Checking Array Bounds by Abstract Interpretation and Symbolic Expressions

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

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

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

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

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.

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

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

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)

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

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

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_26CrossRef

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

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

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

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

10.

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

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_14CrossRef

12.

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

13.

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

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

15.

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

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)

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)MathSciNetCrossRef

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)

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_19CrossRefMATH

20.

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

21.

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

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)

23.

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

24.

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

25.

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

26.

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

Title: Focussing, and the Polynomial Hierarchy
Author: Anupam Das
Publisher: Springer International Publishing
Book: Automated Reasoning
Print ISBN: 978-3-319-94204-9

Electronic ISBN: 978-3-319-94205-6

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-94205-6_45

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner