Collins' Cylindrical Algebraic Decomposition method (CAD) can be used to prove geometry theorems that involve order relation (that is, the algebraic form consists of polynomial equalities and inequalities). Unfortu- nately only very simple geometric statements can be proved this way, as the method is very time consuming. To overcome the slowness of Collins' CAD method for complicated polynomials we propose a method (section 4) that combines the area method for computing geometric quantities and the CAD method. We present an implementation of this method as part of the Geom- etry Prover in the frame of the Theorema project.
| Original language | English |
|---|
| Title of host publication | Knowledge Engineering: Principles and Techniques |
|---|
| Editors | Horia F. Pop |
|---|
| Pages | 307-315 |
|---|
| Number of pages | 9 |
|---|
| Publication status | Published - 2007 |
|---|
| Name | Studia Universitatis "Babes-Bolyai", Series Informatica |
|---|
- 101 Mathematics
- 101001 Algebra
- 101005 Computer algebra
- 101009 Geometry
- 101012 Combinatorics
- 101013 Mathematical logic
- 101020 Technical mathematics