Open World Planning in the Situation Calculus

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Planning and Scheduling

We describe a forward reasoning planner for open worlds that uses domain specific information for pruning its search space. The planner is written in the situation calculus-based programming language GOLOG, and it uses a situation calculus axiomatization of the application domain. Given a sentence sigma to prove,the planner regresses it to an equivalent sentence sigma0 about the initial situation, then invokes a theorem prover to determine whether the initial database entails sigma0 and hence sigma. We describe 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. Finally, we report on our experiments with open world planning based on both these approaches to the theorem proving task.