一阶逻辑自动推理系统

《一阶逻辑自动推理系统》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、一阶逻辑自动推理系统一基础知识（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）定

2、理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

3、F(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中的广义文字集合

4、。（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中某个子句中文字的次序调

5、换不改变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）定义一个二维数组Com[i][j]，Com[i][j]表示子句Ci中第j个广义文字的复杂度；（3）定义一个

6、一维数组num[i]，num[i]表示子句Ci中基广义文字的个数，num[θ[i]]表示子句Ci进行θ替换后生成的新的基广义文字的个数；（4）变量k用于标记当前子句的位置；（5）定义两个一维数组p[k]和R[n]，用p[i]记录子句Ck中当前搜索位置，而R[12k]来储存在S中目前的路径（k表示路径的有效长度）；（6）定义与二维数组C[i][j]相对应的变量t[i][j](iÎ{12m}，jÎ{12n}），在同一路径上的t[i][j]=1的两个广义文字是α-归结对；(7)定义与C[i]相对

7、应的数组t[i]，用于保存子句C[i]中所对应的t[i][j]；(8)定义一个二维数组G[i][p[i]]，G[i][p[i]]表示子句Ci中当前路径p[i]的所有基例。详细的算法如下：（1）置循环变量k=0，p(0)=1，t[i][j]=0，R[0]=C[0][p[0]]。（2）判断是否存在路径R[12m]上广义文字对应的t[i][j]全为0。（2.1）若存在，则选择这样路径中复杂度最高的基广义文字C[i][j]，此时会出现两种情况：（2.1.1）这样的广义文字存在多个，则选择将C[i][j]作为初

8、始文字，G[i][p[i]]=：G[i][p[i]]{C[i][j]}，转到第（4）步；（2.1.2）这样的广义文字若不存在，则转到（3.2）。（2.2）若不存在，则S是α-不可满足的且输出G[i][p[i]]，算法结束。（3）在S中选定C[k]（3.1）若S中含有基广义文字，则在S中选定这样的子句C[i]：A.C[i]中含有最复杂的基广义文字C[i][j]；B.满足条件A的最短的子句，G[i][