合一算法的合一算法的Python实现实现–人工智能人工智能
考察 合一算法合一算法
求点赞，给作者一点分享的鼓励求点赞，给作者一点分享的鼓励
代码没写GUI，因为不喜欢这玩意，直接在终端中进行人机交互
代码写的较为冗余，主要还是我没动力了，不想优化了，因为调试代码已经把我榨干了
文章目录文章目录合一算法是什么？由来合一算法思路及代码
合一算法是什么？合一算法是什么？
由来由来
如何解决 谓词演算归结谓词演算归结 的一个问题，即决定那两个子句是否为亲本子句。例如，下面两个文字
是否能够成为亲本子句呢？
L(f(x)) ∨ L(A)
～L(B)
合一算法正是为此而来
合一算法合一算法
在谓词逻辑中，一个表达式的 项项 是 常量符号、变量符号或函数式常量符号、变量符号或函数式。
表达式的 例示例示(instance) 是指在表达式中用项来置换变量而得到特定的表达式，用来
置换的项称为置换项。
在归结过程中，寻找项之间合适的变量置换使表达式一致的过程，称为合一过程，简称合一(Unify)。
定义定义1：若存在一个代换s，使得二个文字L1与L2进行代换后，有 L1s = L2s，即 L1与～L2为互补文字，则L1与L2为可合一
的。这个代换代换s称为合一元称为合一元(unifier)。
代换的使用：
只能用项（常量，变量或函数符号）t 去代换变量 x在公式中的一切出现，代换记为s = t/x，对一个公式F的作s代换记为Fs。
显然，f(x)、A、B之间不存在代换。
任一被代换的变量不能出现在用作代换的表达式中。{g(x)/x}不是代换。
代换并非唯一。
看一个例子看一个例子，对于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}
再看一个例子，再看一个例子，
评论0