• 考察 合一算法
• 代码没写GUI，因为不喜欢这玩意，直接在终端中进行人机交互
• 代码写的较为冗余，主要还是我没动力了，不想优化了，因为调试代码已经把我榨干了

合一算法是什么？

由来

如何解决 谓词演算归结 的一个问题，即决定那两个子句是否为亲本子句。例如，下面两个文字
是否能够成为亲本子句呢？

L(f(x)) ∨ L(A)

～L(B)

合一算法正是为此而来

合一算法

在谓词逻辑中，一个表达式的 项 是 常量符号、变量符号或函数式。

• 表达式的 例示(instance) 是指在表达式中用项来置换变量而得到特定的表达式，用来
  置换的项称为置换项。
• 在归结过程中，寻找项之间合适的变量置换使表达式一致的过程，称为合一过程，简称合一(Unify)。

定义1：若存在一个代换s，使得二个文字L₁与L₂进行代换后，有 L₁s = L₂s，即 L₁与～L₂为互补文字，则L₁与L₂为可合一的。这个代换s称为合一元(unifier)。

代换的使用：

1. 只能用项（常量，变量或函数符号）t 去代换变量 x在公式中的一切出现，代换记为s = t/x，对一个公式F的作s代换记为Fs。显然，f(x)、A、B之间不存在代换。
2. 任一被代换的变量不能出现在用作代换的表达式中。{g(x)/x}不是代换。
3. 代换并非唯一。

看一个例子，对于F= P(x, f(y), B)，存在四种代换：

s1 = {z/x, w/y}，则Fs1 = P(z, f(w), B)   (较一般的代换)

s2 = {A/y}，则Fs2 = P(x, f(A), B)

s3 = {g(z)/x, A/y}，则Fs3 = P(g(z), f(A), B)

s4 = {C/x, A/y}，则Fs4 = P(C, f(A), B)   (限制最严的代换）

s4称为基例示，因为作替换后不再含有变量。

定义2：表达式集合 {E1, … , Er} 的合一元σ称为是最一般合一元(most general unifier 简写为 mgu)，当且仅当对集合的每一个合一θ都存在代换λ使得θ=σ·λ，即任何代换都可以由σ再次代换而来。

看一个例子，表达式集合{P(x), P(f(y))}是可合一的，其最一般合一元为{f(y)/x}。因为对此集合的合一元θ = {f(a)/x, a/y}，有代换 λ = {a/y}，使θ = σ·λ = {f(y)/x}·{a/y}

再看一个例子，

思路及代码

代码实现之前的准备

1. 为实现方便，可规定将每个文字和函数符表达成一个表，表中第一元素为谓词名，其余元素为变元。
   • P(x, y) 表示成 (P x y )，f(x) 表示成 (f x )。
   • 若变元为函数，则该变元为一个子表，子表中第一元素为函数名。如：P(f(x), y) 表示成 (P ( f x ) y )，这样谓词和函数都统一表示成表。
2. 判断两个文字能否合一，则要判断它们所对应的表的各个项是否能够匹配，判断两个表项匹配的规则为：
   • 变量可与常量、函数或变量匹配；
   • 常量与常量，函数与函数，谓词与谓词相等才可以匹配。不同的常量，函数，谓词之间不能匹配；
3. 判断两个文字能否合一，还必须判断表示文字的表的长度必须相等，并且谓词是否相同。
   例如：P( x , y ) 化成表形式为 (P x y )，其长度为3；
   Q( x , y , g(z) ) 化成表形式为 (Q x y (g z))，其长度为4。

合一算法Unify(L1, L2)

1. 若L₁或L₂为一原子，则执行
   • 若L₁和L₂恒等，则返回NIL
   • 若L₁为一变量，则执行：
     • 若L₁出现在L₂中，则返回F；否则返回（L₂/ L₁）
   • 若L₂为一变量，则执行：
     • 若L₂中出现在L₁中，则返回F；否则返回（L₁/ L₂）
   • 否则返回F
2. 若length（L₁）不等于length（L₂），则返回F。
3. 置SUBST（替代）为NIL，在结束本过程时，SUBST将包含用来合一L₁和L₂的所有代换。
4. 对于i：=1 到L₁的元素数|L₁|，执行
   • 对合一L₁的第 i 个元素和L₂的第 i 个元素调用UNIFY，并将结果放在S中。
   • 若S = F，则返回F 。
   • 若S不等于NIL，则执行：把S应用到L₁和L₂的剩余部分；SUBST：=APPEND(S, SUBST)。返回SUBST。

合一过程Unify(L₁, L₂)

• 输入：
  L₁, L₂ 为表示成为表的两个谓词
  例如：P(x, y) 输入为 (P x y )，
  f(x) 输入为 (f x )；
  P(f(x), y) 输入为 (P ( f x ) y )

• 输出：
  如果找到代换，一张代换表作为其返回的值；
  如果返回空表NIL，表示可以匹配，但无需任何代换；
  如果返回由F值组成的表，则说明合一过程失败。

代码：

import re

"""
处理从键盘中读取的文字，返回列表
- 中文字符切换为英文
- 括号转化为列表
- 空格转为逗号
- 函数名一律转为大写字母
"""
def handleWord(word):
    # 中文字符切换为英文; 空格转为逗号
    word = word.replace('（', '[').replace('）', ']').replace('(', '[').replace(')', ']').replace(' ', ',').strip()
    
    # 对谓词进行操作
    if len(word) > 3: 
        # 函数名一律转为大写字母
        def func(x):
            return '[' + x.string[x.start()+1].upper() 
        word = re.sub(r'\[(\w)', lambda x:func(x), word)

    # 将word中字母字符转化为ASCII码，为了使用eval直接将其转化为元组
    def func2(x):
        return str(ord(x.string[x.start()])) 
    word = re.sub(r'[a-zA-Z]', lambda x:func2(x), word)

    # 将其转化为列表，内部数据为int类型
    word = list(eval(str(word)))
    # print('---handleWord()---')
    # print(word)
    # print(type(word))
    # print('---handleWord()---')
    print()

    return word

"""
判断是变量、常量还是函数
- 是变量，返回1
- 是常量，返回2
- 是函数，返回3
"""
def judge(x):
    if isinstance(x, list):
        return 3
    elif x >= 97 and x <= 122:
        return 1
    elif x >= 65 and x <= 90:
        return 2


"""
合一算法
"""
def unifyAtom(atom1, atom2):
    if judge(atom1) == 3 and judge(atom2) == 3:
        return unifyAllPre(atom1, atom2)
    if atom1 == atom2:
        return 'NIL'
    if judge(atom1) == 1:
        if str(atom1) in str(atom2):
            # print('--2--')
            return False
        else:
            return str(atom2) + '/' + str(atom1) + '/' + 'one' 
    elif judge(atom2) == 1:
        if str(atom2) in str(atom1):
            # print('--3--')
            return False
        else:
            return str(atom1) + '/' + str(atom2) + '/' + 'two'
    else:
        # print('--4--')
        return False

# testNumber = 0
results = []

"""
合一算法(对谓词公式中的参数逐一判断)
"""
def unify(L1, L2):
    global results
    for index in range(len(L1)):
        # global testNumber
        # testNumber += 1
        # print(testNumber)
        if(L1 == L2):
            return results
        atom1 = L1[index]
        atom2 = L2[index]
        S = unifyAtom(atom1, atom2)
        if not S or isinstance(S, list):
            # print('--5--')
            return S
        elif S != 'NIL':
            t = S.split('/')
            result = chr(int(t[0])) + '/' + chr(int(t[1]))
            if t[2] == 'one':
                t1 = str(L1).replace(t[1], t[0])
                L1 = list(eval(t1))
            if t[2] == 'two':
                t2 = str(L2).replace(t[1], t[0])
                L2 = list(eval(t2))
        results.append(result)
        # print(result)
        # print(L1,L2)
    return results

"""
合一算法（两个文字都是谓词公式时）
"""
def unifyAllPre(L1, L2):
    if len(L1) != len(L2) or L1[0] != L2[0]:
        # print('--1--')
        return False
    if L1 == L2:
        return 'NIL'
    del L1[0]
    del L2[0]
    return unify(L1, L2)


def ui():
    print('----')
    print('--------合一算法--------')
    print('约定：')
    print('1.变量输入时为小写字母')
    print('2.常量输入时为大写字母')
    print('3.函数名输入时大写或小写字母，并且程序运行函数名不区分大小写，比如函数名f与函数名F等价')
    print('----')
    print('输入方式：')
    print('比如：P(x, y, g(z)) 输入形式为：(P x y (g z))')
    print('字符之间用一个空格分隔')
    print('----')
    print('输出结果：')
    print('有代换，即输出代换s')
    print('完全相等，输出NIL')
    print('合一失败，输出False')
    print('----')
    word1 = input("输入第一个文字：")
    word2 = input("输入第二个文字：")
    word1 = handleWord(word1)
    word2 = handleWord(word2)
    print(unifyAllPre(word1, word2))


def main():
    ui()


if __name__ == '__main__':
    main()

• 代码注释处，之所以保留，是为了运行出问题时快速定位错误

人机交互示例：

----
--------合一算法--------
约定：
1.变量输入时为小写字母
2.常量输入时为大写字母
3.函数名输入时大写或小写字母，并且程序运行函数名不区分大小写，比如函数名f与函数名F等价
----
输入方式：
比如：P(x, y, g(z)) 输入形式为：(P x y (g z))
字符之间用一个空格分隔
----
输出结果：
有代换，即输出代换s
完全相等，输出NIL
合一失败，输出False
----
输入第一个文字：(P x y W (q r (T y)))
输入第二个文字：(P E D t (Q A (t D)))


['E/x', 'D/y', 'W/t', 'A/r']

---

推荐文章

• 用Python实现一个动物识别专家系统–人工智能
• 用Python实现命题逻辑归结推理系统–人工智能

命题逻辑归结推理 + 合一算法 = 谓词逻辑归结推理 就这样了吧