|
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 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 oe to prove, the planner regresses it to an equivalent sentence oe 0 about the initial situation, then invokes a theorem prover to determine whether the initial database entails oe 0 and hence oe. 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., |
