Complexity of the Ackermann fragment with one leading existential quantifier
Logic in Computer Science
2022-02-01 v2
Abstract
In this short note we prove that the satisfiability problem of the Ackermann fragment with one leading existential quantifier is ExpTime-complete.
Cite
@article{arxiv.2111.05388,
title = {Complexity of the Ackermann fragment with one leading existential quantifier},
author = {Reijo Jaakkola},
journal= {arXiv preprint arXiv:2111.05388},
year = {2022}
}
Comments
Major 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