【人工智能】鲁滨逊归结原理-Python实现

news2024/11/19 17:30:56

一、实验目的

了解鲁滨逊归结算法原理，利用Python编写程序，实现鲁滨逊归结算法。

二、实验原理

鲁滨逊归结原理又称为消解原理，是鲁滨逊提出的一种证明子句集不可满足性，从而实现定理证明的一种理论及方法。它是机器定理证明的基础。

由谓词公式转化为子句集的过程可以看出，在子句集中子句之间是合取关系，其中只要有一个子句不可满足，则子句集就不可满足。由于空子句是不可满足的，所以,若一个子句集中包含空子句，则这个子句集一定是不可满足的。鲁宾逊归结原理就是基于这个思想提出来的。其基本方法是：检查子句集S中是否包含空子句,若包含，则S不可满足；若不包含，就在子句集中选择合适的子句进行归结，一旦通过归结得到空子句，就说明子句集S是不可满足的。

三、实验过程记录

以下为归结原理中归结过程的树形表示：

以下列题目为例，对归结原理进行应用。

下面我们用Python实现命题逻辑归结原理的演绎推理：

S = [] # 以列表形式存储子句集S

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

    filePath = r'./S.txt'

    readClauseSet(filePath)

    print('--------命题逻辑归结推理--------')

    resolution()



if __name__ == '__main__':

    main()