Previous: TR 91-21 Next: TR 92-02

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.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry