Completing the Picture: Complexity of the Ackermann Fragment

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 \({\rm 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 \({\rm NExpTime}\)-hardness.

Daumantas Kojelis
Download Paper