论文部分内容阅读
本文研究了带条件的重写技术在几何定理证明中的应用问题.采用按情形分析的技术,使得归纳模式中所要考虑的变量数目大为减少.此外,我们还给出了一组推理规则,实验例子表明,它们对几何定理可以进行有效的自动证明.
In this paper, we study the application of conditional rewriting in the proof of geometric theorem, and use the case-by-case analysis technique to reduce the number of variables to be considered in the induction mode.In addition, we also present a set of inference rules, Experimental examples show that they can be validated automatically and efficiently for geometric theorems.