Intellektik: Technical report 92-08
Linear Deductive Planning
Gerd Große and Steffen Hölldobler and Josef Schneeberger
Recently, three approaches to deductive planning were developed, which solve
the technical frame problem without the need to state frame axioms explicitly.
These approaches are based on the linear connection method, an equational Horn
logic, and linear logic. At first glance these approaches seem to be very
different. In the linear connection method a syntactical condition --- each
literal is connected at most once --- is imposed on proofs. In the equational
logic approach situations and plans are represented as terms and
SLDE-resolution is applied as an inference rule. The linear logic approach is
a Gentzen style proof system without weakening and contraction rules. On
second glance, however, and as a consequence of the results rigourously proved
in this paper, it will turn that the three approaches are equivalent. They
are based on the very same idea that facts about a situation are taken as
resources which can be consumed and produced.