Handbook of Automated Reasoning

4 AI approaches to automated reasoning in geometry

Generally speaking, the algebraic approaches are decision procedures and are more powerful. The AI approaches are not decision procedures and are less powerful. Despite its “weakness”, it is still worth improving the AI approach because this may lead to techniques useful to automated reasoning in the general case. Even for automated geometry reasoning alone, AI methods have the following advantages. (1) Proofs produced by the AI method are generally easy to understand than proofs based on algebraic computations. (2) Using predicates only (no algebraic computation) makes the reaching of fixpoint possible. (3) Although algebraic methods can prove a much larger number of theorems, there still ...