谓词逻辑与归结原理2

#include

#include

#include

#define null 0

typedef struct

{

char var;

char *s;

}mgu;

void strreplace(char *string,char *str1,char *str2)

{

char *p;

while(p=strstr(string,str1))

{

int i=strlen(string);

int j=strlen(str2);

*(string+i+j-1)='\0';

for(int k=i-1;(string+k)!=p;k--)

*(string+k+j-1)=*(string+k);

for(i=0;i

*(p++)=*(str2+i);

}

}

void sort(mgu *u,int count)

{

int j=count;

int k=j;

if(count==1)return;

for(int i=1;i

{

if(!((u+i)->s))

continue;

if((u+i)->var==(u+j)->var)

{

delete (u+j)->s;

(u+j)->s=null;

k--;

j=i;

}

if(((u+i)->s)&&((u+i)->var==*((u+i)->s)))

{

delete (u+i)->s;

(u+i)->s=null;

k--; }

}

j=count;

if(k==j)return;

count=k;

for(int i=1;i0;i++)

{

if((u+i)->s)

continue;

while(!((u+j)->s))

j--;

(u+i)->var= (u+j)->var;

- 1 - 谓词逻辑定义

谓词逻辑是一种用来描述事物真假性的语言，它的核心是谓词（Predicate）和符号表示法，它可以用来表达自然语言中的复杂概念和描述一些事实及其关系。谓词逻辑是一种强大的数学模型，可以用来表示我们对自然现象的知识，并且可以推断出未来的情况。

谓词逻辑的发展源自上世纪六十年代，受到欧几里得的哲学思想的启发，以便为数学模型提供更完整的语言。它发展成为一种用来描述事物的语言，可以用来描述一些事实及其关系，实现机器模拟思维的目的，它主要用于计算机科学领域，其他领域如哲学也有广泛的应用。

谓词逻辑通过谓词（predicates）来描述一般状况和条件，它是一种抽象的数学语言，可以表达自然语言中的复杂概念，以符号表示法来表达一些有关真假性的概念，并通过推断技术来完成其任务。

谓词逻辑由以下几个部分组成：

1.尔谓词：它是一些布尔谓词（Boolean predicates），用来描述一般状况和条件，比如P（x），Q（x），R（x）等等。

2.号表示：谓词逻辑使用比较简单的符号表示法，以表达一些有关真假性的概念，比如“&”（且），“”（否定），“∨”（或）等等。

3.词逻辑语句（Logical Sentences）：谓词逻辑语句是谓词逻辑中使用的一种有用结构，它由谓词和符号表示法组成，可以表达一些真假性概念。

4.型：谓词逻辑的模型是一种强大的数学模型，它可以用来描述 - 2 - 自然现象的知识，它可以用来表达一些事实及其关系（fact and

relationship）。

谓词逻辑的最大优势在于它是一种可以描述一些有关真假性的复杂概念的语言，它不但可以用来表达自然语言中的复杂概念，也可以用来描述一些事实及其关系，实现机器模拟思维的目的，从而实现机器智能。

谓词逻辑使用比较简单的符号表示法，可以表达一些有关真假性的概念，可以用来计算机科学中的解释和推理，可以用来描述一些事实及其关系，实现机器模拟思维的目的，也可以用于哲学等其他领域。

谓词逻辑

王剑

定义: 一个公式，若它的所有量词均非否定地出现在公式的最左

边，而它们的辖域一直延伸到公式之末，且公式中不出现联

接词“”及“”，则此种形式的公式称前束范式。

EX1 :

(1) xyz (P(x) ∨Q(y)∧R(x, z))

(2) xyz ((P(x,y)∧(Q(x))) ∨(R(y,z)∨(Q(x))))

都是前束范式。§2.5谓词演算中的范式（前束范式和斯柯林范式）前束范式和斯柯林范式

定理任一谓词公式都可以化成为与之等值的前束范式。

任一公式化归为前束范式的过程如下:

1. 消去联结词, 。

2. 将联结词向内深入, 使之只作用于原子公式。

3. 利用换名或代入规则使所有约束变元的符号均不同, 并且自由变

元与约束变元的符号也不同。

4. 利用量词辖域的扩张和收缩律, 将所有量词以在公式中出现的顺

序移到公式最前面, 扩大量词的辖域至整个公式。前束范式和斯柯林范式

EX2: 求公式A：(x P(x)∨y Q(y)) x R(x)的前束范式。

解:A (xP(x)∨yQ(y))∨xR(x)

消去联结词

(xP(x)∧yQ(y))∨xR(x)

德.摩根律

(xP(x)∧yQ(y))∨zR(z)

换名

xy z ((P(x)∧Q(y))∨R(z))

量词辖域扩张

EX3：求公式(xP(x,y) yQ(y))xR(x,y)的前束范式

解原式(xP(x,t) yQ(y)) xR(x,t) 代入

(xP(x,t) yQ(y)) zR(z,t)换名

(xP(x,t)∨yQ(y))∨zR(z,t)消去联结词

(xP(x,t)∧yQ(y))∨zR(z,t)向内深入

(xP(x,t)∧yQ(y))∨zR(z,t)量词转换

x(P(x,t)∧yQ(y))∨zR(z,t)量词辖域扩张

xy(P(x,t)∧Q(y))∨zR(z,t)量词辖域扩张

２００２年第６期　微机发展　４７　

使用ＸＭＬ的一阶谓词逻辑归结原理　

Ｒｅｓｏｌｕｔｉｏｎ　Ｍｅｔｈｏｄ　Ｕｓｉｎｇ　ＸＭＬ　ｉｎ　Ｆｉｒｓｔ——ｏｒｄｅｒ　Ｐｒｅｄｉｃａｔｅ　Ｌｏｇｉｃ　文章编号：１００５—３７５１（２００２）０６—００４７—０６　

谢铉洋，谢荣传（安徽大学计算机科学与工程系，安徽合肥，２３００３９）　

ＸＩＥ　Ｘｕａｎ—ｙａｎｇ，ＸＩＥ　Ｒｏｎｇ—ｃｈｕａｎ（Ｄｅｐｔ．ｏｆ　Ｃｏｍｐｕｔｅｒ　Ｓｃｉ．ａｎｄ　Ｅｎｇ．，Ａｎｈｕｉ　Ｕｎｉｖ．，Ｈｅｆｅｉ　ＡＨ　２３００３９，Ｃｈｉｎａ）　

摘要：归结原理（ｒｅｓｏｌｕｔｉｏｎ　ｐｒｉｎｃｉｐｌｅ）是计算机自动推理的重　

要原理之一。将ＸＭＬ加入到使用归结原理的证明过程中，　利用ＸＭＬ结构与语义自描述的特性，简化归结过程的计算　

机实现。并给出相应基于ＸＭＬ的算法。　关键词：可延伸标示语言；归结原理；不一致集　

Ａｂｓｔｒａｃｔ：Ｒｅｓｏｌｕｔｉｏｎ　ｐｒｉｎｃｉｐｌｅ　ｉｓ　ｏｎｅ　ｏｆ　ｔｈｅ　ｍｏｓｔ　ｉｍｐｏｒｔａｎｔ　ｐｒｉｎｃｉ—　ｐｉｅｓ　ｉｎ　ａｕｔｏｍａｔｉｃ　ｄｅｄｕｃｔｉｏｎ．Ｉｎｔｅｇｒａｔｅ　ＸＭＬ　ｉｎｔｏ　ｔｈｉｓ　ｐｒｏｃｅｄｕｒｅ．　

Ｂｙ　ｕｔｉｌｉｚｉｎｇ　ｔｈｅ　ｓｔｒｕｃｔｕｒｅ　ａｎｄ　ｓｅｍａｎｔｉｃ　ｓｅｌｆ—ｄｅｓｃｒｉｐｔｉｏｎ　ｆｅａｔｕｒｅｓ　

ｏｆ　ＸＭＬ，ｗｅ　ｃａｎ　ｓｅｅ　ｔｈａｔ　ｔｈｅ　ｒｅｓｏｌｕｔｉｏｎ　ｐｒｏｃｅｓｓ　ａｎｄ　ｃｏｍｐｕｔｉｎｇ　ｅｆｆｉｃｉｅｎｃｙ　ｗｉｌｌ　ｂｅ　ｆａｃｉｌｉｔａｔｅｄ．Ｔｈｅ　ＸＭＬ—ｂａｓｅｄ　ａｌｇｏｒｉｔｈｍ　ａｌｓｏ　

ｗｉｌｌｈｅ　ｇｉｖｅｎ．　

Ｋｅｙ　ｗｏｒｄｓ：ＸＭＬ；ｒｅｓｏｌｕｔｉｏｎ　ｐｒｉｎｃｉｐｌｅ；ｄｉｓａｇｒｅｅｍｅｎｔ　ｓｅｔ　

收稿日期：２００２一Ｏ２一Ｏ６　作者简介：谢铉洋（１９７８一），男，安徽合肥人，硕士研究生，主要研究方　向为数据库与ｌｎｔｅｍｅｔ应用；谢荣传（１９４６一），男。安徽宿县人，副教　授，硕士生导师，主要研究方向为效据库与多媒体技术。