• 考察 命题逻辑归结推理
• 求，给作者一点的鼓励
• 代码没写GUI，因为不喜欢这玩意，直接在终端中进行人机交互。使用代码之前，请根据自身情况对字符编码、文件路径进行修改
• 代码没有使用什么算法进行优化，姑且这样吧

归结演绎推理

推理方式：

归结演绎推理 定理：

谓词公式化为子句集

常出现的名词：

• 原子谓词公式：一个不能再分解的命题
• 文字：原子谓词公式及其否定
  • 正文字：P
  • 负文字：~P
  • 正文字、负文字互补
• 子句：任何文字的析取式。（任何文字本身也是子句）
• 空子句（NIL）：不包含任何文字的子句
  • 空子句是永假的，不可满足的
• 子句集：由子句构成的集合

用一个例子来说明一下谓词公式化为子句集的过程

[例]

• 第一步：消去谓词公式中的“
  $rightarrow$

  →” 和 “
  $Leftrightarrow$

  ⇔” 符号

  • 公式：
  • [例]

• 第二步：把否定符号 “~” 移到紧靠谓词的位置上

  • 公式：
  • [例]

• 第三步：变量标准化

  • 公式：
  • [例]

• 第四步：消去存在量词

  • 若存在量词不出现在全称量词的辖域内（很简单，用一个个体表示即可）
  • 若存在量词出现在一个或多个全称量词的辖域内（存在量词 y 的Skolem函数为 y = f(x₁, x₂, …, x_n)，需要用Skolem函数代替每个存在量词量化的变量的过程)
  • Skolem函数表示约束，但不关系约束是什么
  • [例]

• 第五步：化为前束形

  • 前束形 = （前缀）{母式}
  • 前缀：全称量词
  • 母式：不含量词的谓词公式
  • [例] 已经是前束形

• 第六步：化为Skolem标准化

  • 子句的合取式，称为Skolem标准形的母式
  • 公式：
  • [例]

• 第七步：略去全称量词

  • [例]

• 第八步：消去合取词

  • [例]

• 第九步：子句变量标准化

  • 即不同的子句用不同的变元
  • [例]

鲁滨逊归结原理（消解原理）

子句集中子句之间是合取关系，只要有一个子句不可满足，则子句集就不可满足

基本思想：

• 检查子句集S中是否包含空子句
• 若包含，则S不可满足
• 若不包含，在S中选择合适的子句进行归结
• 若归结出空子句，就说明S是不可满足的

1. 命题逻辑中的归结原理（基子句的归结）

• C₁₂ 是 C₁ 和 C₂ 的 归结式
• C₁、C₂ 是 C₁₂ 的 亲本子句

归结式：从亲本子句中去掉一对互补文字后，剩余的两个部分的析取范式

2. 谓词逻辑中的归结原理（含有变量的子句的归结）

证明过程较为复杂，简单来说：函数名相同，虽然变量名不同，可直接看作互补文字

归结反演

1. 将已知前提表示为谓词公式F
2. 将待证明的结论表示为谓词公式Q，并否定得到~Q
3. 把谓词公式集{F, ~Q} 化为子句集
4. 应用归结原理对子句集S中的子句进行归结，并把每次归结得到的归结式都并入到S中，如此反复，若出现了空子句，则停止归结，此时证明了Q为真

已知命题公式集 s，求证 r

第一步，将每个命题化为子句形式：

第二步，用文本文件保存的形式为：
p
～p ∨ ～q ∨ r
～u ∨ q
～t ∨ q
t
~ r

第三步，归结：

这就是一阶命题逻辑语言中一个简单的归结证明

题目及代码

设给定的已知条件为公式集F，要从F求证的命题为G，进行命题演算的归结步骤为：

1. 将公式集F中的所有命题改写成子句。
2. 将命题～G改写成一个子句或多个子句。
3. 将 1、2 所得到的子句合并成子句集S，放到一个文本文件中。（以上为手工完成）

编写程序完成以下功能：

1. 读入以上文本文件
2. 以适当的形式保存为子句集。
3. 在出现一个矛盾或无任何进展（得不到新子句）之前执行：
   • 从子句集中选一对亲本子句（两个子句分别包含某个文字的正文字，另外一个包含负文字）
   • 将亲本子句对归结成一个归结式；
   • 若归结式为非空子句，将其加入子句集；若归结式为空子句，则归结结束。

子句集S存入文本文件

p ～p ∨ ～q ∨ r   ～u ∨ q    ～t ∨ q t ～r 

S = [] # 以列表形式存储子句集S """ 读取子句集文件中子句，并存放在S列表中     - 每个子句也是以列表形式存储     - 以析取式分割     - 例如：～p ∨ ～q ∨ r 存储形式为 ['～p', '～q', 'r'] """ def readClauseSet(filePath): global S     for line in open(filePath, mode = 'r', encoding = 'utf-8'):         line = line.replace(' ', '').strip()         line = line.split('∨')         S.append(line) """ - 为正文字，则返回其负文字 - 为负文字，则返回其正文字 """ def opposite(clause): if '～' in clause: return clause.replace('～', '') else: return '～' + clause   """ 归结 """ def resolution(): global S     end = False while True: if end: break         father = S.pop() for i in father[:]: if end: break for mother in S[:]: if end: break                 j = list(filter(lambda x: x == opposite(i), mother)) if j == []: continue else: print('n亲本子句：' + ' ∨ '.join(father) + ' 和 ' + ' ∨ '.join(mother))                     father.remove(i)                     mother.remove(j[0]) if(father == [] and mother == []): print('归结式：NIL')                         end = True elif father == []: print('归结式：' + ' ∨ '.join(mother)) elif mother == []: print('归结式：' + ' ∨ '.join(mother)) else: print('归结式：' + ' ∨ '.join(father) + ' ∨ ' + ' ∨ '.join(mother)) def ui(): print('----') print('--------命题逻辑归结推理系统--------') print('----') def main():     filePath = r'命题逻辑归结推理系统/S.txt'     readClauseSet(filePath)     ui()     resolution() if __name__ == '__main__':     main() 

很遗憾，我写的代码暂时只能实现命题逻辑归结推理系统，

对于谓词逻辑归结推理，以后有时间再完善代码

推荐文章

• 用Python实现一个动物识别专家系统–人工智能