命题逻辑_No2.pdf

命题逻辑 （The Propositional Logic） 张文生 研究员 中国科学院自动化研究所 自动定理证明 n Automated Theorem Proving(ATP) n 定理机器证明(Mechanical Theorem Proving) n 为什么? n 定理证明是一种智能行为; n 体现了人类的逻辑推理能力; n 推理用计算来实现; n Leibniz的梦想 n Leibniz imagined a universal formal calculus which could express reasoning in any subject, and an algorithmic procedure which could be applied to decide truth of statements in this calculus. n 1930年, Herbrand定理. n 半可判定问题. n 一阶逻辑的判定问题. n 在一阶逻辑中, 有没有方法可以判断任何一个命题是 否定理? (有没有方法可以判断任何一个公式能不能从 公理及推理规则推导出来). n 数理逻辑的基本问题. n 1936年, 证明基本问题是不可解的. n 在一阶逻辑中, 如果一个定理是正确的, 则有一个机械的 方法在有限步内证明它. n 一阶谓词逻辑有很强的表达能力, 凡可计算的函数就可由 一阶谓词表达. 历史 n Newell, Shaw, Simon. n 1956年, The logic theory machine(逻辑理 论机). n 数学定理证明程序(Logic Theorist). n mimic human reasoning. n 《数学原理》第二章中的38个定理. n 1963年，经过改进的LT程序在一部更大的 电脑上，最终完成了第二章全部52条数学定 理的证明. n 王浩 n 1958年, IBM704 电脑, 3-5分钟, 证明了《数 学原理》中有关命题演算的全部220条定理. n 1959年, 8.4分钟, 证明了《数学原理》中全 部（350条以上）定理. n 罗素：“我真希望，在怀特海和我浪费了10 年的时间用手算来证明这些定理之前，就知 道有这种可能。” n 1983年获得首届自动定理证明里程碑奖. 四色定理 n 1852年, 一位21岁的大学生提出来的数学难题： 任何地图都可以用最多四种颜色着色，就能区 分任何两相邻的国家或区域. n 1976年6月，美国伊利诺斯大学, W.Haken, K. Appel. n 3台IBM360 电脑 n 1200个机时，200亿个逻辑判断 n ??? n 《伊利诺斯数学杂志》第21卷刊载的检验表(460p) 三类方法 n 基于归结的方法 n 类人的方法(human simulation) n 判定方法 基于归结的方法 n 1960年, Gilmore在计算机上实现了Herbrand算 法. n 1960年, M.Davis和H.Putnam的改进: n Tautology Rule, One-literal Rule, Pure-literal Rule, Splitting Rule. n 技巧而非本质: 枚举基替换. n 1960年, D.Prawitz n 直接寻找替换, 避免组合爆炸. n 思想深刻, 效果不理想. n 1965年, J.A.Robinson提出归结原理 n One-literal Rule的扩展. n 效率的提高 n 1965: Wos, G.A.Robinson, Curson, 支持集归结; n 1967: Slagle, 语义归结; n 1970: Lov