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