归结原理 人工智能-VisualStudio《实验二归结原理实验》实验步骤步骤

实验二归结原理实验

一、实验目的

加深学生对归结原理进行定理证明过程的理解，掌握基于谓词逻辑的归结过程中子句变换过程、替换与合一算法和归结策略等重要环节，进一步了解实现机器自动定理证明的步骤。

二、实验内容

对于任意一阶谓词逻辑描述的定理，给出基于归结原理的证明过程。如输入：

A1 ： ("x)(P(x)®(Q(x) ÙR(x)))

A2 ： ("x)(P(x) Ù S(x))

G ： ($x)(S(x)ÙR(x))

要证明：G是A1和A2的逻辑结果。

三、实验环境

推荐使用C++语言，编译器推荐使用Microsoft Visual Studio Professional 2019(version=16.3.8)。

四、实验原理

归结原理是一种推理规则。从谓词公式转化为子句集的过程中看出，在子句集中子句之间是合取关系，其中只要有一个子句不可满足，则子句集就不可满足。若一个子句集中包含空子句，则这个子句集一定是不可满足的。归结原理就是基于这一认识提出来的。

应用归结原理进行定理证明的过程：

设要被证明的定义表示为：

A1∧A2∧…∧An→B

(1)首先否定结论B，并将否定后的公式¬B与前提公式集组成如下形式的谓词公式：G= A1∧A2∧…∧An∧¬B。

(2)求谓词公式G的子句集S。

(3)应用归结原理，证明子句集S的不可满足性。

五、实验步骤

步骤一设计谓词公式的存储结构，即内部表示，注意对全称量词"x和存在量词$x可采用其他符号代替。

原符号

替换符号

全称量词∀

@

存在量词∃

#

析取符号∨

|

合取符号∧

&

取反符号¬

~

蕴含符号→

>

例如A1 ： ("x)(P(x)®(Q(x) ÙR(x)))，输入的时候要替换为A1：(@x)(P(x)>(Q(x)&R(x)))。

核心代码如下所示：

typedef string Formula; //谓词公式
typedef vector SubsentenceSet;
typedef map SubsentenceMap;
typedef string::iterator FormulaIter;  //迭代器
typedef string::reverse_iterator FormulaRevIter;  //反向迭代器
typedef vector::iterator VectorIter;
typedef vector::reverse_iterator VectorReIter;
map m1;
int clause[20]; // 用这个来记录被删除的子句
/*("x)(P(x)®(Q(x) ÙR(x)))，输入的时候要替换为A1：(@x)(P(x)>(Q(x)&R(x)))。*/
// 公式符号定义
const char EQ = '#';          // 存在量词符号
const char UQ = '@';          // 全称量词符号
const char IMPLICATION = '>'; // 蕴含符号
const char NEGATION = '~';    // 否定符号
const char CONJUNCTION = '&'; // 合取符号
const char DISJUNCTION = '|'; // 析取符号
const char CONSTANT_ALPHA[] = {'a', 'b', 'c', 'd', 'e',
                               'i', 'j', 'k'};

步骤二 变换子句集，可按以下过程变换，变换过程的核心代码如下所示：

1、消去蕴含连接词。

FormulaRevIter GetBeginOfFormula(FormulaRevIter position,FormulaRevIter rend){
	//考虑用栈来找到蕴含前件
	int location;
	bool isFormula=true;//判断是不是蕴含前件是一个整体还是一个公式，公式是true，整体是false
	stack seek; //创建一个栈
	++position; //逆向回退1
	while(position!=rend){ //循环没有结束
		if(*position.base()==')') //如果是‘)’入栈
			seek.push(*position.base());
		if(seek.size()>1)
			isFormula=false;    //说明括号不止一个，是个整体
		if(*position.base()=='(') //如果是'('出栈
			seek.pop();
		if(seek.empty()==1){ //如果栈为空,说明已经找完了蕴含前件了
			if(isFormula)
				return position; //这里需要注意一下 正向迭代器与反向迭代器之间的关系
			else
				return position-1;
		}
		position++;
	
	}
	return rend;//要么返回第一个字符的位置
}
// 1、消去蕴含连接词。
Formula& RemoveImplication(Formula& f)
{
	FormulaIter iter;
	while((iter = find(f.begin(), f.end(), IMPLICATION))   //找蕴含符号
					!= f.end()) {
		*iter = DISJUNCTION; // 将蕴含符号替换为析取符号
		FormulaRevIter revIter(iter);
        revIter =
			GetBeginOfFormula(revIter, f.rend()); // 查找蕴含前件   //发f,rend()正数第一个字符
        iter = revIter.base()-1;// 反向迭代器到正向迭代器转换需要减1
		f.insert(iter, NEGATION);	// 在前件前面插入否定
	}
	return f;
}

2、将否定符号移到紧靠谓词的位置。

Formula& MoveNegation(Formula& f)
{
	FormulaIter iter = find(f.begin(), f.end(), NEGATION);
	while(iter != f.end()) {
		if(*(iter+1) == '(') {// 否定不是直接修饰谓词公式，需要内移
			// 否定符号修饰着带量词的谓词公式
			if(*(iter+2) == EQ || *(iter+2) == UQ) {
				// 量词取反
				*(iter+2) == EQ ? *(iter+2) = UQ : *(iter+2) = EQ;
				string leftDonePart(f.begin(), iter+5);
				// cout<

Formula& StandardizeValues(Formula& f)
{
	set checkedAlpha;
	FormulaIter iter = FindQuantifier(f.begin(), f.end());
	while(iter != f.end()) {
		char varName = *++iter;	// 获取变量名
		if(checkedAlpha.find(varName) == checkedAlpha.end()) {  //如果set里面没有该变量名字，就加入
			checkedAlpha.insert(varName);
		}else {	// 变量名冲突了，需要改名
			// 获取新名子
			char newName = FindNewLowerAlpha(checkedAlpha);
			checkedAlpha.insert(newName); //这里在源代码的基础上加入一个 要加入新生成的变量名字
			// 查找替换右边界
			FormulaIter rightBorder = FindPairChar(
									iter + 2, f.end(), '(', ')');
			// 将冲突变量名替换为新的名子
			*iter = newName;
			replace(iter, rightBorder, varName, newName);
			iter = rightBorder;	// 移动到新的开始
		}
		iter = FindQuantifier(iter, f.end());
	}
	// 调试
	// for (set::iterator it = checkedAlpha.begin(); it != checkedAlpha.end(); it++)
	// 	cout << *it << " ";
	return f;
}

Formula& TransformToPNF(Formula& f)
{
     FormulaIter iter = FindQuantifier(f.begin(), f.end());
     if(iter == f.end())
            return f;
     else if(iter-1 == f.begin()) { // 量词已经在最前面
            iter += 3;
            string leftPart(f.begin(), iter);
            string rightPart(iter, f.end());
            TransformToPNF(rightPart);  // 递归处理右部分
            (leftPart + rightPart).swap(f);
     }else {    // 量词在内部，需要提到前面
            string quantf(iter-1, iter+3);   // 保存量词
            f.erase(iter-1, iter+3);      // 移除量词
            f.insert(f.begin(), quantf.begin(), quantf.end());
            return TransformToPNF(f);     // 继续处理
     }
     return f;
}

Formula& RemoveEQ(Formula& f)
{
	set checkedAlpha;
	FormulaIter eqIter = find(f.begin(), f.end(), EQ);  //找到存在量词的位置
	if(eqIter == f.end()) return f;
	FormulaRevIter uqIter = find(FormulaRevIter(eqIter), f.rend(), UQ);  //反向迭代器还要减一
	// cout<<"我在测试此时的是啥"<<*uqIter<(isalpha));
		const char oldName = *(eqIter+1);  //eqIter是存在量词的位置，这个得到函数值
		// 准备任意量词的函数来替换该存在量词
		const char funcName = FindNewLowerAlpha(checkedAlpha);
		string funcFormula;
		funcFormula = funcFormula + funcName
						+ '(' + *(uqIter-1) + ')';
		f.erase(eqIter - 1, eqIter + 3);	// 移除存在量词
		ReplaceAlphaWithString(f, oldName, funcFormula);  //在这里产生替换
	}
	// RemoveOuterBracket(f); //这个函数不知道要干啥，感觉没有必要要了，不知道啥含义，我看网上人家也没要
	return RemoveEQ(f);	// 递归处理
}

Formula& RemoveUQ(Formula& f)
{
	FormulaIter uqIter = find(f.begin(), f.end(), UQ);
	while(uqIter != f.end()) {
		uqIter = f.erase(uqIter-1, uqIter+3); // 直接移除全称量词
		uqIter = find(uqIter, f.end(), UQ); // 继续扫描
	}
	// RemoveOuterBracket(f); //这个函数不知道要干啥，感觉没有必要要了，不知道啥含义，我看网上人家也没要
	return f;
}

Formula& TransformToSkolem(Formula& f)
{
	RemoveEQ(f);
	cout<<"6.1消去存在量词："<

Sustitutes MGU(const FormulaNamepace::Subsentence& subsent1,
                          const FormulaNamepace::Subsentence& subsent2)
{
     pair w = { subsent1, subsent2 };
     Sustitutes mgu;
     while(w.first != w.second) { // w未合一
            // 找不一致集
            auto iter1 = FindPredicate(w.first.begin(), w.first.end());
            auto iter2 = FindPredicate(w.second.begin(), w.second.end());
            while(iter1 != w.first.end() && iter2 != w.second.end()) {
                   if(*iter1 != *iter2)
                          break;
                   iter1 = FindPredicate(iter1 + 1, w.first.end());
                   iter2 = FindPredicate(iter2 + 1, w.second.end());
            }
            // 找到不一致集合
            if(iter1 != w.first.end() && iter2 != w.second.end()) {
                   string item1 = GetPredicate(iter1,  w.first.end());
                   string item2 = GetPredicate(iter2,  w.second.end());
                   // 不允许置换有嵌套关系
                   if(StrStr(item1, item2) != item1.end() ||
                          StrStr(item2, item1) != item2.end()) {
                                 throw ResolutionException("cannot unifier");
                   }
                   // 只允许常量替换变量
                   if(!IsConstantAlpha(*iter1))
                          item1.swap(item2);
                   // 更新置换，然后置换子句集
                   Sustitutes sustiSet = { make_pair(item1, item2) };
                   mgu = ComposeSustitutes(mgu, sustiSet);
                   Substitution(w.first, mgu);
                   Substitution(w.second, mgu);
            }
            else {     // 两子句不可合一
                   throw ResolutionException("cannot unifier");
            }
     }
     return mgu;
}