{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T11:00:49Z","timestamp":1784804449874,"version":"3.55.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325884","type":"print"},{"value":"9783032325891","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Building on the small-model constructions for \u00c5qvist\u2019s deontic logics introduced in\u00a0[24], we present\n                    <jats:sc>Deo-SMT<\/jats:sc>\n                    , an SMT-based reasoner implemented in Z3 for checking validity and generating countermodels.\n                    <jats:sc>Deo-SMT<\/jats:sc>\n                    covers all four of \u00c5qvist\u2019s logics (\n                    <jats:bold>E<\/jats:bold>\n                    ,\u00a0\n                    <jats:bold>F<\/jats:bold>\n                    ,\u00a0\n                    <jats:bold>F+(CM)<\/jats:bold>\n                    ,\u00a0\n                    <jats:bold>G<\/jats:bold>\n                    ) and provides countermodel visualizations as text, matrices, and directed graphs. Our tool outperforms the existing Isabelle\/HOL approach, while providing a lightweight and accessible interface for normative reasoning.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32589-1_27","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:02:36Z","timestamp":1784800956000},"page":"455-464","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SMT-Based Deontic Reasoning for\u00a0\u00c5qvist Logics"],"prefix":"10.1007","author":[{"given":"Christian","family":"K\u00f6ll","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Agata","family":"Ciabattoni","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dmitry","family":"Rozplokhas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"27_CR1","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/978-94-009-6259-0_11","volume-title":"Handbook of Philosophical Logic","author":"L \u00c5qvist","year":"1984","unstructured":"\u00c5qvist, L.: Deontic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. II, pp. 605\u2013714. Springer, Dordrecht (1984)"},{"issue":"5","key":"27_CR2","first-page":"733","volume":"6","author":"C Benzm\u00fcller","year":"2019","unstructured":"Benzm\u00fcller, C., Farjami, A., Parent, X.: \u00c5qvist\u2019s dyadic deontic logic E in HOL. FLAP 6(5), 733\u2013754 (2019)","journal-title":"FLAP"},{"key":"27_CR3","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103348","volume":"287","author":"C Benzm\u00fcller","year":"2020","unstructured":"Benzm\u00fcller, C., Parent, X., van der Torre, L.W.N.: Designing normative theories for ethical and legal reasoning: Logikey framework, methodology, and tool support. Artif. Intell. 287, 103348 (2020)","journal-title":"Artif. Intell."},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-319-94418-0_6","volume-title":"Sailing Routes in the World of Computation","author":"C Benzm\u00fcller","year":"2018","unstructured":"Benzm\u00fcller, C., Parent, X., van der Torre, L.: A Deontic Logic Reasoning Infrastructure. In: Manea, F., Miller, R.G., Nowotka, D. (eds.) CiE 2018. LNCS, vol. 10936, pp. 60\u201369. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94418-0_6"},{"issue":"3","key":"27_CR5","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1305\/ndjfl\/1093883456","volume":"22","author":"J Burgess","year":"1981","unstructured":"Burgess, J.: Quick completeness proofs for some logics of conditionals. Notre Dame J. Formal Logic 22(3), 76\u201384 (1981)","journal-title":"Notre Dame J. Formal Logic"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., Olivetti, N., Parent, X.: Dyadic obligations: proofs and countermodels via hypersequents. In: Proceedings of the PRIMA 2022, pp. 54\u201371. Springer (2022)","DOI":"10.1007\/978-3-031-21203-1_4"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., Rozplokhas, D., Tesi, M.: GL-based calculi for PCL and its deontic cousin. In: Proceedings of the JELIA 2025 (2025)","DOI":"10.1007\/978-3-032-04587-4_11"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., Tesi, M.: Sequents vs hypersequents for \u00c5qvist systems. In: Proceedings of the IJCAR 2024, pp. 176\u2013195. Springer (2024)","DOI":"10.1007\/978-3-031-63501-4_10"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Friedman, N., Halpern, J.Y.: On the complexity of conditional logics. In: Proceedings of the KR 1994, pp. 202\u2013213. Elsevier (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50115-9"},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-82453-1_15","volume-title":"Logics and Models of Concurrent Systems","author":"DM Gabbay","year":"1985","unstructured":"Gabbay, D.M.: Theoretical foundations for non-monotonic reasoning in expert systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems, pp. 439\u2013457. Springer, Berlin Heidelberg, Berlin, Heidelberg (1985)"},{"key":"27_CR12","unstructured":"Gabbay, D.M., Horty, J., Parent, X., van\u00a0der Meyden, R., van\u00a0der Torre, L., (eds.): Handbook of Deontic Logic and Normative Systems. College Publications (2013)"},{"key":"27_CR13","volume-title":"Handbook of Deontic Logic and Normative Systems","year":"2021","unstructured":"Gabbay, D.M., Horty, J.F., Parent, X., van der Meyden, R., van der Torre, L. (eds.): Handbook of Deontic Logic and Normative Systems, vol. 2. College Publications, London (2021)"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: Analytic tableaux calculi for KLM logics of nonmonotonic reasoning. ACM Trans. Comput. Log. 10(3), 18:1\u201318:47 (2009)","DOI":"10.1145\/1507244.1507248"},{"key":"27_CR15","volume-title":"On the Proof Theory of Conditional Logics","author":"M Girlando","year":"2019","unstructured":"Girlando, M.: On the Proof Theory of Conditional Logics. Aix-Marseille Universite; Helsinki University, Theses (2019)"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Hansson, B.: An analysis of some deontic logics. Deontic Logic Introductory Syst. Readings, 121\u2013147. Springer (1971)","DOI":"10.1007\/978-94-010-3146-2_5"},{"issue":"1\u20132","key":"27_CR17","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0004-3702(90)90101-5","volume":"44","author":"S Kraus","year":"1990","unstructured":"Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. 44(1\u20132), 167\u2013207 (1990)","journal-title":"Artif. Intell."},{"key":"27_CR18","unstructured":"Lewis, D.: Counterfactuals, blackwells (1973)"},{"issue":"4","key":"27_CR19","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1023\/A:1004748624537","volume":"29","author":"D Makinson","year":"2000","unstructured":"Makinson, D., van der Torre, L.W.N.: Input\/output logics. J. Philos. Log. 29(4), 383\u2013408 (2000)","journal-title":"J. Philos. Log."},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Parent, X.: Maximality vs. optimality in dyadic deontic logic. J. Philos. Log. 43, 1101\u20131128 (2014)","DOI":"10.1007\/s10992-013-9308-0"},{"key":"27_CR21","unstructured":"Parent, X.: Preference semantics for Hansson-type dyadic deontic logic: a survey of results. In: Gabbay, D., Horty, J., Parent, X., van\u00a0der Torre, L., van\u00a0der Meyden, R., (eds.) Handbook of Deontic Logic and Normative Systems, vol. 2, pp. 7\u201370. College Publications, London (2021)"},{"key":"27_CR22","unstructured":"Parent, X., Benzm\u00fcller, C.: Automated verification of deontic correspondences in Isabelle\/HOL-first results. In: Proceedings of the Automated Reasoning in Quantified Non-Classical Logics, 4th International Workshop (associated with FLoC and IJCAR 2022), pp. 92\u2013108 (2022)"},{"issue":"4","key":"27_CR23","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1080\/11663081.2024.2386917","volume":"34","author":"X Parent","year":"2024","unstructured":"Parent, X., Benzm\u00fcller, C.: Conditional normative reasoning as a fragment of HOL. J. Appl. Non Class. Logics 34(4), 561\u2013592 (2024)","journal-title":"J. Appl. Non Class. Logics"},{"key":"27_CR24","unstructured":"Rozplokhas, D.: Lego-like small model constructions for \u00e5qvist\u2019s logics. In: Ciabattoni, A., Gabelaia, D., Sedl\u00e1r, I., (eds.) Advances in Modal Logic, pp. 631\u2013651. College Publications (2024)"},{"key":"27_CR25","unstructured":"Shoham, Y.: A semantical approach to nonmonotic logics. In: Proceedings of the Symposium on Logic in Computer Science (LICS \u201987), pp. 275\u2013279. IEEE Computer Society (1987)"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"Steen, A.: A reduction of input\/output logics to sat. J. Appl. Non-Classical Logics, 1\u201334 (2026)","DOI":"10.1080\/11663081.2026.2658659"},{"issue":"237","key":"27_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/mind\/LX.237.1","volume":"60","author":"GH Von Wright","year":"1951","unstructured":"Von Wright, G.H.: Deontic logic. Mind 60(237), 1\u201315 (1951)","journal-title":"Mind"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32589-1_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:02:40Z","timestamp":1784800960000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32589-1_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325884","9783032325891"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32589-1_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/ijcar","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}