Event Calculus Planning Through Satisfiability
Murray Shanahan and Mark Witkowski
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.