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

参考链接： 人工智能中的命题逻辑

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

 文章目录

 归结演绎推理谓词公式化为子句集鲁滨逊归结原理（消解原理）1. 命题逻辑中的归结原理（基子句的归结）2. 谓词逻辑中的归结原理（含有变量的子句的归结）

   归结反演

  题目及代码

归结演绎推理 

推理方式：  

归结演绎推理 定理：  

谓词公式化为子句集 

常出现的名词： 

原子谓词公式：一个不能再分解的命题文字：原子谓词公式及其否定 

  正文字：P负文字：~P正文字、负文字互补 子句：任何文字的析取式。（任何文字本身也是子句）空子句（NIL）：不包含任何文字的子句 

  空子句是永假的，不可满足的 子句集：由子句构成的集合 

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

[例]  

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

           →

          \rightarrow

       →” 和 “

           ⇔

          \Leftrightarrow

       ⇔” 符号 

  公式：[例]   第二步：把否定符号 “~” 移到紧靠谓词的位置上 

  公式：[例]   第三步：变量标准化 

  公式：[例]   第四步：消去存在量词 

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

  前束形 = （前缀）{母式}前缀：全称量词母式：不含量词的谓词公式[例] 已经是前束形  第六步：化为Skolem标准化 

  子句的合取式，称为Skolem标准形的母式公式：[例]   第七步：略去全称量词 

  [例]   第八步：消去合取词 

  [例]   第九步：子句变量标准化 

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

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

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

基本思想： 

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

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

C12 是 C1 和 C2 的 归结式C1、C2 是 C12 的 亲本子句 

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

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()

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

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

推荐文章 

用Python实现一个动物识别专家系统–人工智能合一算法的Python实现–人工智能