Reasoning about actions: a model-theoretic approach

A knowledge-based agent reasons with its knowledge and answers queries while performing various tasks. We consider the case where we describe the agent's knowledge in a propositional fragment of the situation calculus and queries in a fragment of ID-logic, the extension of first-order logic with inductive definitions. This fragment of ID-logic is equivalently as expressive as the alternation-free mu calculus. We formulate the agent's reasoning process as the following question: does the representation T of the agent's knowledge logically entail the query Q? We provide an efficient algorithm for this task, using a model-theoretic approach: we construct from T a canonical model M of the agent's knowledge and ask whether M satisfies Q. Using this approach, the agent can answer the query in time linear with respect to both the size of T and the size of Q.