Many practical problems can be understood as the search for a state of affairs that extends a fixed partial state of affairs, the \emph{environment}, while satisfying certain conditions that are formally specified. Such problems are found in, e.g., 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.

翻译：许多实际问题可理解为在固定部分事态（即“环境”）基础上，寻找满足形式化约束条件的事态扩展。此类问题广泛存在于工程、法律或经济学等领域中。本文研究当用户在搜索初始阶段未知环境相关部分信息时的这类问题。在搜索过程中，用户可能考虑包含对这些未知信息隐式假设的试探性解决方案。为确保解的正确性，必须通过观测环境验证这些假设。此外，我们假设用户不仅具备解的构成知识，还拥有环境的一般性规律知识。我们形式化定义具有足够已验证事实以保证完整且适当解存在的部分解，并提出一种交互式系统辅助用户搜索：1）确定试探性解中哪些隐式假设必须在环境中验证；2）确定哪些观测能为搜索提供有用信息。最后，我们提出一种高效方法对相关信息集进行超近似，并评估了实现效果。