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

实验三 化为子句集的九步法实验

一、实验目的

理解和掌握消解原理，熟悉谓词公式化为子句集的九个步骤，理解消解推理规则，能把任意谓词公式转换成子句集。 二、实验原理

消解是可用于一定的子句公式的重要推理规则，任一谓词演算公式可以化成一个子句集。通过九步法消解可以从这两个父辈子句推导出一个新子句。

九步法消解包括消去蕴涵符号、减否定符辖域、对变量标准化、消去存在量词、化为前束型、化为合取范式、消去全程量词、消去合取符、更换变量名，依次变换即可得到子句集。具体为：

（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）报告提交到：ftp://192.168.129.253/xstjzy/任建平/人工智能

百度搜索“70edu”或“70教育网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读，70教育网，提供经典综合文库人工智能实验三_谓词公式化为子句集在线全文阅读。