Requirement-Based Cooperative Theorem Proving                   

Dirk Fuchs
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, 67653 Kaiserslautern
Germany
E-mail: dfuchs@informatik.uni-kl.de

Abstract
We examine an approach for demand-driven cooperative 
theorem proving. We briefly point out the problems arising
 from the use of common success-driven cooperation methods, 
and we propose the application of our approach of 
requirement-based cooperative theorem proving. This 
approach allows for a better orientation on current needs 
of provers in comparison with conventional cooperation
concepts. We introduce an abstract framework for 
requirement-based cooperation and describe two 
instantiations of it: Requirement-based exchange of 
facts and sub-problem division and transfer via
requests. Finally, we report on experimental studies 
conducted in the areas superposition and unfailing 
completion.

Keywords
theorem proving, cooperation, requirements