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