自动推理中反证法的研究

摘要

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