Open World Planning in the Situation Calculus

Abstract

We describe a forward reasoning planner for open worlds that uses domain specific information for pruning its search space, as suggested by (Bacchus & Kabanza 1996; 2000). The plan-ner is written in the situation calculus-based programming language GOLOG, and it uses a situation calculus axiomati-zation of the application domain. Given a sentence to prove, the planner regresses it to an equivalent sentence about the initial situation, then invokes a theorem prover to determine whether the initial database entails and hence . We de-scribe two approaches to this theorem proving task, one based on compiling the initial database to prime implicate form, the other based on Relsat, a Davis/Putnam-based procedure. Fi-nally, we report on our experiments with open world planning based on both these approaches to the theorem proving task.