{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T00:59:43Z","timestamp":1777424383484,"version":"3.51.4"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,6,30]],"date-time":"2015-06-30T00:00:00Z","timestamp":1435622400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF","award":["IIS-0905276 and IIS-1217869"],"award-info":[{"award-number":["IIS-0905276 and IIS-1217869"]}]},{"name":"ERC Starting Grant Sosna"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2015,6,30]]},"abstract":"<jats:p>We consider restrictions of first-order logic and of fixpoint logic in which all occurrences of negation are required to be guarded by an atomic predicate. In terms of expressive power, the logics in question, called GNFO and GNFP, extend the guarded fragment of first-order logic and the guarded least fixpoint logic, respectively. They also extend the recently introduced unary negation fragments of first-order logic and of least fixpoint logic.<\/jats:p>\n          <jats:p>We show that the satisfiability problem for GNFO and for GNFP is 2ExpTime-complete, both on arbitrary structures and on finite structures. We also study the complexity of the associated model checking problems. Finally, we show that GNFO and GNFP are not only computationally well behaved, but also model theoretically: we show that GNFO and GNFP have the tree-like model property and that GNFO has the finite model property, and we characterize the expressive power of GNFO in terms of invariance for an appropriate notion of bisimulation.<\/jats:p>\n          <jats:p>Our complexity upper bounds for GNFO and GNFP hold true even for their \u201cclique-guarded\u201d extensions CGNFO and CGNFP, in which clique guards are allowed in the place of guards.<\/jats:p>","DOI":"10.1145\/2701414","type":"journal-article","created":{"date-parts":[[2015,7,6]],"date-time":"2015-07-06T14:04:16Z","timestamp":1436191456000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Guarded Negation"],"prefix":"10.1145","volume":"62","author":[{"given":"Vince","family":"B\u00e1r\u00e1ny","sequence":"first","affiliation":[{"name":"LogicBlox Inc., Atlanta, GA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Balder Ten","family":"Cate","sequence":"additional","affiliation":[{"name":"LogicBlox Inc. and University of California Santa Cruz"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luc","family":"Segoufin","sequence":"additional","affiliation":[{"name":"INRIA and ENS-Cachan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,6,30]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004275029985"},{"key":"e_1_2_1_2_1","volume-title":"Rudiments of Mu-Calculus","author":"Arnold Andr\u00e9","unstructured":"Andr\u00e9 Arnold and Damian Niwinski . 2001. Rudiments of Mu-Calculus . Elsevier . Andr\u00e9 Arnold and Damian Niwinski. 2001. Rudiments of Mu-Calculus. Elsevier."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the International Symposium on Mathematical Foundations of Computer Science (MFCS).","author":"B\u00e1r\u00e1ny Vince","year":"2013","unstructured":"Vince B\u00e1r\u00e1ny , Michael Benedikt , and Balder ten Cate . 2013 . Rewriting guarded negation queries . In Proceedings of the International Symposium on Mathematical Foundations of Computer Science (MFCS). Vince B\u00e1r\u00e1ny, Michael Benedikt, and Balder ten Cate. 2013. Rewriting guarded negation queries. In Proceedings of the International Symposium on Mathematical Foundations of Computer Science (MFCS)."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2012.02.005"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.26"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the International Conference on Very Large Databases (VLDB).","author":"B\u00e1r\u00e1ny Vince","year":"2012","unstructured":"Vince B\u00e1r\u00e1ny , Balder ten Cate , and Martin Otto . 2012 . Queries with guarded negation . In Proceedings of the International Conference on Very Large Databases (VLDB). Vince B\u00e1r\u00e1ny, Balder ten Cate, and Martin Otto. 2012. Queries with guarded negation. In Proceedings of the International Conference on Very Large Databases (VLDB)."},{"key":"e_1_2_1_7_1","first-page":"356","article-title":"Guarded negation. In Proceedings of the International Conference on Automata, Languages and Programming (ICALP)","volume":"6756","author":"B\u00e1r\u00e1ny Vince","year":"2011","unstructured":"Vince B\u00e1r\u00e1ny , Balder ten Cate , and Luc Segoufin . 2011 . Guarded negation. In Proceedings of the International Conference on Automata, Languages and Programming (ICALP) . Lecture Notes in Computer Science , vol. 6756 , Spring er, 356 -- 367 . Vince B\u00e1r\u00e1ny, Balder ten Cate, and Luc Segoufin. 2011. Guarded negation. In Proceedings of the International Conference on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 6756, Springer, 356--367.","journal-title":"Lecture Notes in Computer Science"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/645710.664459"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463664.2465223"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00866-6"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1182353853"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/602220.602222"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00012-9"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753628"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586808"},{"key":"e_1_2_1_16_1","unstructured":"Erich Gr\u00e4del. 2001. Why are modal logics so robustly decidable? In Current Trends in Theoretical Computer Science 393--408.   Erich Gr\u00e4del. 2001. Why are modal logics so robustly decidable? In Current Trends in Theoretical Computer Science 393--408."},{"key":"e_1_2_1_17_1","first-page":"4","article-title":"Undecidability results on two-variable logics","volume":"38","author":"Gr\u00e4del Erich","year":"1999","unstructured":"Erich Gr\u00e4del , Martin Otto , and Eric Rosen . 1999 . Undecidability results on two-variable logics . Arch. Math. Log. 38 , 4 -- 5 , 313--354. Erich Gr\u00e4del, Martin Otto, and Eric Rosen. 1999. Undecidability results on two-variable logics. Arch. Math. Log. 38, 4--5, 313--354.","journal-title":"Arch. Math. Log."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788956"},{"key":"e_1_2_1_19_1","volume-title":"Model Theory","author":"Hodges W.","unstructured":"W. Hodges . 1993. Model Theory . Cambridge University Press . W. Hodges. 1993. Model Theory. Cambridge University Press."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015178417181"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011207512025"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.04.003"},{"key":"e_1_2_1_24_1","first-page":"1418","article-title":"Expressive completeness through logically tractable models","volume":"12","author":"Otto Martin","year":"2012","unstructured":"Martin Otto . 2012 . Expressive completeness through logically tractable models . Ann. Pure Appl. Logic 12 , 1418 -- 1453 . Martin Otto. 2012. Expressive completeness through logically tractable models. Ann. Pure Appl. Logic 12, 1418--1453.","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Balder ten Cate and Luc Segoufin. 2013. Unary negation. Log. Meth. Comput. Sci. 9.  Balder ten Cate and Luc Segoufin. 2013. Unary negation. Log. Meth. Comput. Sci. 9.","DOI":"10.2168\/LMCS-9(3:25)2013"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Moshe Y. Vardi. 1996. Why is modal logic so robustly decidable? In Descr. Complex. Finite Models. 149--184.  Moshe Y. Vardi. 1996. Why is modal logic so robustly decidable? In Descr. Complex. Finite Models. 149--184.","DOI":"10.1090\/dimacs\/031\/05"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 7th International Conference on Very Large Data Bases -","volume":"7","author":"Yannakakis Mihalis","year":"1981","unstructured":"Mihalis Yannakakis . 1981 . Algorithms for acyclic database schemes . In Proceedings of the 7th International Conference on Very Large Data Bases - Volume 7 (VLDB'81). VLDB Endowment, 82--94. Mihalis Yannakakis. 1981. Algorithms for acyclic database schemes. In Proceedings of the 7th International Conference on Very Large Data Bases - Volume 7 (VLDB'81). VLDB Endowment, 82--94."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2701414","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2701414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:10Z","timestamp":1750227190000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2701414"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,30]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6,30]]}},"alternative-id":["10.1145\/2701414"],"URL":"https:\/\/doi.org\/10.1145\/2701414","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,30]]},"assertion":[{"value":"2014-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-06-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}