Technical report: Intellektik 91-24
An Implementation of Setheo on a Transputer System and its Adaptation to Deductive Planning
U. Egly and S. Sanguanpong
In this paper, we present an implementation of Setheo on a transputer system
and its adaptation to deductive plan generation. After a brief overview of
Setheo's architecture, the concept of linear proofs \cite{bib86} is
introduced. Using Setheo as our deductive vehicle, a normal form
transformation of the problem description is necessary, which gives rise to
several difficulties \cite{fro87}.
Additionally, examples show that the ability of a prover to find linear proofs
depends on the search strategy. Several strategies are examined and it turns
out that a PROLOG--like strategy is not able to detect linear proofs in some
cases. Fortunately, there is a deductive planning approach which does not have
any of the problems mentioned above. This approach is based on the
representation of plans and situations as terms, on an AC1--unification
algorithm, and on the SLD--resolution as an inference rule.
Finally, two well--known examples demonstrates the ability to use \setheo
for deductive planning tasks.