{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T14:44:35Z","timestamp":1762008275685,"version":"build-2065373602"},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Past research into decidable fragments of first-order logic (FO) has produced two very prominent fragments: the guarded fragment GF, and the two-variable fragment FO2. These fragments are of crucial importance because they provide significant insights into decidabil- ity and expressiveness of other (computational) logics like Modal Logics (MLs) and various Description Logics (DLs), which play a central role in Verification, Knowledge Represen- tation, and other areas. In this paper, we take a closer look at GF and FO2, and present a new fragment that subsumes them both. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF: quantification is required to be guarded only for subformulae with three or more free variables. We show that, in the absence of equality, satisfiability in TGF is N2ExpTime-complete, but becomes NExpTime-complete if we bound the arity of predicates by a constant (a natural assumption in the context of MLs and DLs). Finally, we observe that many natural extensions of TGF, including the addition of equality, lead to undecidability.<\/jats:p>","DOI":"10.29007\/m8ts","type":"proceedings-article","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T16:06:42Z","timestamp":1540310802000},"page":"604-587","source":"Crossref","is-referenced-by-count":4,"title":["The Triguarded Fragment of First-Order Logic"],"prefix":"10.29007","volume":"57","author":[{"given":"Sebastian","family":"Rudolph","sequence":"first","affiliation":[]},{"given":"Mantas","family":"Simkus","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T16:06:48Z","timestamp":1540310808000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/wlJ3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/m8ts","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}