谓词公式和命题公式一样.PPT

* * * * 证明：由定理2.2知，公式G必有与之等价的前束范式，设G的前束范式为：G=(Q1x1)(Q2x2)…(Qnxn)M(x1,x2, …xn) (1).如果Qi是存在量词，且Qi的左边没有全称量词，则直接用一个常量符号a来取代xi在M中的一切出现，且该a不同于M中的任何其他常量符号； (2).如果Qi是存在量词，且Qi的左边有全称量词(任意xj)，(任意xl)，…(任意xk)，则直接用一个函数f(xj, xl, …xk)来取代xi在M中的一切出现，该函数符号f不同于M中的任何其他函数符号； (3).如果Qi是全称量词，则直接用一个变量符号x来取代xi在M中的一切出现，且该变量x不同于M中的任何其他变量符号： (4).反复使用上述(1), (2), (3)，可消去前束范式中的所有存在量词的全称量词，此时得到的公式为该公式的Skolem标准形，且该标准形显然不于原公式等价。 * 2.4 一阶逻辑的推理 2.4.2推理规则的应用 一般情况下，总是假定相同的个体域(即全总个体域)下进行的。 (1).推理过程中，可以直接引用：前提引入、结论引入、置换、CP等规则以及谓词逻辑中的等价式和永真蕴含式导出的规则； (2).可以引用UI，EI规则消去量词，此时量词必须位于整个公式的最前端，且其辖域延伸到公式的末端； (3).可以引用UG，EG规则加入量词； 2.4 一阶逻辑的推理 (4).在推理过程中，如既要使用UI规则，又要使用EI规则消去量词，而且选用的个体是同一个符号，则必须先使用规则EI，再使用规则UI； (5).如果一个变量是用规则EI消去量词，对该变量在添加量词时，则只能使用规则EG，而不能使用规则UG，如使用规则UI消去量词，对该变量在添加量词时，则可使用规则EG和UG。 2.4 一阶逻辑的推理 2.4.3举例 例2-26：证明苏格拉底三段论。 例2-27：证明下述论断的正确性：所有的哺乳动物都是脊椎动物；并非所有的哺乳动物都是胎生动物。故有些脊椎动物不是胎生的。 例2-28：给出下面推理的证明： 前提： 结论： 2.4 一阶逻辑的推理 例2-29：构造下面推理的证明： 前提： 结论： 例2-30：证明下面论断的正确性。 有些学生相信所有的老师，任何一个学生都不相信骗子。所以，教师都不是骗子。 2.4 一阶逻辑的推理 例2-31：用反证法证明： 例2-32：证明： 2.5 谓词逻辑在计算机科学中的应用 2.5.1谓词逻辑与数据库语言 1张二维表可表示一个n元有序组的集合，可以用一个n元特性谓词来刻划：某元组属于二维表的充要条件是给其对应的谓词为真 如： F(x, y)=N(x) ∧(x=y) 即{(x, y)|F(x, y)}。 x y 1 1 2 2 3 3 … … 2.5 谓词逻辑在计算机科学中的应用 对数据库而言，基本操作插入，删除等； 此外，修改，选择等都可以用谓词公式来表示，因而，可以用谓词逻辑这一工具来研究关系数据库。 基本操作 关系代数 逻辑公式 插入 R∨S {(x1, …xn)|P(x1, …xn) ∨Q(x1, …xn)} 删除 R-S {(x1, …xn)|P(x1, …xn) ∧?Q(x1, …xn)} 2.5 谓词逻辑在计算机科学中的应用 2.5.2谓词逻辑与逻辑程序设计语言 我们知道谓词逻辑是不可判定的，但1965年美国数理逻辑学家罗宾逊Robinson，证明了谓词逻辑的“半可判定性”，即在谓词逻辑中存在一种算法，只要公式是永真的，就能用此算法推出，他们使用的算法叫消解原理，1972年法国马赛大学的Colmerauer设计了一种逻辑程序设计语言，Prolog语言，实现了消解法。 现实世界=谓词逻辑表示=Prolog程序=计算机实现 2.5 谓词逻辑在计算机科学中的应用 1.子句和子句集 谓词公式→斯科林范式→子句集→Horn子句 (1).谓词公式→斯科林范式，一个命题公式； (2).斯科林范式：化为合取范式，将每个合取项用蕴含式表示，这种蕴含式称为子句； (3).一个公式总可以用一组子句来表示，每个子句具有单一的蕴含形式，公式是永真的，则该子句集中的每一个子句永真。 2.5 谓词逻辑在计算机科学中的应用 例2-34：求下公式的子句集。 例2-35：试将“每个人都犯错误”用子句形式表示。 例2-36：试将祖先关系“父母是祖先，祖先的祖先是祖先”用子句集表示。 2.5 谓词逻辑在计算机科学中的应用 2.消解原理 在公理系统中，有公理和定理两部分，公理是已知的永真公式，定理是要求证明的永真公式，公理可用子句集表示，设子句