用带条件重写技术证明几何定理

PROVING GEOMETRY THEOREMS BASED ON CONDITIONAL REWRITING TECHNIQUES

本文研究了带条件的重写技术在几何定理证明中的应用问题.采用按情形分析的技术,使得归纳模式中所要考虑的变量数目大为减少.此外,我们还给出了一组推理规则,实验例子表明,它们对几何定理可以进行有效的自动证明.

This paper shows how to apply conditional rewriting techniques to prove geometry theorems. We reduce the number of induction variables in inductive proof schema by case analysis. Furthermore, we propose a set of inference rules which can make automatic geometry theorem proving more efficient.