Model Reconciliation in Logic Programs

Abstract

Inspired by recent research in explainable planning, we investigate the model reconciliation problem between two logic programs $\pi _a$ and $\pi _h$, which represent the knowledge bases of an agent and a human, respectively. Given $\pi _a$, $\pi _h$, and a query q such that $\pi _a$ entails q and $\pi _h$ does not entail q (or $\pi _a$ does not entail q and $\pi _h$ entails q), the model reconciliation problem focuses on the question of how to modify $\pi _h$, by adding $\epsilon ^+ \subseteq \pi _a$ to $\pi _h$ and removing $\epsilon ^- \subseteq \pi _h$ from $\pi _h$ such that the resulting program $\hat{\pi }_h = (\pi _h{\setminus } \epsilon ^-) \cup \epsilon ^+$ has an answer set containing q (or has no answer set containing q). The pair $(\epsilon ^+,\epsilon ^-)$ is referred to as a solution for the model reconciliation problem $(\pi _a,\pi _h,q)$ (or $(\pi _a, \pi _h, \lnot q)$). We prove that, for a reasonable selected set of rules $\epsilon ^+ \subseteq \pi _a$ there exists a way to modify $\pi _h$ such that $\hat{\pi }_h$ is guaranteed to credulously entail q (or skeptically entail $\lnot q$). Given that there are potentially several solutions, we discuss different characterizations of solutions and algorithms for computing solutions for model reconciliation problems.

This research is partially supported by NSF grants 1757207, 1812619, 1812628, and 1914635.