{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:01:21Z","timestamp":1747173681467,"version":"3.40.5"},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2023,8,8]],"date-time":"2023-08-08T00:00:00Z","timestamp":1691452800000},"content-version":"unspecified","delay-in-days":38,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2023,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Many practical problems can be understood as the search for a state of affairs that extends a fixed partial state of affairs, the <jats:italic>environment<\/jats:italic>, while satisfying certain conditions that are formally specified. Such problems are found in, for example, engineering, law or economics. We study this class of problems in a context where some of the relevant information about the environment is not known by the user at the start of the search. During the search, the user may consider tentative solutions that make implicit hypotheses about these unknowns. To ensure that the solution is appropriate, these hypotheses must be verified by observing the environment. Furthermore, we assume that, in addition to knowledge of what constitutes a solution, knowledge of general laws of the environment is also present. We formally define partial solutions with enough verified facts to guarantee the existence of complete and appropriate solutions. Additionally, we propose an interactive system to assist the user in their search by determining (1) which hypotheses implicit in a tentative solution must be verified in the environment, and (2) which observations can bring useful information for the search. We present an efficient method to over-approximate the set of relevant information, and evaluate our implementation.<\/jats:p>","DOI":"10.1017\/s1471068423000261","type":"journal-article","created":{"date-parts":[[2023,8,8]],"date-time":"2023-08-08T06:49:10Z","timestamp":1691477350000},"page":"648-663","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Interactive Model Expansion in an Observable Environment"],"prefix":"10.1017","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7074-1870","authenticated-orcid":false,"given":"PIERRE","family":"CARBONNELLE","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"JOOST","family":"VENNEKENS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MARC","family":"DENECKER","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3460-4251","authenticated-orcid":false,"given":"BART","family":"BOGAERTS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2023,8,8]]},"reference":[{"key":"S1471068423000261_ref3","unstructured":"Carbonnelle, P. , Vandevelde, S. , Vennekens, J. and Denecker, M. 2022. IDP-Z3: A reasoning engine for FO(.). CoRR, abs\/2202.00343."},{"key":"S1471068423000261_ref13","unstructured":"Mitchell, D. G. , Ternovska, E. , Hach, F. and Mohebali, R. 2006. Model expansion as a framework for modelling and solving search problems. Technical Report TR 2006-24, Simon Fraser University, Canada."},{"key":"S1471068423000261_ref5","doi-asserted-by":"crossref","unstructured":"de Moura, L. M. and Bj\u00f8rner, N. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Ramakrishnan, C. R. and Rehof, J. , Eds., vol. 4963. Lecture Notes in Computer Science. Springer, 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"S1471068423000261_ref12","unstructured":"Madsen, J. N. 2003. Methods for interactive constraint satisfaction. Master\u2019s thesis, Department of Computer Science, University of Copenhagen."},{"key":"S1471068423000261_ref2","unstructured":"Bowen, J. and Bahler, D. 1991. Conditional existence of variables in generalised constraint networks. In Proceedings of the 9th National Conference on Artificial Intelligence, Dean, T. L. and McKeown, K. R. , Eds. AAAI Press, 215\u2013220."},{"key":"S1471068423000261_ref15","unstructured":"OMG. 2021. Decision Model and Notation (DMN). URL: https:\/\/www.omg.org\/dmn\/. [Accessed on February 22, 2021]."},{"key":"S1471068423000261_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(97)00075-1"},{"key":"S1471068423000261_ref11","unstructured":"Jansen, J. , Bogaerts, B. , Devriendt, J. , Janssens, G. and Denecker, M. 2016. Relevance for SAT(ID). In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI, New York, NY, USA, 9\u201315 July 2016. IJCAI\/AAAI Press, 596\u2013602."},{"key":"S1471068423000261_ref6","doi-asserted-by":"crossref","unstructured":"Deryck, M. , Vennekens, J. , Devriendt, J. , and Marynissen, S. 2019. Legislation in the knowledge base paradigm: Interactive decision enactment for registration duties. In 13th IEEE International Conference on Semantic Computing, ICSC 2019, Newport Beach, CA, USA, January 30 \u2013 February 1, 2019. IEEE, 174\u2013177.","DOI":"10.1109\/ICOSC.2019.8665543"},{"volume-title":"Distributed Constraint Satisfaction: Foundations of Cooperation in Multi-agent Systems","year":"2012","author":"Yokoo","key":"S1471068423000261_ref20"},{"key":"S1471068423000261_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-415817-7.00006-2"},{"key":"S1471068423000261_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2021.115869"},{"key":"S1471068423000261_ref14","unstructured":"Mittal, S. and Falkenhainer, B. 1990. Dynamic constraint satisfaction problems. In Proceedings of the 8th National Conference on Artificial Intelligence, Shrobe, H. E. , Dietterich, T. G. , and Swartout, W. R. , Eds. AAAI Press\/The MIT Press, 25\u201332."},{"key":"S1471068423000261_ref4","doi-asserted-by":"crossref","unstructured":"Cimatti, A. , Griggio, A. and Sebastiani, R. 2007. A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. In Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, Marques-Silva, J. and Sakallah, K. A. , Eds., vol. 4501. Lecture Notes in Computer Science. Springer, 334\u2013339.","DOI":"10.1007\/978-3-540-72788-0_32"},{"key":"S1471068423000261_ref7","unstructured":"Falkner, A. A. , Haselb\u00f6ck, A. , Krames, G. , Schenner, G. and Taupe, R. 2019. Constraint solver requirements for interactive configuration. In Proceedings of the 21st Configuration Workshop, Hotz, L. , Aldanondo, M. , and Krebs, T. , Eds., vol. 2467. CEUR Workshop Proceedings, 65\u201372."},{"key":"S1471068423000261_ref16","doi-asserted-by":"crossref","unstructured":"Stumptner, M. and Haselb\u00f6ck, A. 1993. A generative constraint formalism for configuration problems. In Proceedings of Advances in Artificial Intelligence, Torasso, P. , Ed., vol. 728. Lecture Notes in Computer Science. Springer, 302\u2013313.","DOI":"10.1007\/3-540-57292-9_68"},{"key":"S1471068423000261_ref19","first-page":"1","article-title":"Tackling the DM challenges with cDMN: A tight integration of DMN and constraint reasoning","volume":"23","author":"Vandevelde","year":"2021","journal-title":"Theory and Practice of Logic Programming"},{"key":"S1471068423000261_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32409-4_3"},{"key":"S1471068423000261_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-415817-7.00015-3"},{"volume-title":"Knowledge-Based Configuration: From Research to Business Cases","year":"2014","author":"Felfernig","key":"S1471068423000261_ref9"},{"key":"S1471068423000261_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068416000156"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068423000261","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,27]],"date-time":"2024-02-27T09:38:23Z","timestamp":1709026703000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068423000261\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,7]]}},"alternative-id":["S1471068423000261"],"URL":"https:\/\/doi.org\/10.1017\/s1471068423000261","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2023,7]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}