自动定理证明

来自计算思维百科
跳转至: 导航搜索

数学领域中对臆测的定理寻求一个证明,一直被认为是一项需要智能才能完成的任务。证明定理时,不仅需要有根据假设进行演绎的能力,而且需要有某些直觉的技巧。例如数学家在求证一个定理时,会熟练地运用他丰富的专业知识,猜测应当先证明哪一个引理,精确判断出已有的哪些定理将起作用,并把主问题分解为若干子问题,分别独立进行求解。因此人工智能研究中机器定理证明很早就受到注视,并取得不少成果。自动定理证明在人工智能的研究中是一个极其重要的领域。如基于谓词演算的推理自动化研究,使我们更清楚地理解某些推理的细节。许多非数学领域的问题,如医疗诊断、信息检索、规划制定和难题求解,都可以像定理证明问题那样进行形式化,从而转化为一个定理证明问题。因此,自动定理证明在人工智能研究中起着重要作用。自动定理证明的方法通常有自动演绎法、决策过程法和定理证明器。