人工智能实验三_谓词公式化为子句集.pdfVIP

人工智能实验三_谓词公式化为子句集--第1页 实验三 化为子句集的九步法实验 一、实验目的 理解和掌握消解原理，熟悉谓词公式化为子句集的九个步骤，理解消解推理规则，能把 任意谓词公式转换成子句集。 二、实验原理 消解是可用于一定的子句公式的重要推理规则，任一谓词演算公式可以化成一个子句 集。通过九步法消解可以从这两个父辈子句推导出一个新子句。 九步法消解包括消去蕴涵符号、减否定符辖域、对变量标准化、消去存在量词、化为 前束型、化为合取范式、消去全程量词、消去合取符、更换变量名，依次变换即可得到子句 集。具体为： （1）消去连接词“→”和“↔” P→Q⇔﹁P∨QP↔Q⇔(P∧Q)∨(﹁P∧﹁Q) （2）将否定符号“﹁”移到仅靠谓词的位置 ﹁(﹁P)⇔P ﹁(P∧Q)⇔﹁P∨﹁Q ﹁(P∨Q)⇔﹁P∧﹁Q ﹁(∀x)P(x)⇔(∃x)﹁P(x) ﹁(∃x)P(x)⇔(∀x)﹁P(x) (∀x)(﹁(∀y)P(x,y)∨﹁(∀y)(﹁Q(x,y)∨R(x,y)))⇔(∀x)((∃y)﹁P(x,y)∨(∃y)(Q(x,y)∧﹁R(x,y))) （3）对变元标准化 (∀x)((∃y)﹁P(x,y)∨(∃z)(Q(x,z)∧﹁R(x,z))) （4）化为前束范式 (∀x)(∃y)(∃z)(﹁P(x,y)∨(Q(x,z)∧﹁R(x,z))) （5）消去存在量词 (∀x)(﹁P(x,f(x))∨(Q(x,g(x))∧﹁R(x,g(x)))) （6）化为Skolem标准形P∨(Q∧R)⇔(P∨Q)∧(P∨R) (∀x)((﹁P(x,f(x))∨Q(x,g(x))∧(﹁P(x,f(x))∨﹁R(x,g(x)))) （7）消去全称量词 (∀x)((﹁P(x,f(x))∨Q(x,g(x))∧(﹁P(x,f(x))∨﹁R(x,g(x)))) （8）消去合取词 ﹁P(x,f(x))∨Q(x,g(x)) ﹁P(x,f(x))∨﹁R(x,g(x)) （9）更换变量名称 ﹁P(x,f(x))∨Q(x,g(x)) ﹁P(y,f(y))∨﹁R(y,g(y)) 三、实验内容 （1）可以采用自己熟悉的C#、C++、JAVA等任一种语言编写出Windows应用程序，演示 子句消解推理演示程序。 （2）界面中可以通过实例按钮，由程序指定具体的实例，给出原始谓词公式； （3）设计九个步骤的按钮，每按一步按钮，给出这一步消解的结果； （4）该程序主要帮助初学者学习、掌握九步法谓词公式化为子句集的过程。 四、实验要求 （1）提交实验报告，以word文档形式“学号+姓名”命名； （2）报告中要有程序源代码； （3）有程序运行结果截图； （4）报告提交到：53/xstjzy/任建平/人工智能 人工智能实验三_谓词公式化为子句集--第1页