{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:49:53Z","timestamp":1763459393227,"version":"3.45.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,12,6]],"date-time":"2015-12-06T00:00:00Z","timestamp":1449360000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/H017690\/1, EP\/L012138\/1"],"award-info":[{"award-number":["EP\/H017690\/1, EP\/L012138\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["IIS-1217869"],"award-info":[{"award-number":["IIS-1217869"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2016,3,28]]},"abstract":"<jats:p>Desirable properties of a logic include decidability, and a model theory that inherits properties of first-order logic, such as interpolation and preservation theorems. It is known that the Guarded Fragment (GF) of first-order logic is decidable and satisfies some preservation properties from first-order model theory; however, it fails to have Craig interpolation. The Guarded Negation Fragment (GNF), a recently defined extension, is known to be decidable and to have Craig interpolation. Here we give the first results on effective interpolation for extensions of GF. We provide an interpolation procedure for GNF whose complexity matches the doubly exponential upper bound for satisfiability of GNF. We show that the same construction gives not only Craig interpolation, but Lyndon interpolation and relativized interpolation, which can be used to provide effective proofs of some preservation theorems. We provide upper bounds on the size of GNF interpolants for both GNF and GF input, and complement this with matching lower bounds.<\/jats:p>","DOI":"10.1145\/2814570","type":"journal-article","created":{"date-parts":[[2015,12,7]],"date-time":"2015-12-07T14:33:52Z","timestamp":1449498832000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Effective Interpolation and Preservation in Guarded Logics"],"prefix":"10.1145","volume":"17","author":[{"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Balder Ten","family":"Cate","sequence":"additional","affiliation":[{"name":"LogicBlox and UC Santa Cruz, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael Vanden","family":"Boom","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,12,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/551350"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004275029985"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/772062.772068"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Franz Baader Diego Calvanese Deborah L. McGuinness Daniele Nardi and Peter F. Patel-Schneider (Eds.). 2003. The Description Logic Handbook. Cambridge.","DOI":"10.5555\/1215128"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Vince B\u00e1r\u00e1ny Michael Benedikt and Pierre Bourhis. 2013a. Access patterns and integrity constraints revisited. In ICDT.","DOI":"10.1145\/2448496.2448522"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Vince B\u00e1r\u00e1ny Michael Benedikt and Balder ten Cate. 2013b. Rewriting guarded negation queries. In MFCS.","DOI":"10.1007\/978-3-642-40313-2_11"},{"key":"e_1_2_1_7_1","volume-title":"Balder ten Cate, and Luc Segoufin","author":"B\u00e1r\u00e1ny Vince","year":"2011","unstructured":"Vince B\u00e1r\u00e1ny, Balder ten Cate, and Luc Segoufin. 2011. Guarded negation. In ICALP."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603108"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.08.015"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Anuj Dawar Martin Grohe Stephan Kreutzer and Nicole Schweikardt. 2007. Model theory makes formulas large. In ICALP.","DOI":"10.5555\/2394539.2394645"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/230183"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(76)90167-5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586808"},{"key":"e_1_2_1_15_1","unstructured":"Eva Hoogland. 2000. Definability and Interpolation: Model-Theoretic Investigations. Ph.D. dissertation. University of Amsterdam."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Eva Hoogland Maarten Marx and Martin Otto. 1999. Beth definability for the guarded fragment. In LPAR.","DOI":"10.5555\/645709.664328"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1959.9.129"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Maarten Marx. 2007. Queries determined by views: Pack your views. In PODS. 10.1145\/1265530.1265534","DOI":"10.1145\/1265530.1265534"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Maarten Marx Szabolcs Mikul\u00e1s and Mark Reynolds. 2000. The mosaic method for temporal logics. In TABLEAUX.","DOI":"10.5555\/646891.709290"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Ken McMillan. 2004. Applications of Craig interpolation to model checking. In CSL.","DOI":"10.1007\/978-3-540-30124-0_3"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.2.305"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274095"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806907.1806913"},{"key":"e_1_2_1_24_1","unstructured":"Istvan N\u00e9meti. 1986. Free Algebras and Decidability in Algebraic Logic. Ph.D. dissertation. Hungarian Academy of Sciences Budapest."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.2307\/420966"},{"key":"e_1_2_1_26_1","unstructured":"Balder ten Cate Enrico Franconi and Inanc Seylan. 2011. Beth definability in expressive description logics. In IJCAI."},{"key":"e_1_2_1_27_1","unstructured":"Balder ten Cate and Luc Segoufin. 2011. Unary negation. In STACS."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2814570","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2814570","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2814570","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:43:24Z","timestamp":1763459004000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2814570"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,6]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,3,28]]}},"alternative-id":["10.1145\/2814570"],"URL":"https:\/\/doi.org\/10.1145\/2814570","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2015,12,6]]},"assertion":[{"value":"2015-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-08-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-12-06","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}