歸結(jié)原理實(shí)驗(yàn)
一、實(shí)驗(yàn)?zāi)康?/h4>
加深學(xué)生對歸結(jié)原理進(jìn)行定理證明過程的理解，掌握基于謂詞邏輯的歸
結(jié)過程中子句變換過程、替換與合一算法即歸結(jié)策略等重要環(huán)節(jié)，進(jìn)一步了解實(shí)
現(xiàn)機(jī)器自動(dòng)定理證明的步驟。
二、實(shí)驗(yàn)內(nèi)容
對于任意一階謂詞邏輯描述的定理，給出基于歸結(jié)原理的證明過程。如輸入：
A1 ： (?x)(P(x)→(Q(x) ∧R(x)))
A2 ： (?x)(P(x)∧S(x))
G ： (?x)(S(x)∧R(x))
要證明：G 是 A1 和 A2 的邏輯結(jié)果
歸結(jié)原理是一種推理規(guī)則。從謂詞公式轉(zhuǎn)化為字句集的過程中看出，在子句
集中字句之間是合取關(guān)系，其中只要有一個(gè)字句不可滿足，則字句集就不可滿足。
若一個(gè)字句集中包含空字句，則這個(gè)字句集一定是不可滿足的。歸結(jié)原理就是基
于這一認(rèn)識(shí)提出來的。
應(yīng)用歸結(jié)原理進(jìn)行定理證明的過程：
設(shè)要被證明的定義表示為：
A1∧A2∧…∧An→B
(1)首先否定結(jié)論 B，并將否定后的公式?B 與前提公式集組成如下形式的謂
詞公式：G= A1∧A2∧…∧An∧?B。
(2)求謂詞公式 G 的字句集 S。
(3)應(yīng)用歸結(jié)原理，證明子句集 S 的不可滿足性。
三、實(shí)驗(yàn)環(huán)境
Visual Studio Code
四、實(shí)驗(yàn)步驟
步驟一 設(shè)計(jì)謂詞公式的存儲(chǔ)結(jié)構(gòu)，即內(nèi)部表示，注意對全稱量詞x 和存在
量詞?x 可采用其他符號(hào)代替。
原符號(hào) 替換符號(hào)
全稱量詞? @
存在量詞? #
析取符號(hào)∨ |
合取符號(hào)∧ &
取反符號(hào)? ~
蘊(yùn)含符號(hào)→ >
例 如 A1 ： (?x)(P(x)→(Q(x) ∧R(x))) ， 輸 入 的 時(shí) 候 要 替 換 為 A1 ：
(@x)(P(x)>(Q(x)&R(x)))。
核心代碼如下所示：
namespace FormulaNamepace {
// 公式符號(hào)定義
const char EQ = '#'; // 存在量詞符號(hào)
const char UQ = '@';// 全稱量詞符號(hào)
const char IMPLICATION = '>'; // 蘊(yùn)含符號(hào)
const char NEGATION = '~'; // 否定符號(hào)
const char CONJUNCTION = '&';// 合取符號(hào)
const char DISJUNCTION = '|'; // 析取符號(hào)
const char CONSTANT_ALPHA[] = { 'a', 'b', 'c', 'd', 'e',
'i', 'j', 'k'};
}
#endif // SUBSENTENCE_H
步驟二 變換子句集，可按以下過程變換，變換過程的核心代碼如下所示：
1、消去蘊(yùn)含連接詞。
Formula& RemoveImplication(Formula& f)
{
FormulaIter iter;
while((iter = find(f.begin(), f.end(), IMPLICATION))
!= f.end()) {
*iter = DISJUNCTION; // 將蘊(yùn)含符號(hào)替換為析取符號(hào)
FormulaRevIter revIter(iter);
revIter =
GetBeginOfFormula(revIter, f.rend()); // 查找蘊(yùn)含前件
iter = revIter.base()-1;// 反向迭代器到正向迭代器轉(zhuǎn)換需要減 1
f.insert(iter, NEGATION);// 在前件前面插入否定
}
return f;
}
2、將否定符號(hào)移到緊靠謂詞的位置。
Formula& MoveNegation(Formula& f)
{
FormulaIter iter = find(f.begin(), f.end(), NEGATION);
while(iter != f.end()) {
if(*(iter+1) == '(') {// 否定不是直接修飾謂詞公式，需要內(nèi)移
// 否定符號(hào)修飾著帶量詞的謂詞公式
if(*(iter+2) == EQ || *(iter+2) == UQ) {
// 量詞取反
*(iter+2) == EQ ? *(iter+2) = UQ : *(iter+2) = EQ;
string leftDonePart(f.begin(), iter+5);
// 移除否定符號(hào)
leftDonePart.erase(find(leftDonePart.begin(),
leftDonePart.end(), NEGATION));
string rightPart(iter + 5, f.end());
// 否定內(nèi)移
rightPart.insert(rightPart.begin(), NEGATION);
// 遞歸處理右部分
MoveNegation(rightPart);
string(leftDonePart + rightPart).swap(f);
return f;
}else { // 修飾著多個(gè)公式，形如~(P(x)|Q(x))
iter = f.insert(iter+2, NEGATION); // 內(nèi)移否定符號(hào)
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));// 清除原否定符號(hào)
return MoveNegation(f);
}
}else if(*(iter+1) == NEGATION) {// 兩個(gè)否定，直接相消
f.erase(iter, iter + 2);
return MoveNegation(f); // 重新處理
}else {
iter = find(iter + 1, f.end(), NEGATION);
} }
return f;
}
3、適當(dāng)改名使量詞間不含同名指導(dǎo)變元，對變元標(biāo)準(zhǔn)化。
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; // 移動(dòng)到新的開始
}
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()) { // 量詞已經(jīng)在最前面
iter += 3;
string leftPart(f.begin(), iter);
string rightPart(iter, f.end());
TransformToPNF(rightPart); // 遞歸處理右部分
(leftPart + rightPart).swap(f);
}else { // 量詞在內(nèi)部，需要提到前面
string quantf(iter-1, iter+3); // 保存量詞
f.erase(iter-1, iter+3); // 移除量詞
f.insert(f.begin(), quantf.begin(), quantf.end());
return TransformToPNF(f); // 繼續(xù)處理
}
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 {
// 記錄公式中已經(jīng)存在的字母
copy_if(f.begin(), f.end(),
inserter(checkedAlpha, checkedAlpha.begin()),
ptr_fun<int, int>(isalpha));
const char oldName = *(eqIter+1);
// 準(zhǔn)備任意量詞的函數(shù)來替換該存在量詞
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); // 繼續(xù)掃描
}
RemoveOuterBracket(f);
return f;
}
7、化為 Skolem 標(biāo)準(zhǔn)型。
Formula& TransformToSkolem(Formula& f)
{
RemoveEQ(f);
RemoveUQ(f);
return f;
}
8、消去合取詞，以子句為元素組成一個(gè)集合 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));
}
需要考慮子句、子句集的存儲(chǔ)結(jié)構(gòu)的設(shè)計(jì)。
步驟三 選擇并設(shè)計(jì)歸結(jié)策略，常用的歸結(jié)策略有：
刪除策略、支持集策略、線性歸結(jié)策略、輸入歸結(jié)策略、單元?dú)w結(jié)策略、鎖
歸結(jié)策略、祖先過濾型策略等。
步驟四實(shí)現(xiàn)歸結(jié)算法，并在其中實(shí)現(xiàn)合一算法，使用歸結(jié)原理進(jìn)行定理證
明，要求采用歸結(jié)反演過程，即：
1、先求出要證明的命題公式的否定式的子句集 S； 2、然后對子句集 S（一次或者多次）使用歸結(jié)原理；
3、若在某一步推出了空子句，即推出了矛盾，則說明子句集 S 是不可滿足
的，從而原否定式也是不可滿足的，進(jìn)而說明原公式是永真的。
合一算法及核心代碼如下：
1、置 k＝0，Sk＝S， σk ＝ε；
2、若 Sk 只含有一個(gè)謂詞公式，則算法停止， σk 就是最一般合一；
3、求 Sk 的差異集 Dk； 4、若中存在元素 xk 和 tk ，其中 xk 是變元， tk 是項(xiàng)且 xk 不在 tk 中出現(xiàn)，
則置 Sk ＋1＝Sk{tk/ xk} σk ＝ε然后轉(zhuǎn) 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());
// 不允許置換有嵌套關(guān)系
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;
}
步驟五 編寫代碼，調(diào)試程序
五、實(shí)驗(yàn)結(jié)果與分析
實(shí)驗(yàn)結(jié)果圖
實(shí)驗(yàn)結(jié)果：
輸入：
2
(@x)(P(x)>(Q(x)&R(x)))
(@x)(P(x)&S(x))
(#x)(S(x)&R(x))
輸出：
謂詞公式的個(gè)數(shù)：2
第1個(gè)謂詞公式: (@x)(P(x)>(Q(x)&R(x)))
第2個(gè)謂詞公式: (@x)(P(x)&S(x))
邏輯結(jié)論為：(#x)(S(x)&R(x))
合并后的謂詞公式：
(@x)(P(x)>(Q(x)&R(x)))&(@x)(P(x)&S(x))&~(#x)(S(x)&R(x))
消去蘊(yùn)含：
(@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))
變元標(biāo)準(zhǔn)化：
(@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 標(biāo)準(zhǔn)型：
(~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)
歸結(jié):
歸結(jié)策略1：
(6) ~R(r) [ (4),(5) { r/l } ]
(7) ~P(r) [ (2),(6) { r/x } ]
(8) Nil [ (3),(7) { r/l } ]
成功
歸結(jié)策略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 } ]
成功
實(shí)驗(yàn)分析：歸結(jié)采用水平歸結(jié)，從尾部開始進(jìn)行，即從結(jié)論出發(fā)開始遍歷尋找相應(yīng)結(jié)論的逆命題直至close表歸結(jié)為Nill（空），此時(shí)結(jié)論證明成功。采用的是支持集策略。
六、實(shí)驗(yàn)總結(jié)
利用歸結(jié)反演方法來證明定理的具體步驟為：
步1否定目標(biāo)公式G，得到?G；
步2將?G并入到公式集F1＾F2＾．．．＾Fn中；
步3將公式集化子句集，得到子句集S；
步4對S進(jìn)行歸結(jié)，每次歸結(jié)的結(jié)果并入到S中。如此反復(fù)，直到得到空子句為止。此時(shí)，就證明了在前提F1＾F2＾．．．＾Fn為真時(shí)，結(jié)論G為真。
支持集策略
（1）每次歸結(jié)時(shí)，兩個(gè)親本子句中至少要有一個(gè)是目標(biāo)公式否定的子句或其后裔。
（2）目標(biāo)公式否定的子句及其后裔即為支持集。
特點(diǎn)
（1）盡量避免在可滿足的子句集中做歸結(jié)，因?yàn)閺闹袑?dǎo)不出空子句。而求證公式的前提通常是一致的，所以支持集策略要求歸結(jié)時(shí)從目標(biāo)公式否定的子句出發(fā)進(jìn)行歸結(jié)。支持集策略實(shí)際是一種目標(biāo)制導(dǎo)的反向推理。
（2）支持集策略是完備的。
實(shí)驗(yàn)指導(dǎo)書
參考文獻(xiàn):
人工智能歸結(jié)原理實(shí)驗(yàn)
基于謂詞邏輯的歸結(jié)原理研究文章來源：http://www.zghlxwxcb.cn/news/detail-401171.html
代碼
文章來源地址http://www.zghlxwxcb.cn/news/detail-401171.html
到了這里，關(guān)于人工智能 歸結(jié)原理實(shí)驗(yàn)報(bào)告的文章就介紹完了。如果您還想了解更多內(nèi)容，請?jiān)谟疑辖撬阉鱐OY模板網(wǎng)以前的文章或繼續(xù)瀏覽下面的相關(guān)文章，希望大家以后多多支持TOY模板網(wǎng)！
