"Event Calculus Planning Through Satisfiability"
Murray Shanahan and Mark Witkowski
Intelligent Systems and
Networks Group,
Department of Electrical and Electronic Engineering,
Imperial College,
Exhibition Road,
London SW7 2BT, U.K.
{m.shanahan, m.witkowski}@imperial.ac.uk
Abstract
Previous work on event calculus planning has viewed it as an abductive
task, whose implementation through abductive logic programming reduces to
partial order planning. By contrast, this paper presents a formal framework
for tackling event calculus planning through satisfiability, in the style
of Kautz and Selman. A provably correct conjunctive normal form encoding
for event calculus planning problems is supplied, rendering them soluble
by an off-the-shelf SAT solver.
Journal of Logic and Computation, accepted to appear