-
PLATIN A Planning System for Inductive Theorem Proving Implementation and Experiences
(1997)
- This paper provides a description of PLATIN. With PLATIN we present an imple-mented system for planning inductive theorem proofs in equational theories that arebased on rewrite methods. We provide a survey of the underlying architecture ofPLATIN and then concentrate on details and experiences of the current implementa-tion.
-
Extending automatic theorem proving by planning
(1993)
- A general concept for combining planning with automatic theorem provingis introduced. From this a system architecture based on the notion of planningtrees, methods and sensors is developed. It is illustrated by examples taken fromthe domain of sorting algorithms.
