Automatic discovery of geometry theorems using minimal canonical comprehensive Gröbner systems. (English) Zbl 1195.68093

Montes, Antonio; Recio, Tomás

Botana, Francisco (ed.) et al., Automated deduction in geometry. 6th international workshop, ADG 2006, Pontevedra, Spain, August 31–September 2, 2006. Revised papers. Berlin: Springer (ISBN 978-3-540-77355-9/pbk). Lecture Notes in Computer Science 4869. Lecture Notes in Artificial Intelligence, 113-138 (2007).

Summary: The main proposal in this paper is the merging of two techniques that have been recently developed. On the one hand, we consider a new approach for computing some specializable Gröbner basis, the so called Minimal Canonical Comprehensive Gröbner Systems (MCCGS) that is – roughly speaking – a computational procedure yielding “good” bases for ideals of polynomials over a field, depending on several parameters, that specialize “well”, for instance, regarding the number of solutions for the given ideal, for different values of the parameters. The second ingredient is related to automatic theorem discovery in elementary geometry. Automatic discovery aims to obtain complementary (equality and inequality type) hypotheses for a (generally false) geometric statement to become true. The paper shows how to use MCCGS for automatic discovering of theorems and gives relevant examples.
For the entire collection see [Zbl 1132.68006].

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30	Symbolic computation and algebraic computation
51-04	Software, source code, etc. for problems pertaining to geometry

Keywords:

automatic discovering; comprehensive Gröbner system; automatic theorem proving; canonical Gröbner system

Software:

CoCoA