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^*

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Citation (Scopus)

211 Downloads (Pure)

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:
Subtitle of host publication	9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Editors	Roberto Sebastiani, Didier Galmiche, Stephan Schulz
Publisher	Springer
Pages	689-705
ISBN (Electronic)	9783319942056
ISBN (Print)	9783319942049
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, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: 14 Jul 2018 → 17 Jul 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10900 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/Territory	United Kingdom
City	Oxford
Period	14/07/18 → 17/07/18

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-94205-6_45Licence: None: All rights reserved

Das_Focussing_MALL_and_the_Polynomial_Hierarchy_IJCAR_2018Accepted author manuscript, 395 KBLicence: None: All rights reserved

https://link.springer.com/chapter/10.1007%2F978-3-319-94205-6_45Licence: None: All rights reserved

Cite this

Das, A. (2018). Focussing, MALL and the Polynomial Hierarchy. In R. Sebastiani, D. Galmiche, & S. Schulz (Eds.), Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 689-705). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10900 LNAI). Springer. https://doi.org/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, Proceedings. editor / Roberto Sebastiani ; Didier Galmiche ; Stephan Schulz. Springer, 2018. pp. 689-705 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{aae830d3eb1e4c118558c3dc95daf881,

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 = "9783319942049",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "689--705",

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

booktitle = "Automated Reasoning:",

note = "9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 14-07-2018 Through 17-07-2018",

}

Das, A 2018, Focussing, MALL and the Polynomial Hierarchy. in R Sebastiani, D Galmiche & S Schulz (eds), Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10900 LNAI, Springer, pp. 689-705, 9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 14/07/18. 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, Proceedings. ed. / Roberto Sebastiani; Didier Galmiche; Stephan Schulz. Springer, 2018. p. 689-705 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10900 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

UR - http://www.scopus.com/inward/record.url?scp=85049956770&partnerID=8YFLogxK

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

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

M3 - Conference contribution

AN - SCOPUS:85049956770

SN - 9783319942049

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 689

EP - 705

BT - Automated Reasoning:

A2 - Sebastiani, Roberto

A2 - Galmiche, Didier

A2 - Schulz, Stephan

PB - Springer

T2 - 9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018

Y2 - 14 July 2018 through 17 July 2018

ER -

Das A. Focussing, MALL and the Polynomial Hierarchy. In Sebastiani R, Galmiche D, Schulz S, editors, Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer. 2018. p. 689-705. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-94205-6_45

Focussing, MALL and the Polynomial Hierarchy

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this