【自动定理证明】石纯一.pdf
自动定理证明 石纯一编落 氯蒙出厥社
目 帐(1S 第一章一阶谓词逻辑81请词和个体词(S) 81函数和量词合式公式自然语句的形式化有限论域下公式(Vx)P(x),(x)P(x)的表示法普遍有效性和可满足性.1 判定何题.1 等值式1前束范式1推理演算.51调词逻辑的公理系统和自然演绎系统 第二章命题逻辑的定理证明,82王浩方法82归结(resolution)方法
前言 自动定理证明是人工智能的一个重要分支.人工智能”术语是在1956年于达特茅斯(Dartmouth)大学召开的学术会议上提出的,人工智能学科一般认为也是 1956年开始的.人工智能是研究使计算机能够完成表现出人类智能的任 务。中心课题是计算机实现智能的原理、制造类似于人脑的 智能计算机,以及使计算机更聪明些实现高层次的应用系 统.实现高层次的应用包括使机器由“知道干什么”提高到“知道怎么干”,由“数值计算”过渡到“符号处理”。而 符号处理主要不是靠推理而是强调知识,特别是专门领域的 独到的经验知识的获取、表示和利用.计算机会不会思维,或说机器能不能有智能,以及智能:是什么？