{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T02:39:19Z","timestamp":1777516759259,"version":"3.51.4"},"reference-count":21,"publisher":"SAGE Publications","issue":"4","license":[{"start":{"date-parts":[[2017,3,6]],"date-time":"2017-03-06T00:00:00Z","timestamp":1488758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Computability"],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>Two new characterizations of [Formula: see text]-definable sets, i.e. sets of integers definable in first-order logic with the order relation and modular relations, are provided. Those characterizations are used to prove that satisfiability of first-order logic over words with an order relation and a [Formula: see text]-definable set that is not [Formula: see text]-definable is undecidable.<\/jats:p>","DOI":"10.3233\/com-170069","type":"journal-article","created":{"date-parts":[[2017,3,7]],"date-time":"2017-03-07T10:18:26Z","timestamp":1488881906000},"page":"333-363","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":1,"title":["Undecidability of satisfiability of expansions of FO[&lt;] over words with a\u00a0FO[+]-definable set"],"prefix":"10.1177","volume":"6","author":[{"given":"Arthur","family":"Milchior","sequence":"first","affiliation":[{"name":"IRIF, Universit\u00e9 Paris 7\u00a0\u2013 Denis Diderot, France"},{"name":"CNRS UMR 8243, Universit\u00e9 Paris Diderot\u00a0\u2013 Paris 7, Case 7014, 75205 Paris Cedex 13, France"},{"name":"Universit\u00e9 Paris-Est, LACL (EA 4219), UPEC, F-94010 Cr\u00e9teil, France. ."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2017,3,6]]},"reference":[{"key":"ref001","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(92)90014-A"},{"key":"ref002","first-page":"191","volume":"1","author":"Bruy\u00e8re V.","year":"1994","journal-title":"Bull. Belg. Math. Soc"},{"key":"ref003","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"issue":"1","key":"ref004","first-page":"121","volume":"42","author":"Choffrut C.","year":"2008","journal-title":"RAIRO ITA"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"C.\u00a0Choffrut, A.\u00a0Malcher, C.\u00a0Mereghetti and B.\u00a0Palano, On the expressive power of FO[+], in: LATA, A.H.\u00a0Dediu, H.\u00a0Fernau and C.\u00a0Mart\u00edn-Vide, eds, Lecture Notes in Computer Science, Vol.\u00a06031, Springer, 2010, pp.\u00a0190\u2013201.","DOI":"10.1007\/978-3-642-13089-2_16"},{"key":"ref006","first-page":"91","volume":"7","author":"Cooper D.C.","year":"1972","journal-title":"Machine Intelligence"},{"key":"ref007","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1961-0139530-9"},{"key":"ref008","doi-asserted-by":"publisher","DOI":"10.2307\/2269808"},{"key":"ref009","unstructured":"A.\u00a0Finkel and J.\u00a0Leroux, Presburger functions are piecewise linear, Research Report LSV-08-08, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France, 2008, 9\u00a0pp."},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1966.16.285"},{"key":"ref011","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"ref012","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2004.1313817"},{"key":"ref013","unstructured":"R.\u00a0McNaughton and S.\u00a0Papert, Counter-Free Automata, M.I.T. Press, Cambridge, Mass, 1971."},{"key":"ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(95)00022-4"},{"key":"ref015","doi-asserted-by":"publisher","DOI":"10.2307\/1970290"},{"key":"ref016","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00047-6"},{"key":"ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90152-6"},{"key":"ref018","unstructured":"M.\u00a0Presburger, \u00dcber die vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt, in: Comptes Rendus du Premier Congr\u00e8s des Math\u00e9maticienes des Pays Slaves, Warsaw, 1927, pp.\u00a092\u2013101, 395."},{"key":"ref019","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0289-9"},{"key":"ref020","first-page":"569","volume":"70","author":"Trakhtenbrot B.A.","year":"1950","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"ref021","first-page":"326","volume":"140","author":"Trakhtenbrot B.A.","year":"1961","journal-title":"Dokl. Akad. Nauk SSSR"}],"container-title":["Computability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/COM-170069","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/COM-170069","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/COM-170069","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T15:59:55Z","timestamp":1777391995000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/COM-170069"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,6]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.3233\/COM-170069"],"URL":"https:\/\/doi.org\/10.3233\/com-170069","relation":{},"ISSN":["2211-3568","2211-3576"],"issn-type":[{"value":"2211-3568","type":"print"},{"value":"2211-3576","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,6]]}}}