Automated theorem provers normally need interaction with the user to be successful on non-trivial problems. To enhance the degree of automation for a prover the domain of interest is drastically restricted and knowledge about this domain of interest is integrated into the control component of the prover. Such knowledge may consist of typical proof methods and frequently used proof schemes. Therefore the usage of such provers even in very similar domains necessitates major changes in the prover. In PLATIN we propose an architecture for proof-planning that allows one to easily introduce knowledge about the domains of interest and that is to a large extent independent of the basic prover. The knowledge about a domain of interest is represented in such a way that it can be used to decompose the problem into several subproblems. This decomposition of the problem can be repeated until the subproblems become so small that they can be handled by the basic prover, called verifier.
Inger Sonntag and Jörg Denzinger, ``Extending automatic theorem proving by planning'', SEKI-Report SR-93-02, University of Kaiserslautern, Kaiserslautern (Germany), 1993
Robert Eschbach , Wolfgang Jekeli and Carlo Reiffers, ``Implementation of PLATIN'', yet unpublished