Computer-assisted Proving by the PCS Method

Bruno Buchberger 

In: Proceedings of the Workshop on Constructive Algebra (M. Hazewinkel, ed.),
Amsterdam, Nov. 1-3, 2000. Lecture Notes in Computer Science, to appear, 14 pages



ABSTRACT:


Abstract: In this paper we describe Theorema, a system for supporting
mathematical proving by computer. The emphasis of the paper is on 
showing how, in many situations, proving can be reduced to solving 
in algebraic domains. We first illustrate this by known techniques, 
in particular the Gröbner bases technique. Then we go into the details 
of describing the PCS technique, a new technique that is particularly 
well suited for doing proofs in elementary analysis and similar areas 
in which the notions involved, typically, contain alternating quantifiers 
in their definitions. We conclude with a general view on the interplay 
between automated proving, solving, and simplifying.