一阶逻辑自动推理系统.doc

一阶逻辑自动推理系统一基础知识(1)定义1设t是LF(X)中的项,若t为常量或变元,则t为0元项,记为0-T;若t为fn(t1t2……tn)的形式,则t为n元项。(2)定义2设g是LF(X)中的广义文字,若g为如下形式:P(f1(f2(fm(t))))或ØP(f1(f2(fm(t))))这里P是LF(X)中的谓词符号,fi(i=12m)是LF(X)中的函数符号且fi(i=12 m)为0元或1元,t为常量或变元,且g中不含有蕴涵算子“®”,则称g为简单广义文字,称m为g的 复杂度。(3)定理1设g1,g2是LF(X)中的简单广义文字,且g1,g2分别为如下形式:P(f(f(f(a))))(k个f)ØP(f(f(f(x))))(k个f)这里k,l分别是g1,g2的复杂度,a是LF(X)中的常量,x是LF(X)中的变元,f是LF(X)中的函数符号。 如果k<l,则(g1g2)不是α-归结对。(4)定义3设C是LF(X)中的子句,且C为如下形式:g1Úg2ÚÚgn,其中gi(i=12n)为LF(X)中简单广义文字,则称C为简单广义子句。(5)定义4设S={C1C2Cm}是LF(X)中的子句集,若Ci(i=12m)为简单广义子句, 则称S为简单广义子句集。(6)定理2LF(X)中子句集S为α-不可满足的当且仅当存在S中子句的基例的有穷集合S′,S′是α-不可 满足的。(7)定理3设S为LF(X)中的子句集,S*是S经过基替换后得到的子句集,若S*是α-不可满足的,则S是α -不可满足的。(8)引理1LF(X)中的子句集S={C1C2Cm}是α-不可满足的当且仅当对于任意的piÎGi,存在 最一般合一σ,使得pσ1Ùpσ2ÙÙpσm£α,这里Gi是子句Ci中的广义文字集合。(9)定理4LF(X)中的子句集S为α-不可满足,当且仅当S的每一条路径上均有α-归结对,即对任意的 PiÎHi(i=12m),{P1P2Pm}中有α-归结对。(10)定理5设S=S1S2是LF(X)中的子句集,S1={C1C2Ck},S2={Ck+1Ck+2Cm}, 如果存在S的一条无α-归结对的前k元子路径R1,并且R1与子句集S2无α-归结对,则S为α-不可满 足的当且仅当S2为α-不可满足的(11)定理6将LF(X)中的子句集S中子句的次序调换或S中某个子句中文字的次序调换不改变S的α-不可 满足性和α-可满足性。二简单子句集的归结自动推理算法为了便于计算机程序的编制,首先对LF(X)中的子句集S进行如下的预处理:(1)定义一个二维数组C[m][n]来存储子句集S,其中n为子句集S中所有子句所含文字的最大数,则C[i]表示S中子句Ci;C[i][0]表示子句Ci广义文字的个数,C[i][j]表示子句Ci中第j个广义文字,iÎ{12m},jÎ{12n};(2)[i][j],Com[i][j]表示子句Ci中第j个广义文字的复杂度;(3)定义一个一维数组num[i],num[i]表示子句Ci中基广义文字的个数,num[θ[i]]表示子句Ci进行θ替换后生成的新的基广义文字的个数;(4)变量k用于标记当前子句的位置;(5)定义两个一维数组p[k]和R[n],用p[i]记录子