Completing the Picture: Complexity of the Ackermann Fragment

Daumantas Kojelis

doi:10.21942/uva.20368233.v2

Completing the Picture: Complexity of the Ackermann Fragment

Daumantas Kojelis

Department of Computer Science

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

We give a decision procedure for the satisfiability problem of the Ackermann fragment with equality, when the number of trailing existential quantifiers is bounded by some fixed integer m, and thus establish an ExpTime upper-bound. Taking the work of R. Jaakkoa into account, we conclude that any Ackermann (sub-)fragment must feature at least two leading as well as an unbounded number of trailing existential quantifiers to retain NExpTime-hardness.

Original language	English
Title of host publication	33RD EUROPEAN SUMMER SCHOOL IN LOGIC, LANGUAGE AND INFORMATION
DOIs	https://doi.org/10.21942/uva.20368233.v2
Publication status	Published - 25 Jul 2022

Access to Document

10.21942/uva.20368233.v2

Cite this

@inproceedings{d1a0011ed38348a6b524184a20e09674,

title = "Completing the Picture: Complexity of the Ackermann Fragment",

abstract = "We give a decision procedure for the satisfiability problem of the Ackermann fragment with equality, when the number of trailing existential quantifiers is bounded by some fixed integer m, and thus establish an ExpTime upper-bound. Taking the work of R. Jaakkoa into account, we conclude that any Ackermann (sub-)fragment must feature at least two leading as well as an unbounded number of trailing existential quantifiers to retain NExpTime-hardness.",

author = "Daumantas Kojelis",

year = "2022",

month = jul,

day = "25",

doi = "10.21942/uva.20368233.v2",

language = "English",

booktitle = "33RD EUROPEAN SUMMER SCHOOL IN LOGIC, LANGUAGE AND INFORMATION",

}

TY - GEN

T1 - Completing the Picture: Complexity of the Ackermann Fragment

AU - Kojelis, Daumantas

PY - 2022/7/25

Y1 - 2022/7/25

N2 - We give a decision procedure for the satisfiability problem of the Ackermann fragment with equality, when the number of trailing existential quantifiers is bounded by some fixed integer m, and thus establish an ExpTime upper-bound. Taking the work of R. Jaakkoa into account, we conclude that any Ackermann (sub-)fragment must feature at least two leading as well as an unbounded number of trailing existential quantifiers to retain NExpTime-hardness.

AB - We give a decision procedure for the satisfiability problem of the Ackermann fragment with equality, when the number of trailing existential quantifiers is bounded by some fixed integer m, and thus establish an ExpTime upper-bound. Taking the work of R. Jaakkoa into account, we conclude that any Ackermann (sub-)fragment must feature at least two leading as well as an unbounded number of trailing existential quantifiers to retain NExpTime-hardness.

U2 - 10.21942/uva.20368233.v2

DO - 10.21942/uva.20368233.v2

M3 - Conference contribution

BT - 33RD EUROPEAN SUMMER SCHOOL IN LOGIC, LANGUAGE AND INFORMATION

ER -

Completing the Picture: Complexity of the Ackermann Fragment

Abstract

Access to Document

Fingerprint

Cite this