{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:24:09Z","timestamp":1760081049944,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2019,9,10]],"date-time":"2019-09-10T00:00:00Z","timestamp":1568073600000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,9,10]],"date-time":"2019-09-10T00:00:00Z","timestamp":1568073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,9,10]],"date-time":"2019-09-10T00:00:00Z","timestamp":1568073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/L012138\/1"],"award-info":[{"award-number":["EP\/L012138\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/N014359\/1"],"award-info":[{"award-number":["EP\/N014359\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back and forth between relational logics and logics over trees.<\/jats:p>","DOI":"10.23638\/lmcs-15(3:29)2019","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:38:35Z","timestamp":1743701915000},"source":"Crossref","is-referenced-by-count":1,"title":["Definability and Interpolation within Decidable Fixpoint Logics"],"prefix":"10.23638","volume":"Volume 15, Issue 3","author":[{"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Bourhis","sequence":"additional","affiliation":[]},{"given":"Michael Vanden","family":"Boom","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2019,9,10]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/arxiv.org\/pdf\/1705.01823v4","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/arxiv.org\/pdf\/1705.01823v4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:38:35Z","timestamp":1743701915000},"score":1,"resource":{"primary":{"URL":"http:\/\/lmcs.episciences.org\/4729"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,10]]},"references-count":0,"URL":"https:\/\/doi.org\/10.23638\/lmcs-15(3:29)2019","relation":{"has-preprint":[{"id-type":"arxiv","id":"1705.01823v3","asserted-by":"subject"},{"id-type":"arxiv","id":"1705.01823v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1705.01823","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1705.01823","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2019,9,10]]},"article-number":"4729"}}