Complexity of the Ackermann fragment with one leading existential quantifier

Abstract

In this short note we prove that the satisfiability problem of the Ackermann fragment with one leading existential quantifier is ExpTime-complete.

arXiv commentMajor revision. The alternating procedure that was presented in the previous version was not sound and hence accepted sentences which were not satisfiable. The problem present in the previous version is now fixed, but the resulting proof is more involved. The presentation has been improved significantly