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 Citationer (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.

Originalsprog	Engelsk
Titel	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
Redaktører	Didier Galmiche, Stephan Schulz, Roberto Sebastiani
Forlag	Springer
Publikationsdato	30 jun. 2018
Sider	689-705
Kapitel	45
ISBN (Trykt)	978-3-319-94204-9
ISBN (Elektronisk)	978-3-319-94205-6
DOI	https://doi.org/10.1007/978-3-319-94205-6_45
Status	Udgivet - 30 jun. 2018
Begivenhed	9th International Joint Conference on Automated Reasoning - Oxford, Storbritannien Varighed: 14 jul. 2018 → 17 jul. 2018

Konference

Konference	9th International Joint Conference on Automated Reasoning
Land/Område	Storbritannien
By	Oxford
Periode	14/07/2018 → 17/07/2018

Navn	Lecture Notes in Computer Science
Vol/bind	10900
ISSN	0302-9743

Adgang til dokumentet

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

Citationsformater

Das, A. (2018). Focussing, MALL and the Polynomial Hierarchy. I D. Galmiche, S. Schulz, & R. Sebastiani (red.), 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 (s. 689-705). Springer. Lecture Notes in Computer Science Bind 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. red. / Didier Galmiche; Stephan Schulz; Roberto Sebastiani. Springer, 2018. s. 689-705 (Lecture Notes in Computer Science, Bind 10900).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Das, A 2018, Focussing, MALL and the Polynomial Hierarchy. i D Galmiche, S Schulz & R Sebastiani (red), 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, bind 10900, s. 689-705, 9th International Joint Conference on
Automated Reasoning, Oxford, Storbritannien, 14/07/2018. https://doi.org/10.1007/978-3-319-94205-6_45

Das A. Focussing, MALL and the Polynomial Hierarchy. I Galmiche D, Schulz S, Sebastiani R, red., 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. s. 689-705. (Lecture Notes in Computer Science, Bind 10900). doi: 10.1007/978-3-319-94205-6_45

@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

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater