PLATIN A Planning System for Inductive Theorem Proving Implementation and Experiences
Robert Eschbach, Inger Sonntag · 1997
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.