Constructive algebra and systems theory
Bernard Hanzon, Michiel Hazewinkel · Data Archiving and Networked Services (DANS) · 2006
In this chapter we describe Theorema, a system for supporting mathematical proving by computer. The emphasis of the chapter 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 Grobner 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. 1. ALGEBRA, ALGORITHMS, PROVING 1.1. An algebraic notion: Grobner bases We start with a typical algebraic definition, the definition of the concept of “Grobner basis” which, in the notation of our Theorema system [2,3], looks like this: Definition [ “Grobner basis”, any[F ], is-Grobner-basis[F ] :⇐⇒ ∀ f∈Ideal[F ] f →F ∗ 0 ] . Here, →F ∗ denotes the algorithmic reduction (division) relation on polynomials modulo sets F of multivariate polynomials. The notion of Grobner basis turned out to be important for polynomial ideal theory because many ideal theoretic problems can be solved “easily” if Grobner bases generating the ideals involved are known