Interactive Model Expansion in an Observable Environment

Pierre Carbonnelle, Joost Vennekens, Marc Denecker, Bart Bogaerts

Research output: Contribution to journalArticlepeer-review


Many practical problems can be understood as the search for a state of affairs that extends a fixed partial state of affairs, the environment, 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.

Original languageEnglish
Pages (from-to)648-663
Number of pages16
JournalTheory and Practice of Logic Programming
Issue number4
Publication statusPublished - 2023

Bibliographical note

Funding Information:
This research received funding from the Flemish Government under the “Onderzoeksprogramma Artificiële Intelligentie (AI) Vlaanderen” program.

Publisher Copyright:
© The Author(s), 2023. Published by Cambridge University Press.


Dive into the research topics of 'Interactive Model Expansion in an Observable Environment'. Together they form a unique fingerprint.

Cite this