用Python实现命题逻辑归结推理系统--人工智能

索儿呀

23778人浏览 · 2020-04-15 23:07:58

索儿呀 · 2020-04-15 23:07:58 发布

考察 命题逻辑归结推理
代码没写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. 谓词逻辑中的归结原理（含有变量的子句的归结）

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

本文只涉及命题逻辑归结推理，若要实现谓词逻辑归结推理，还需要实现合一算法

合一算法的Python实现–人工智能

归结反演

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

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

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

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

第三步，归结：

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

题目及代码

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

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

编写程序完成以下功能：

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

子句集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()