PLATIN: A Planning System for Inductive Theorem Proving -
Implementation and Experiences

Robert Eschbach, Inger Sonntag
Fachbereich Informatik
Universitaet Kaiserslautern
Postfach 3049
D-67653 Kaiserslautern
e-mail: eschbach@informatik.uni-kl.de
        sonntag@informatik.uni-kl.de

Abstract
This paper provides a description of PLATIN. With PLATIN we present an
implemented system for planning inductive theorem proofs in equational
theories that are based on Rewrite-methods. We provide a survey of the
underlying architecture of PLATIN and then concentrate on details and
experiences of the current implementation. 

Keywords
theorem proving, inductive theorem proving, planning, proof planning
Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1997/
file: Eschbach.SR-97-02.ps.gz