A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering

摘要

We report our effort to build a geometry deductive database, which can be used to find the fixpoint for a geometric configuration. The system can find all the properties of the configuration that can be deduced using a fixed set of geometric rules. To control the size of the database, we propose the idea of a structured deductive database. Our experiments show that this technique could reduce the size of the database by one hundred times. We propose the data-based search strategy to improve the efficiency of forward chaining. We also make clear progress in the problems of how to select good geometric rules, how to add auxiliary points, and how to construct numerical diagrams as models automatically. The program is tested with l60 nontrivial geometry configurations. For these geometric configurations, the program not only finds most of their well-known properties but also often gives unexpected results, some of which are possibly new. Also, the proofs generated by the program are generally short and totally geometric.