Focussing, MALL and the Polynomial Hierarchy

Anupam Das

doi:10.1007/978-3-319-94205-6_45

Focussing, MALL and the Polynomial Hierarchy

Anupam Das

1 Citation (Scopus)

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 MALL_w (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 MALL_w complete for each level of the polynomial hierarchy. This refines the well-known result that MALL_w is PSPACE-complete.

Original language	English
Title of host publication	Automated reasoning : 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings
Editors	Didier Galmiche, Stephan Schulz, Roberto Sebastiani
Publisher	Springer
Publication date	30 Jun 2018
Pages	689-705
Chapter	45
ISBN (Print)	978-3-319-94204-9
ISBN (Electronic)	978-3-319-94205-6
DOIs	https://doi.org/10.1007/978-3-319-94205-6_45
Publication status	Published - 30 Jun 2018
Event	9th International Joint Conference on Automated Reasoning - Oxford, United Kingdom Duration: 14 Jul 2018 → 17 Jul 2018

Conference

Conference	9th International Joint Conference on Automated Reasoning
Country/Territory	United Kingdom
City	Oxford
Period	14/07/2018 → 17/07/2018

Series	Lecture Notes in Computer Science
Volume	10900
ISSN	0302-9743

Access to Document

10.1007/978-3-319-94205-6_45

Cite this

Das, A. (2018). Focussing, MALL and the Polynomial Hierarchy. In D. Galmiche, S. Schulz, & R. Sebastiani (Eds.), Automated reasoning: 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings (pp. 689-705). Springer. Lecture Notes in Computer Science Vol. 10900 https://doi.org/10.1007/978-3-319-94205-6_45

Focussing, MALL and the Polynomial Hierarchy. / Das, Anupam.

Automated reasoning: 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings. ed. / Didier Galmiche; Stephan Schulz; Roberto Sebastiani. Springer, 2018. p. 689-705 (Lecture Notes in Computer Science, Vol. 10900).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Das, A 2018, Focussing, MALL and the Polynomial Hierarchy. in D Galmiche, S Schulz & R Sebastiani (eds), Automated reasoning: 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings. Springer, Lecture Notes in Computer Science, vol. 10900, pp. 689-705, 9th International Joint Conference on
Automated Reasoning, Oxford, United Kingdom, 14/07/2018. https://doi.org/10.1007/978-3-319-94205-6_45

Das A. Focussing, MALL and the Polynomial Hierarchy. In Galmiche D, Schulz S, Sebastiani R, editors, Automated reasoning: 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings. Springer. 2018. p. 689-705. (Lecture Notes in Computer Science, Vol. 10900). doi: 10.1007/978-3-319-94205-6_45

Das, Anupam. / Focussing, MALL and the Polynomial Hierarchy. Automated reasoning: 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings. editor / Didier Galmiche ; Stephan Schulz ; Roberto Sebastiani. Springer, 2018. pp. 689-705 (Lecture Notes in Computer Science, Vol. 10900).

@inproceedings{661882da789e429da2aaab6a2b460eee,

title = "Focussing, MALL and the Polynomial Hierarchy",

abstract = "We investigate how to extract alternating time bounds from {\textquoteleft}focussed{\textquoteright} 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 MALLw (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 MALLw complete for each level of the polynomial hierarchy. This refines the well-known result that MALLw is PSPACE-complete.",

author = "Anupam Das",

year = "2018",

month = jun,

day = "30",

doi = "10.1007/978-3-319-94205-6_45",

language = "English",

isbn = "978-3-319-94204-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "689--705",

editor = "Galmiche, {Didier } and Schulz, {Stephan } and Roberto Sebastiani",

booktitle = "Automated reasoning",

note = "9th International Joint Conference on<br/>Automated Reasoning ; Conference date: 14-07-2018 Through 17-07-2018",

}

TY - GEN

T1 - Focussing, MALL and the Polynomial Hierarchy

AU - Das, Anupam

PY - 2018/6/30

Y1 - 2018/6/30

N2 - 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 MALLw (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 MALLw complete for each level of the polynomial hierarchy. This refines the well-known result that MALLw is PSPACE-complete.

AB - 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 MALLw (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 MALLw complete for each level of the polynomial hierarchy. This refines the well-known result that MALLw is PSPACE-complete.

U2 - 10.1007/978-3-319-94205-6_45

DO - 10.1007/978-3-319-94205-6_45

M3 - Article in proceedings

SN - 978-3-319-94204-9

T3 - Lecture Notes in Computer Science

SP - 689

EP - 705

BT - Automated reasoning

A2 - Galmiche, Didier

A2 - Schulz, Stephan

A2 - Sebastiani, Roberto

PB - Springer

T2 - 9th International Joint Conference on<br/>Automated Reasoning

Y2 - 14 July 2018 through 17 July 2018

ER -

Focussing, MALL and the Polynomial Hierarchy

Abstract

Conference

Access to Document

Fingerprint

Cite this