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

痛定思痛。 2023-07-24 14:42 30阅读 0赞

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

### 文章目录 ###

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

# 归结演绎推理 #

推理方式：  
![20200412180420332.png][]

**归结演绎推理** 定理：  
![20200412181314899.png][]

## 谓词公式化为子句集 ##

**常出现的名词：**

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

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

**\[例\]**  
![20200413002104753.png][]

*  第一步：**消去谓词公式中的“ → \\rightarrow →” 和 “ ⇔ \\Leftrightarrow ⇔” 符号**
    
     *  公式：![20200413001154705.png][]
     *  **\[例\]** ![20200413001901447.png][]
 *  第二步：**把否定符号 “~” 移到紧靠谓词的位置上**
    
     *  公式：![20200413135839670.png][]
     *  **\[例\]** ![20200413140105340.png][]
 *  第三步：**变量标准化**
    
     *  公式：![20200413141209387.png][]
     *  **\[例\]** ![20200413141322527.png][]
 *  第四步：**消去存在量词**
    
     *  若存在量词不出现在全称量词的辖域内（很简单，用一个个体表示即可）
     *  若存在量词出现在一个或多个全称量词的辖域内（存在量词 y 的Skolem函数为 y = f(x1, x2, …, xn)，需要用Skolem函数代替每个存在量词量化的变量的过程)
     *  Skolem函数表示约束，但不关系约束是什么
     *  **\[例\]** ![20200413142202138.png][]
 *  第五步：**化为前束形**
    
     *  前束形 = （前缀）\{母式\}
     *  前缀：全称量词
     *  母式：不含量词的谓词公式
     *  **\[例\]** 已经是前束形
 *  第六步：**化为Skolem标准化**
    
     *  子句的合取式，称为Skolem标准形的母式
     *  公式：![20200413142828931.png][]
     *  **\[例\]** ![20200413142950634.png][]
 *  第七步：**略去全称量词**
    
     *  **\[例\]** ![20200413143135643.png][]
 *  第八步：**消去合取词**
    
     *  **\[例\]** ![20200413143329715.png][]
 *  第九步：**子句变量标准化**
    
     *  即不同的子句用不同的变元
     *  **\[例\]** ![20200413143513872.png][]

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

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

基本思想：

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

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

![20200413145054985.png][]

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

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

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

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

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

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

## 归结反演 ##

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

**已知命题公式集 s，求证 r**  
![20200413151056305.png][]

第一步，将每个命题化为子句形式：  
![20200413152127358.png][]

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

第三步，归结：  
![20200413152437181.png][]

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

# 题目及代码 #

设给定的已知条件为公式集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()

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

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

--------------------