{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:30:33Z","timestamp":1742913033135,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted predicates are often undecidable, as is, for instance, Presburger arithmetic extended with a single uninterpreted unary predicate. In the SMT world, difference logic is a quite popular fragment of linear arithmetic which is less expressive than Presburger arithmetic. Difference logic on integers with uninterpreted unary predicates is known to be decidable, even in the presence of quantifiers. We here show that (quantified) difference logic on real numbers with a single uninterpreted unary predicate is undecidable, quite surprisingly. Moreover, we prove that difference logic on integers, together with order on reals, combined with uninterpreted unary predicates, remains decidable.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_31","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"542-559","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Decidability of\u00a0Difference Logic over\u00a0the\u00a0Reals with\u00a0Uninterpreted Unary Predicates"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4721-3824","authenticated-orcid":false,"given":"Bernard","family":"Boigelot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4700-6031","authenticated-orcid":false,"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5545-4579","authenticated-orcid":false,"given":"Baptiste","family":"Vergain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"31_CR1","unstructured":"Boigelot, B., Fontaine, P., Vergain, B.: Decidability of difference logics with unary predicates. In: Proceedings, 7th International Workshop on Satisfiability Checking and Symbolic Computation (2022)"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Fontaine, P., Vergain, B.: Decidability of difference logic over the reals with uninterpreted unary predicates. arXiv preprint arXiv:2305.15059 (2023)","DOI":"10.1007\/978-3-031-38499-8_31"},{"issue":"1","key":"31_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jcss.2006.10.009","volume":"73","author":"V Bruy\u00e8re","year":"2007","unstructured":"Bruy\u00e8re, V., Carton, O.: Automata on linear orderings. J. Comput. Syst. Sci. 73(1), 1\u201324 (2007)","journal-title":"J. Comput. Syst. Sci."},{"key":"31_CR4","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science (1962)"},{"issue":"2","key":"31_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1305\/ndjfl\/1093870820","volume":"26","author":"JP Burgess","year":"1985","unstructured":"Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Formal Logic 26(2), 115\u2013128 (1985)","journal-title":"Notre Dame J. Formal Logic"},{"key":"31_CR6","unstructured":"Cristau, J.: Automata and temporal logic over arbitrary linear time. In: FSTTCS 2009. LIPIcs, vol. 4, pp. 133\u2013144 (2009)"},{"key":"31_CR7","unstructured":"Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Center for Research in Computer Technology, Harvard University, Technical report (1972)"},{"key":"31_CR8","volume-title":"A Mathematical Introduction to Logic","author":"HB Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, Boston (2001)","edition":"2"},{"issue":"2\u20133","key":"31_CR9","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0003-4843(82)90004-3","volume":"23","author":"Y Gurevich","year":"1982","unstructured":"Gurevich, Y., Shelah, S.: Monadic theory of order and topology in ZFC. Ann. Math. Logic 23(2\u20133), 179\u2013198 (1982)","journal-title":"Ann. Math. Logic"},{"issue":"3","key":"31_CR10","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/3242953.3242964","volume":"5","author":"C Haase","year":"2018","unstructured":"Haase, C.: A survival guide to Presburger arithmetic. ACM SIGLOG News 5(3), 67\u201382 (2018)","journal-title":"ACM SIGLOG News"},{"issue":"2","key":"31_CR11","doi-asserted-by":"publisher","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is $$\\Pi _1^1$$ complete. J. Symbolic Logic 56(2), 637\u2013642 (1991)","journal-title":"J. Symbolic Logic"},{"key":"31_CR12","volume-title":"Hilbert\u2019s Tenth Problem","author":"YV Matiyasevich","year":"1993","unstructured":"Matiyasevich, Y.V.: Hilbert\u2019s Tenth Problem. MIT Press, Cambridge (1993)"},{"key":"31_CR13","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1016\/j.ic.2011.11.002","volume":"210","author":"A Rabinovich","year":"2012","unstructured":"Rabinovich, A.: Temporal logics over linear time domains are in PSPACE. Inf. Comput. 210, 40\u201367 (2012)","journal-title":"Inf. Comput."},{"issue":"8","key":"31_CR14","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/j.apal.2010.01.002","volume":"161","author":"M Reynolds","year":"2010","unstructured":"Reynolds, M.: The complexity of temporal logic over the reals. Ann. Pure Appl. Logic 161(8), 1063\u20131096 (2010)","journal-title":"Ann. Pure Appl. Logic"},{"key":"31_CR15","volume-title":"Linear Orderings","author":"JG Rosenstein","year":"1982","unstructured":"Rosenstein, J.G.: Linear Orderings. Academic Press, Cambridge (1982)"},{"key":"31_CR16","first-page":"157","volume":"34","author":"CE Shannon","year":"1956","unstructured":"Shannon, C.E.: A universal Turing machine with two internal states. Automata Stud. 34, 157\u2013165 (1956)","journal-title":"Automata Stud."},{"issue":"3","key":"31_CR17","doi-asserted-by":"publisher","first-page":"379","DOI":"10.2307\/1971037","volume":"102","author":"S Shelah","year":"1975","unstructured":"Shelah, S.: The monadic theory of order. Ann. Math. 102(3), 379\u2013419 (1975)","journal-title":"Ann. Math."},{"key":"31_CR18","volume-title":"Cardinal and ordinal numbers","author":"W Sierpi\u0144ski","year":"1965","unstructured":"Sierpi\u0144ski, W.: Cardinal and ordinal numbers, 2nd edn. PWN, Warszawa (1965)","edition":"2"},{"issue":"5\u20136","key":"31_CR19","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s00153-013-0328-9","volume":"52","author":"SO Speranski","year":"2013","unstructured":"Speranski, S.O.: A note on definability in fragments of arithmetic with free unary predicates. Arch. Math. Log. 52(5\u20136), 507\u2013516 (2013)","journal-title":"Arch. Math. Log."},{"key":"31_CR20","doi-asserted-by":"publisher","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,20]],"date-time":"2023-12-20T21:38:31Z","timestamp":1703108311000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}