{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:37:05Z","timestamp":1753889825737,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2013,9,24]],"date-time":"2013-09-24T00:00:00Z","timestamp":1379980800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["0905276"],"award-info":[{"award-number":["0905276"]}]},{"name":"National Science Foundation","award":["1217869"],"award-info":[{"award-number":["1217869"]}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["226513"],"award-info":[{"award-number":["226513"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We study fragments of first-order logic and of least fixed point logic that\nallow only unary negation: negation of formulas with at most one free variable.\nThese logics generalize many interesting known formalisms, including modal\nlogic and the $\\mu$-calculus, as well as conjunctive queries and monadic\nDatalog. We show that satisfiability and finite satisfiability are decidable\nfor both fragments, and we pinpoint the complexity of satisfiability, finite\nsatisfiability, and model checking. We also show that the unary negation\nfragment of first-order logic is model-theoretically very well behaved. In\nparticular, it enjoys Craig Interpolation and the Projective Beth Property.<\/jats:p>","DOI":"10.2168\/lmcs-9(3:25)2013","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:44:29Z","timestamp":1385732669000},"source":"Crossref","is-referenced-by-count":8,"title":["Unary negation"],"prefix":"10.46298","volume":"Volume 9, Issue 3","author":[{"given":"Luc","family":"Segoufin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Balder ten","family":"Cate","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2013,9,24]]},"reference":[{"key":"839:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/792\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/792\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:56:16Z","timestamp":1681242976000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/792"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,24]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-9(3:25)2013","relation":{"is-same-as":[{"id-type":"arxiv","id":"1309.2069","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1309.2069","asserted-by":"subject"}],"is-part-of":[{"id-type":"doi","id":"10.4230\/lipics.stacs.2011","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2013,9,24]]},"article-number":"792"}}