论文部分内容阅读
计算机自动解几何问题,已经有不少研究成果。前推搜索法能够产生可读证明,因此也是应用较多的一种方法。在目前诸多算法中,一般是采用直接证明的方法。在手工证明几何问题的方法中,间接证明也是一种重要的方法,其中反证法是较为有效的方法之一。在计算机自动推理研究中,如何运用反证法,是自动推理中的一个难题,关于这方面的研究成果也少有报道。给出一个算法:根据命题的结论将命题分类,针对不同类型,设计不同的解决方案。有效地实现了反证法在自动推理中的运用。