Proving Goal Achievability

Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference (KR2008)

Volume

Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference (KR2008)

Contents

Given an action theory, a goal, and a set of initial states, we consider the problem of checking whether the goal is always achievable in every initial state of the set. To address this problem, we introduce a notion of reduction between sets of states, and show that if the set of the initial states can be reduced to one of its subsets, then the problem is equivalent to checking whether the goal is achievable in every initial state of the subset, provided that all the variables in the goal, if any, are existentially quantified, and that the preconditions and effects of the actions can be specified by quantifier-free formulas. We believe that this result provides an effective way of proving goal achievability, and illustrate it through some examples.