The PCS Prover in Theorema

Bruno Buchberger

In: Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided
Systems Theory - Formal Methods and Tools for Computer Science), Feb. 19-23,
2001, Las Palmas de Gran Canaria, (R. Moreno-Diaz, B. Buchberger, J.L. Freire eds.), 
Lecture Notes in Computer Science 2178,  2201,  pp. 469-478.
 
(ISSN 0302-9743, ISBN 3-540-42959-X. 
Copyright: Springer, Berlin - Heidelberg - New York.)




ABSTRACT:

We describe the PCS (Proving - Computing - Solving) method, a new method for automated 
theorem proving. The method is a heuristic approach that is particularly suited for proving
propositions about notions whose definitions involve alternating quantifiers ("for all ... 
there exists ... such that for all ... etc."). A typical example of such a notion is the 
notion of limit in elementary analysis.

By the PCS method, typically, proving reduces to solving in certain special domains. 
For example, the proof of propositions in elementary analysis often reduces to constraint 
solving over the real numbers. For this, we call a real number constraint solver, like 
Collins' algorithm, as a black box.

We explain the PCS method by going through the details of an example proof automatically 
generated by the method, namely the proof of the fact that the sequence f+g has limit
a+b if f has limit a and g has limit b.