{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T21:07:45Z","timestamp":1789938465334,"version":"4.0.1"},"reference-count":28,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":5215,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1999,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Guarded fragments of first-order logic were recently introduced by Andr\u00e9ka, van Benthem and N\u00e9meti; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable fragments of first-order logic.<\/jats:p><jats:p>Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the <jats:italic>guarded fragment<\/jats:italic> (<jats:bold>GF<\/jats:bold>) and the <jats:italic>loosely guarded fragment<\/jats:italic> (<jats:bold>LGF<\/jats:bold>) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is E<jats:sc>xptime<\/jats:sc>-complete. We further establish a <jats:italic>tree model property<\/jats:italic> for both the guarded fragment and the loosely guarded fragment, and give a proof of the <jats:italic>finite model property<\/jats:italic> of the guarded fragment.<\/jats:p><jats:p>It is also shown that some natural, modest extensions of the guarded fragments are undecidable.<\/jats:p>","DOI":"10.2307\/2586808","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:03:57Z","timestamp":1146938637000},"page":"1719-1742","source":"Crossref","is-referenced-by-count":194,"title":["On the Restraining Power of Guards"],"prefix":"10.1017","volume":"64","author":[{"given":"Erich","family":"Gr\u00e4del","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S002248120001286X_ref002","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004275029985"},{"key":"S002248120001286X_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/BF00971620"},{"key":"S002248120001286X_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(89)90023-7"},{"key":"S002248120001286X_ref011","doi-asserted-by":"publisher","DOI":"10.2307\/421196"},{"key":"S002248120001286X_ref026","first-page":"87","volume-title":"Surveys in combinatorics","author":"Reed","year":"1997"},{"key":"S002248120001286X_ref001","first-page":"243","volume":"64","author":"Andr\u00e9ka","year":"1999","journal-title":"Finite algebras of relations are representable on finite sets"},{"key":"S002248120001286X_ref024","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"S002248120001286X_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"S002248120001286X_ref014","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/s001530050130","article-title":"Undecidability results on two-variable logics","volume":"38","author":"Gr\u00e4del","year":"1999","journal-title":"Archive of Mathematical Logic"},{"key":"S002248120001286X_ref019","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4993"},{"key":"S002248120001286X_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-75357-2"},{"key":"S002248120001286X_ref006","unstructured":"van Benthem J. , Dynamic bits and pieces, ILLC Research Report, 1997."},{"key":"S002248120001286X_ref016","unstructured":"Grohe M. and Mari\u00f1o J. , Definability and descriptive complexity on databases of bounded treewidth, submitted for publication."},{"key":"S002248120001286X_ref009","first-page":"193","volume-title":"Principles of knowledge representation","author":"Donnini","year":"1996"},{"key":"S002248120001286X_ref025","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"S002248120001286X_ref028","volume-title":"Why is modal logic so robustly decidable","volume":"31","author":"Vardi","year":"1997"},{"key":"S002248120001286X_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/BF01299742"},{"key":"S002248120001286X_ref013","volume-title":"Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS '97, Warsaw","author":"Gr\u00e4del","year":"1997"},{"key":"S002248120001286X_ref004","volume-title":"Modal logic an classical logic","author":"van Benthem","year":"1983"},{"key":"S002248120001286X_ref005","volume-title":"Exploring logical dynamics","author":"van Benthem","year":"1996"},{"key":"S002248120001286X_ref007","doi-asserted-by":"crossref","unstructured":"Berger R. , The undecidability of the domino problem , Memoirs of the American Mathemtical Society, no. 66, 1966.","DOI":"10.1090\/memo\/0066"},{"key":"S002248120001286X_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00308-9"},{"key":"S002248120001286X_ref015","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19990450304"},{"key":"S002248120001286X_ref018","first-page":"51","article-title":"Recurring dominoes: Making the highly undecidable highly understandable","volume":"24","author":"Harel","year":"1985","journal-title":"Annals of Discrete Mathematics"},{"key":"S002248120001286X_ref021","article-title":"Extending partial isomorphisms for the small index property of many \u03c9-categorical structures","author":"Herwig","journal-title":"Israel Journal of Mathematics"},{"key":"S002248120001286X_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BF01305233"},{"key":"S002248120001286X_ref023","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.48.3.365"},{"key":"S002248120001286X_ref027","first-page":"953","article-title":"On recursive separability","volume":"88","author":"Trakhtenbrot","year":"1953","journal-title":"Doklady Akademii Nauk SSSR"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S002248120001286X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,9]],"date-time":"2019-05-09T19:57:10Z","timestamp":1557431830000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S002248120001286X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,12]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1999,12]]}},"alternative-id":["S002248120001286X"],"URL":"https:\/\/doi.org\/10.2307\/2586808","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,12]]}}}