Extending automatic theorem proving by planning Inger Sonntag, Joerg Denzinger Fachbereich Informatik, Universitaet Kaiserslautern Postfach 3049, W-6750 Kaiserslautern, GERMANY E-mail: {sonntag,denzinge}@informatik.uni-kl.de Abstract A general concept for combining planning with automatic theorem proving is introduced. From this a system architecture based on the notion of planning trees, methods and sensors is developed. It is illustrated by examples taken from the domain of sorting algorithms. Keywords Theorem prover, Automated reasoning, Proof planning, Inductive theorem proving, Equational theory, Term rewriting systems, Verification, Sorting algorithms Source anonymous FTP server ftp.uni-kl.de [131.246.94.94] path: /reports_uni-kl/computer_science/SEKI/1993/papers/ file: Sonntag.SR-93-02.english.ps.Z