人工智能归结原理实验报告-Toy模板网

这篇具有很好参考价值的文章主要介绍了人工智能归结原理实验报告。希望对大家有所帮助。如果存在错误或未考虑完全的地方，请大家不吝赐教，您也可以点击"举报违法"按钮提交疑问。

归结原理实验

一、实验目的

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

二、实验内容

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

A1 ： (∀x)(P(x)→(Q(x) ∧R(x))) 
A2 ： (∀x)(P(x)∧S(x)) 
G ： (∃x)(S(x)∧R(x))

要证明：G 是 A1 和 A2 的逻辑结果
归结原理是一种推理规则。从谓词公式转化为字句集的过程中看出，在子句
集中字句之间是合取关系，其中只要有一个字句不可满足，则字句集就不可满足。
若一个字句集中包含空字句，则这个字句集一定是不可满足的。归结原理就是基
于这一认识提出来的。
应用归结原理进行定理证明的过程：
设要被证明的定义表示为：
A1∧A2∧…∧An→B
(1)首先否定结论 B，并将否定后的公式¬B 与前提公式集组成如下形式的谓
词公式：G= A1∧A2∧…∧An∧¬B。
(2)求谓词公式 G 的字句集 S。
(3)应用归结原理，证明子句集 S 的不可满足性。

三、实验环境

Visual Studio Code

四、实验步骤

步骤一 设计谓词公式的存储结构，即内部表示，注意对全称量词x 和存在
量词x 可采用其他符号代替。
原符号替换符号
全称量词∀ @
存在量词∃ #
析取符号∨ |
合取符号∧ &
取反符号¬ ~
蕴含符号→ >
例如 A1 ： (∀x)(P(x)→(Q(x) ∧R(x))) ，输入的时候要替换为 A1 ：
(@x)(P(x)>(Q(x)&R(x)))。
核心代码如下所示：

namespace FormulaNamepace {
// 公式符号定义
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'};
}
#endif // SUBSENTENCE_H

步骤二 变换子句集，可按以下过程变换，变换过程的核心代码如下所示：
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()); // 查找蕴含前件
 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);
// 移除否定符号
leftDonePart.erase(find(leftDonePart.begin(),
leftDonePart.end(), NEGATION));
string rightPart(iter + 5, f.end());
// 否定内移
rightPart.insert(rightPart.begin(), NEGATION);
// 递归处理右部分
MoveNegation(rightPart);
string(leftDonePart + rightPart).swap(f);
return f;
}else { // 修饰着多个公式，形如~(P(x)|Q(x))
iter = f.insert(iter+2, NEGATION); // 内移否定符号
while(1) {
iter = FindFormula(iter, f.end());
assert(iter != f.end() && "No Predicate Formula!");
FormulaIter iter2 = FindPairChar(
iter, f.end(), '(', ')');
++iter2;
if(IsConnector(*iter2)) {
*iter2 == DISJUNCTION ? *iter2 = CONJUNCTION
 : *iter2 = DISJUNCTION;
iter = f.insert(iter2+1, NEGATION);
}else
break;
}
f.erase(find(f.begin(), f.end(),
NEGATION));// 清除原否定符号
return MoveNegation(f);
}
}else if(*(iter+1) == NEGATION) {// 两个否定，直接相消
f.erase(iter, iter + 2);
return MoveNegation(f); // 重新处理
}else {
iter = find(iter + 1, f.end(), NEGATION);
} }
return f;
}

3、适当改名使量词间不含同名指导变元，对变元标准化。

Formula& StandardizeValues(Formula& f)
{
set<char> checkedAlpha;
FormulaIter iter = FindQuantifier(f.begin(), f.end());
while(iter != f.end()) {
char varName = *++iter;// 获取变量名
if(checkedAlpha.find(varName) == checkedAlpha.end()) {
checkedAlpha.insert(varName);
}else { // 变量名冲突了，需要改名
// 获取新名字
char newName = FindNewLowerAlpha(checkedAlpha);
// 查找替换右边界
FormulaIter rightBorder = FindPairChar(
iter + 2, f.end(), '(', ')');
// 将冲突变量名替换为新的名字
*iter = newName;
replace(iter, rightBorder, varName, newName);
iter = rightBorder; // 移动到新的开始
}
iter = FindQuantifier(iter, f.end());
}
return f;
}

4、化为前束范式。

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;
}

5、消去存在量词。

Formula& RemoveEQ(Formula& f)
{
set<char> checkedAlpha;
FormulaIter eqIter = find(f.begin(), f.end(), EQ);
if(eqIter == f.end()) return f;
FormulaRevIter uqIter = find(FormulaRevIter(eqIter), f.rend(), UQ);
if(uqIter == f.rend()) { // 该存在量词前没有任意量词
char varName = *(eqIter + 1);
char newName = GetNewConstantAlha(f);
auto rightBound = FindPairChar(eqIter + 3, f.end(), '(', ')');
assert(rightBound != f.end());
replace(eqIter + 3, rightBound, varName, newName); // 常量化
f.erase(eqIter - 1, eqIter + 3); // 移除存在量词
}else {
// 记录公式中已经存在的字母
copy_if(f.begin(), f.end(),
inserter(checkedAlpha, checkedAlpha.begin()),
ptr_fun<int, int>(isalpha));
const char oldName = *(eqIter+1);
// 准备任意量词的函数来替换该存在量词
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); // 递归处理
}

6、消去全称量词。

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;
}

7、化为 Skolem 标准型。

Formula& TransformToSkolem(Formula& f)
{
RemoveEQ(f);
RemoveUQ(f);
return f;
}

8、消去合取词，以子句为元素组成一个集合 S。

void ExtractSubsentence(SubsentenceSet& subset,
const Formula& f)
{
auto leftIter = f.begin(),
middleIter = find(f.begin(), f.end(), CONJUNCTION);
while(middleIter != f.end()) {
subset.insert(string(leftIter, middleIter));
leftIter = middleIter + 1;
middleIter = find(middleIter + 1, f.end(), CONJUNCTION);
}
subset.insert(string(leftIter, middleIter));
}

需要考虑子句、子句集的存储结构的设计。
步骤三 选择并设计归结策略，常用的归结策略有：
删除策略、支持集策略、线性归结策略、输入归结策略、单元归结策略、锁
归结策略、祖先过滤型策略等。
步骤四实现归结算法，并在其中实现合一算法，使用归结原理进行定理证
明，要求采用归结反演过程，即：
1、先求出要证明的命题公式的否定式的子句集 S； 2、然后对子句集 S（一次或者多次）使用归结原理；
3、若在某一步推出了空子句，即推出了矛盾，则说明子句集 S 是不可满足
的，从而原否定式也是不可满足的，进而说明原公式是永真的。
合一算法及核心代码如下：
1、置 k＝0，Sk＝S， σk ＝ε；
2、若 Sk 只含有一个谓词公式，则算法停止， σk 就是最一般合一；
3、求 Sk 的差异集 Dk； 4、若中存在元素 xk 和 tk ，其中 xk 是变元， tk 是项且 xk 不在 tk 中出现，
则置 Sk ＋1＝Sk{tk/ xk} σk ＝ε然后转 Step2； 5、算法停止，S 的最一般合一不存在。

Sustitutes MGU(const FormulaNamepace::Subsentence& subsent1,
const FormulaNamepace::Subsentence& subsent2)
{
pair<Subsentence, Subsentence> 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;
}

步骤五 编写代码，调试程序

五、实验结果与分析

实验结果图
人工智能归结原理实验报告
实验结果：
输入：

2
(@x)(P(x)>(Q(x)&R(x)))
(@x)(P(x)&S(x))
(#x)(S(x)&R(x))

输出：

谓词公式的个数：2
第1个谓词公式: (@x)(P(x)>(Q(x)&R(x)))
第2个谓词公式: (@x)(P(x)&S(x))
逻辑结论为：(#x)(S(x)&R(x))
合并后的谓词公式：
(@x)(P(x)>(Q(x)&R(x)))&(@x)(P(x)&S(x))&~(#x)(S(x)&R(x))

消去蕴含：
(@x)(~P(x)|(Q(x)&R(x)))&(@x)(P(x)&S(x))&~(#x)(S(x)&R(x))

处理否定：
(@x)(~P(x)|(Q(x)&R(x)))&(@x)(P(x)&S(x))&(@x)(~S(x)|~R(x))

变元标准化：
(@x)(~P(x)|(Q(x)&R(x)))&(@l)(P(l)&S(l))&(@r)(~S(r)|~R(r))

消去存在：
(@x)(~P(x)|(Q(x)&R(x)))&(@l)(P(l)&S(l))&(@r)(~S(r)|~R(r))

化为前束范式：
(@x)(@l)(@r)(~P(x)|(Q(x)&R(x)))&(P(l)&S(l))&(~S(r)|~R(r))

化为 Skolem 标准型：
(~P(x)|(Q(x)&R(x)))&(P(l)&S(l))&(~S(r)|~R(r))

化为合取范式：
(~P(x)|Q(x))&(~P(x)|R(x))&P(l)&S(l)&(~S(r)|~R(r))

子句集：
(1) ~P(x)|Q(x)
(2) ~P(x)|R(x)
(3) P(l)
(4) S(l)
(5) ~S(r)|~R(r)
归结:

归结策略1：

(6) ~R(r)          	[ (4),(5) { r/l } ]
(7) ~P(r)          	[ (2),(6) { r/x } ]
(8) Nil            	[ (3),(7) { r/l } ]
成功

归结策略2：

(6) Q(x)           	[ (3),(1) { x/l } ]
(7) R(x)           	[ (3),(2) { x/l } ]
(8) ~S(r)|~P(x)    	[ (5),(2) { x/r } ]
(9) ~R(r)          	[ (5),(4) { l/r } ]
(10) ~P(x)|~S(r)    	[ (2),(5) { r/x } ]
(11) ~S(r)          	[ (5),(7) { x/r } ]
(12) Nil            	[ (9),(7) { x/r } ]
成功

实验分析：归结采用水平归结，从尾部开始进行，即从结论出发开始遍历寻找相应结论的逆命题直至close表归结为Nill（空），此时结论证明成功。采用的是支持集策略。

六、实验总结

利用归结反演方法来证明定理的具体步骤为：
步1否定目标公式G，得到¬G；
步2将¬G并入到公式集F1＾F2＾．．．＾Fn中；
步3将公式集化子句集，得到子句集S；
步4对S进行归结，每次归结的结果并入到S中。如此反复，直到得到空子句为止。此时，就证明了在前提F1＾F2＾．．．＾Fn为真时，结论G为真。
支持集策略
（1）每次归结时，两个亲本子句中至少要有一个是目标公式否定的子句或其后裔。
（2）目标公式否定的子句及其后裔即为支持集。
特点
（1）尽量避免在可满足的子句集中做归结，因为从中导不出空子句。而求证公式的前提通常是一致的，所以支持集策略要求归结时从目标公式否定的子句出发进行归结。支持集策略实际是一种目标制导的反向推理。
（2）支持集策略是完备的。