Alberto Finzi and Fiora Pirri, Universit&eagrave; degli Studi di Roma "La Sapienza"; Ray Reiter, University of Toronto
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.