### 实验8 子句集消解实验
#### 实验目的
本次实验旨在掌握子句集消解的基本方法，具体包括以下两点：
1. **熟悉子句集化简的九个步骤**：通过一系列规范化的步骤，将任意复杂的谓词公式简化为子句集形式，便于进一步的逻辑推理和计算。
2. **理解消解规则，能把任意谓词公式转换成子句集**：学习并运用消解规则，将复杂谓词公式转换为子句集，这是实现自动定理证明的重要基础。
#### 实验环境
- **操作系统**：Windows 10
- **开发工具**：Visual C++ 6.0
#### 实验内容与步骤
##### 1. 消除连接词 “→” 和 “↔”
任何包含蕴含（“→”）或等价（“↔”）连接词的谓词公式可以通过等价变换转换为不包含这两种连接词的形式。具体操作如下：
- **消除蕴含**：\(P → Q\) 变换为 \(\neg P \lor Q\)
- **消除等价**：\(P ↔ Q\) 变换为 \((P \land Q) \lor (\neg P \land \neg Q)\)
##### 2. 减少否定符号的辖域
此步骤涉及将每个否定符号“\(\neg\)”尽可能移至谓词前面，即通过以下规则进行转换：
- **双重否定**：\(\neg(\neg P) \Leftrightarrow P\)
- **德·摩根律**：\(\neg(P \land Q) \Leftrightarrow \neg P \lor \neg Q\)；\(\neg(P \lor Q) \Leftrightarrow \neg P \land \neg Q\)
- **量词转换**：\(\neg(\forall x)P(x) \Leftrightarrow (\exists x)\neg P(x)\)；\(\neg(\exists x)P(x) \Leftrightarrow (\forall x)\neg P(x)\)
##### 3. 对变元标准化
为了防止量词辖域内的变量名称冲突，需要将每个量词辖域内的变量重命名为一个新的未使用过的变量名。例如，对于公式 \((\forall x)P(x) \land (\exists y)Q(x, y)\)，可以将其标准化为 \((\forall x')P(x') \land (\exists y')Q(x', y')\)。
##### 4. 化为前束范式
将所有量词移到公式的最左侧，并保持它们之间的相对顺序不变，从而得到前束范式。
##### 5. 消去存在量词
对于存在量词 \((\exists x)P(x)\)，可以引入一个与 x 无关的新常量 c（称为 Skolem 常量），并用 c 替换所有 x 的实例，即得到 \(P(c)\)。
##### 6. 化为 Skolem 标准形
在前束范式的基础上，通过引入 Skolem 函数来消除所有存在量词。
##### 7. 消去全称量词
将全称量词 \((\forall x)P(x)\) 消去后，可以直接考虑 \(P(x)\)，其中 x 是自由变量。
##### 8. 消去合取词
将含有合取词（\(\land\)）的公式转换为子句集的形式。例如，\((P \land Q) \lor R\) 转换成 \((P \lor R) \land (Q \lor R)\) 后，再分别拆分成子句 \(P \lor R\) 和 \(Q \lor R\)。
##### 9. 更换变量名称
为了避免子句集中出现相同变量名称导致的混淆，对子句集中的某些变量重新命名，确保任意两个子句中没有相同的变量名。
#### 部分源程序代码
下面提供了一个简单的 C++ 示例代码，用于演示子句集化简的九个步骤之一——消去蕴含连接词 “→”。
```cpp
#include <iostream>
#include <string>
#include <stack>
using namespace std;
bool isAlbum(char c) {
return (c >= 'A' && c <= 'Z') || (c >= 'a' && c <= 'z');
}
string del_inlclue(string temp) {
string output = "";
int length = temp.length();
int i = 0, right_bracket = 0, falg = 0;
stack<char> stack1, stack2, stack3;
char ctemp[length + 1];
strcpy(ctemp, temp.c_str());
while (ctemp[i] != '\0' && i <= length - 1) {
stack1.push(ctemp[i]);
if (ctemp[i] == '>') { // 如果是 a > b，则用 ~a ! b 替代
falg = 1;
if (isAlbum(ctemp[i - 1])) { // 如果是字母，则把 ctemp[i - 1] 弹出
stack1.pop();
stack1.push('~');
stack1.push(ctemp[i - 1]);
stack1.push('!');
i++;
}
else if (ctemp[i - 1] == ')') {
right_bracket++;
do {
if (ctemp[i - 1] == '(')
right_bracket--;
stack3.push(stack1.top());
stack1.pop();
} while (right_bracket != 0);
stack3.push(stack1.top());
stack1.pop();
stack1.push('~');
while (!stack3.empty()) {
stack1.push(stack3.top());
stack3.pop();
}
stack1.push('!');
}
}
i++;
}
while (!stack1.empty()) {
output += stack1.top();
stack1.pop();
}
reverse(output.begin(), output.end());
return output;
}
int main() {
string ini;
initString(ini);
string result = del_inlclue(ini);
cout << "转换后的谓词公式: " << result << endl;
return 0;
}
```
以上代码展示了如何读入一个谓词公式，并通过 `del_inlclue` 函数来消除蕴含连接词 “→”，最后输出转换后的结果。通过这种方式，我们可以逐步完成整个子句集消解的过程。
