归结原理实验

一、实验目的

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

二、实验内容

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

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）支持集策略是完备的。

实验指导书

参考文献:

人工智能归结原理实验
基于谓词逻辑的归结原理研究

代码