Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | https://arxiv.org/abs/2602.16410 |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911454384357376 |
|---|---|
| author | Chew, Leroy Janota, Mikoláš Olšák, Miroslav Suda, Martin |
| author_facet | Chew, Leroy Janota, Mikoláš Olšák, Miroslav Suda, Martin |
| contents | In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (Effectively Propositional). While Bernays-Schoenfinkel is NEXPTIME-complete, we already can obtain fragments that are PSPACE-complete by restricting our clauses to DET-HORN or KROM. However such restrictions yield very different formulas to the canonical PSPACE-complete language of Quantified Boolean Formulas (QBF). This is despite Bernays-Schoenfinkel having a natural connection to an extension of QBF known as Dependency QBF. Our main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy. We use this definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_16410 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Reintroducing the Second Player in EPR Chew, Leroy Janota, Mikoláš Olšák, Miroslav Suda, Martin Logic in Computer Science In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (Effectively Propositional). While Bernays-Schoenfinkel is NEXPTIME-complete, we already can obtain fragments that are PSPACE-complete by restricting our clauses to DET-HORN or KROM. However such restrictions yield very different formulas to the canonical PSPACE-complete language of Quantified Boolean Formulas (QBF). This is despite Bernays-Schoenfinkel having a natural connection to an extension of QBF known as Dependency QBF. Our main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy. We use this definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy. |
| title | Reintroducing the Second Player in EPR |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.16410 |