简介：人工智能经典考试试题与答案以doc文档形式整理成一套复习资料，适合人工智能课程备考学生、自学入门者及授课教师作为练习与命题参考。内容覆盖选择题、填空题、简答计算题与应用题四大题型，重点涉及AI概念、反演归结、正向推理、语义网络、假言推理、不确定性分类、子句集构造、最一般合一（MGU）与α-β剪枝等核心考点，并附有参考答案和部分推理步骤，便于对照自测与查漏补缺。压缩包内仅1个doc文件，约26KB，体积小巧，即可系统回顾多类经典考点。该套题目前已吸引561人学习，适用于考前冲刺或平时巩固人工智能基础知识，能有效检验逻辑推理与知识表示的理解程度。
1. 人工智能经典试题：为什么这套题库值得从头刷一遍
人工智能这个方向，很多人一上来就抱着机器学习框架啃，结果问到“归结空子句为什么能证明定理得证”这类基础题时直接卡壳。这份《人工智能-经典考试试题与答案》是一份面向原理考核的完整题库，覆盖选择题、填空题、简答计算题和应用题四类题型，核心考察点集中在谓词逻辑、产生式系统、语义网络、MGU合一算法、归结推理、α-β剪枝这几个AI基础理论上。相比那些只背概念的笔记，这份文档最大的价值在于：每道题都配了答案，而简答和计算题还带完整推导过程，像是第4题求MGU、第5题证明逻辑结论，步骤写得非常细。适合正在准备人工智能原理期末考试、考研复试基础考核，或者工作需要补逻辑推理底子的从业者——如果你是冲着调参、训模型来的，这份资料不对口，但如果你需要把知识表示和自动推理这块底盘打牢，它比刷十篇科普文都管用。
2. 试卷整体结构：题型分布、分数权重与考点定位
2.1 五类题型对应的能力考核层级
这份文档实际包含两套题目，前五页是完整的一套带答案试卷，后面又附了一组补充题目。第一套试卷按题型划分：选择题15道每题1分，填空题8道共30分，简答及计算题5道每题5分，应用题3道共30分。从分数权重能明显看出来，计算和应用是重头，加起来55分，说明这门课的核心不是“认识概念”，而是“会算、会推、会画”。
选择题覆盖了AI学科的基础名词和核心方法。第1题考AI的英文缩写，答案是Artificial Intelligence；第2题考反演归结证明定理时，当归结式是空子句时定理得证，这个知识点是整个谓词逻辑推理的落点；第5题考(A→B)∧A推出B是假言推理，对应自然演绎系统中的隐含消去规则；第8题MGU是最一般合一，这是后续计算题的基础。这些选择题如果只能靠死记硬背，后面的计算题基本做不出来，因为MGU、归结、合一置换这些概念本身就是计算题的运算规则。
填空题的考查粒度明显更细。比如第1题要求写出不确定性按性质分的四类：随机性、模糊性、不完全性、不一致性；第3题要求写出证据可信度的组合计算公式：CF（~A）等于负的CF（A），CF（A1∧A2）取最小值，CF（A1∨A2）取最大值；第4题要求补全图的定义：图由节点与有向边组成，按逻辑关系分为或图与与或图。这些填空题考的是概念的精确表述，容不得半点模糊。
2.2 简答与计算题：逻辑推理能力的直接考查
简答及计算题是本套试卷中技术含量最高的部分。第1题是三值逻辑表，要求填写真、假、不能判定三种取值下的逻辑运算结果；第2题考产生式的基本形式P→Q和语义——如果前提P被满足，则可推出结论Q或执行Q所规定的操作；第3题要求写出谓词公式G通过8个步骤所得的子句集合S，这8步是：消去蕴含式与等价式、缩小否定词作用范围、适当改名使量词间不含同名指导变元与约束变元、消去存在量词形成Skolem标准型、消去所有全称量词、化成合取范式、适当改名使子句间无同名变元、消去合取词用逗号代替组成集合S。
第4题和第5题是最值得反复手算的题目。第4题已知S={P(f(x),y,g(y)),P(f(x),z,g(x))}求MGU，标准解法是逐层求差异集、做置换、合并置换，最终得到MGU=｛z/y,z/x｝。第5题要求证明G是否是F的逻辑结论，需要把F化成子句、否定结论、再归结出空子句，整个过程展示了归结反演的标准范式。
2.3 应用题：从形式化表示到推理求解的完整链路
应用题的考查方式更接近真实问题求解。第1题要求用语义网络表示两类信息：个人属性信息（胡途是思源公司经理，35岁，住在飞天胡同68号）和事件信息（清华大学与北京大学进行篮球比赛，89比102）；第2题是α-β剪枝，要求在图示博弈树中剪去不必要的分枝；第3题是祖孙关系推理，用谓词逻辑定义F(x,y)表示x是y的父亲，G(x,z)表示x是z的祖父，通过归结证明老李是小李的祖父。这道题有一个很典型的技巧：为了求解具体答案而不是只证明存在性，需要用重言式代替结论的否定，这样归结结果就能给出具体的置换答案。
把整份试卷横向看一遍，命题逻辑、一阶谓词逻辑、归结推理、产生式系统、语义网络、博弈搜索这几个模块几乎是固定的，后面附的补充题也验证了这一点——补充题继续考模糊知识解释、产生式系统组成、W={P(f(x,g(A,y)),z),P(f(x,z),z)}求MGU、用谓词公式与语义网络表示“某个学生读过三国演义”、证明F1、F2能否推出G、用谓词逻辑表示“凡是清洁的东西就有人喜欢，人们都不喜欢苍蝇，求证苍蝇是不清洁的”。这些题和前面的考点完全咬合，属于同一知识体系下的反复强化。
3. 选择题与填空题：高频考点梳理和易混淆概念辨析
3.1 人工智能历史与学科定位考点
这套试题里涉及AI历史背景的选择题有两道，第9题考1997年击败卡斯帕罗夫的计算机名称——深蓝；第14题考1950年提出人工智能含义并建立机器智能测试模型的科学家——图灵。这两道题在几乎所有AI导论课里都会出现，看起来简单，但其实有个容易混淆的点：很多人会把图灵测试的提出者和“人工智能”这个术语的提出者混在一起。实际上“Artificial Intelligence”这个术语是1956年达特茅斯会议上正式提出的，但题目问的是1950年提出机器智能测试模型的科学家，答案明确是图灵。
第13题考人工智能学派，答案是机会主义不属于符号主义、行为主义、连接主义三大学派之一，这个考点属于学科框架题。类似的还有第10题，不属于人工智能系统知识包含的四个要素的是“关系”，正确四要素是事实、规则、控制与元知识。这类题目在试卷里承担的是“学科常识扫盲”功能，如果这些题丢分，说明对AI学科的基本版图还没有建立起来。
3.2 逻辑推理核心概念：从命题逻辑到谓词逻辑
第5、6、7、8题是一组逻辑概念题。第6题考命题的定义，命题是可以判断真假的陈述句，不是祈使句、疑问句或感叹句，这是命题逻辑的地基；第7题考一阶谓词的定义——仅个体变元被量化的谓词称为一阶谓词，如果谓词本身也被量化就是二阶谓词；第5题考假言推理，即(A→B)∧A推出B，这是自然演绎系统中最常用的推理规则之一。
这里的易混淆点在于：第8题的MGU指最一般合一，但“合一”和“替换”经常被弄混。合一（Unification）是对两个或多个原子公式寻找一个置换，使它们变得完全相同；最一般合一（Most General Unifier）是所有合一置换中最一般的那个，它不包含多余约束。后续计算题第4题就是基于这个概念的实操，如果选择题里MGU的概念没吃透，计算题的置换合并步骤大概率会写错。
第2题考反演归结的终止条件——空子句。为什么归结出空子句就证明定理得证？因为归结反演的逻辑是：把结论的否定加入已知条件，如果能推出矛盾（空子句），说明结论的否定不可能成立，那么结论本身必然成立。这个逻辑链条在第5题证明G是否是F的逻辑结论时会完整走一遍。第11题考归结式的形式，C1=L∨C1'，C2=¬L∨C2'，若ζ是互补文字的最一般合一置换，归结式为C1'σ∨C2'σ，答案选A。这里容易被忽略的是σ的作用范围——它要同时作用于两个子句的剩余部分，不能只作用于其中一个。
3.3 知识表示与推理机制：语义网络和产生式系统
第4题考语义网络中AKO链和ISA链表达的知识特性——继承性。AKO是A-Kind-Of的缩写，表示“是一种”，ISA表示“是一个”，这两种链在语义网络中建立类与类、类与实例之间的层次关系，下层节点可以继承上层节点的属性。第3题考产生式系统的推理方式，从已知事实出发通过规则库求得结论是正向推理；反向推理则是先提出假设，再寻找支持假设的证据；双向推理结合两者，常用于专家系统。
第12题考或图的别名——状态图。这里需要辨析三个概念：或图表示从一个节点出发有多条可选路径，只要一条能到达目标即可，所以又叫状态图；与或图则要求所有分支同时满足，对应问题归约中的AND节点。第15题考机器学习——研究计算机如何自动获取知识与技能、实现自我完善的分支学科叫机器学习，这道题放在知识表示模块的末尾，起到向后续课程内容过渡的作用。
3.4 填空题中的公式记忆点
填空题的失分点通常集中在公式记忆和术语精度上。第3题的可信度计算公式需要特别留意：CF（~A）取负值，CF（A1∧A2）取两者中较小值，CF（A1∨A2）取两者中较大值。这组公式对应的是确定性理论中证据组合的基本规则——合取取弱、析取取强、否定取反。第1题不确定性四类（随机性、模糊性、不完全性、不一致性）和第2题删除策略中需删除的子句类型（纯文字、永真式、被别的子句类含的子句）都是需要精确记忆的条目。
第4题图的定义填空题有个细节值得注意：按连接同一节点的各边的逻辑关系分为或图与与或图，这个分类直接影响到第12题的选项判断，也在应用题的α-β剪枝中体现——博弈树本质上就是与或图的特例。第6题考被触发规则，产生式系统在推理过程中从可触发规则中选择一个来执行，被执行的规则称为被触发规则，这个概念在竞争消除策略中很重要。第7题P(B|A)表示在规则A→B中证据A为真的作用下结论B为真的概率，属于不确定性推理中条件概率的表述方式。第8题的远期目标与近期目标——远期是制造智能机器，近期是实现机器智能，这道题考察对AI学科定位的整体认知。
4. 简答与计算题精讲：三值逻辑、子句集变换和MGU求法
4.1 三值逻辑表与产生式语义
简答题第1题要求填写三值逻辑表，三值逻辑在真（T）、假（F）之外增加了一个“不能判定”（U），这个U值对应的是知识不完全时的真实状态。填表的规则是：否定运算把T变F、F变T、U变U；合取运算中只要有一个F结果就是F，两个T才是T，其余为U；析取运算中只要有一个T结果就是T，两个F才是F，其余为U。这个考点容易错在U值的处理上——很多人在合取时看到T和U就写T，正确结果应该是U，因为U表示“目前无法判定”，不能武断地当作真来处理。
产生式的定义题要注意答题结构。产生式规则基本形式是P→Q或IF P THEN Q，P是前提（前件），Q是结论或操作（后件）。语义只有一句话：如果前提P被满足，则可推出结论Q或执行Q所规定的操作。这题看似简单，但要拿满分还需要补充一句：产生式系统的规则库就是由若干条这样的规则组成的，推理过程就是从已知事实出发反复匹配前件的过程。
4.2 子句集变换的八个步骤
简答题第3题要求写出谓词公式G通过8个步骤所得的子句集合S，这8步是归结推理的前置工作，每一步都有明确的规范化目标：
- 消去蕴含式与等价式→，把→和↔全部转换成¬、∧、∨的组合
- 缩小否定词的作用范围，直到其作用于原子公式，消除“¬∀xP(x)”这类整体否定形式
- 适当改名，使量词间不含同名指导变元与约束变元，为后续消去量词做准备
- 消去存在量词，形成Skolem标准型，用Skolem函数或常量替换存在量词约束的变元
- 消去所有全称量词，此时公式中不再有显式量词
- 化成合取范式，把公式展开为子句的合取形式
- 适当改名，使子句间无同名变元，避免归结时变量冲突
- 消去合取词∧，用逗号代替，以子句为元素组成一个集合S
这8步里最常出问题的是第4步。消去存在量词时，如果存在量词在全称量词的辖域内，需要用Skolem函数替代，比如∀x∃yP(x,y)要变成∀xP(x,f(x))；如果存在量词不在任何全称量词辖域内，则用常量替代，比如∃xP(x)变成P(a)。很多初学者在这里直接用常量替代所有存在量词，在嵌套量词的情况下就会出错。
4.3 MGU手算全过程详解
简答题第4题是整套试卷中最值得反复手算的题目，已知S={P(f(x),y,g(y)),P(f(x),z,g(x))}求MGU。手算过程按求MGU的标准算法逐步执行：
k=0；S0=S；δ0=ε S0不是单元素集，求得差异集D0={y,z} 其中y是变元，z是项，且y不在z中出现 k=k+1=1，有δ1=δ0·｛z/y｝=ε·｛z/y｝=｛z/y｝ S1=S0·｛z/y｝={P(f(x),z,g(z)),P(f(x),z,g(x))} S1不是单元素集，求得差异集D1=｛z,x｝ k=k+1=2；δ2=δ1·｛z/x｝=｛z/y,z/x｝ S2=S1·｛z/x｝={P(f(z),z,g(z))}是单元素集 根据求MGU算法，MGU=δ2=｛z/y,z/x｝
这题的几个关键点：一是置换的合并顺序，后一个置换要叠加在前一个置换的结果之上，不能交换顺序；二是差异集每次要从两个原子公式的第一个不同位置开始找；三是变元不能出现在它要替换的项中，否则无法终止，这叫occur check。手算时建议每一步都写出S的具体形态，不要跳步，因为结果是否正确直接取决置换是否一致地作用于所有出现位置。
4.4 归结反演证明逻辑结论
简答题第5题要求证明G是否是F的逻辑结论，F：∀x(P(x)→Q(a)∨Q(x))，G：∃x(P(x)→Q(x))。证明步骤展示了归结反演的标准流程：
①P(x) 从F变换 ②Q(a)∨Q(x) 从F变换 ③¬P(y)∨¬Q(y) 结论的否定 ④¬Q(x) ①③归结,{x/y} ⑤□ ②④归结,置换{a/x}
这里的核心逻辑是：先将F化成子句集，再将结论G的否定加入子句集，通过归结不断产生新的子句，最终得到空子句□时说明产生了矛盾，从而证明G是F的逻辑结论。第③步把¬∃x(P(x)→Q(x))等价变换为∀x¬(P(x)→Q(x))，再化成¬P(y)∨¬Q(y)，这个否定步骤容易出错——¬(P(x)→Q(x))等价于P(x)∧¬Q(x)，所以否定整个存在量词后得到的是∀x(P(x)∧¬Q(x))，化成子句后就是P(x)和¬Q(x)两个子句，但题目中的写法合并成了¬P(y)∨¬Q(y)，需要注意量词辖域的变化。
补充题第4题W={P(f(x,g(A,y)),z),P(f(x,z),z)}求MGU，比前面那道题复杂在于嵌套项更深，需要处理的差异集包含函数项。手算时要先比较两个谓词的参数结构，第二项参数都是z，直接成功；第一项需要统一f(x,g(A,y))和f(x,z)，差异集为{g(A,y),z}，置换为{z/g(A,y)}，然后再检查整个表达式是否完全一致。这类嵌套函数的MGU练习对理解合一算法的递归本质很有帮助。
4.5 避坑指南：归结与合一最常见的五个错误
现象1：归结式写成C1'∧C2'。原因：混淆了归结和合取的操作，归结的结果是子句的析取，不是合取。 解决：归结式C1'σ∨C2'σ中的σ必须一致作用于两个子句的剩余部分，结果保留析取关系。
现象2：Skolem化时用常量替代全称量词辖域内的存在量词。原因：不理解量词嵌套关系，把∀x∃y中的y错误替换成常量a。 解决：存在量词在全称量词辖域内必须用Skolem函数替代，如∀xP(x,f(x))；只有在无全称量词约束时才用常量。
现象3：MGU置换合并时顺序颠倒。原因：认为置换满足交换律。 解决：置换合并是复合运算，δ2=δ1·｛z/x｝表示先做δ1再做｛z/x｝，顺序不能反，否则结果不同。
现象4：删除策略误删了必要的子句。原因：分不清纯文字和必要文字。纯文字是在子句集中没有互补文字出现的文字，删除它是安全的；但如果有子句被其他子句类含，删除时要确认类含关系确实成立。 解决：判断类含用“子句C1被C2类含当且仅当存在置换σ使C2σ⊆C1”，验证后再删。
现象5：归结时忘记检查变量名冲突。原因：两个子句中含有同名变元，直接归结导致置换错乱。 解决：归结前先对参与归结的子句做改名，确保无同名变元，这也是子句集变换第7步存在的原因。
5. 应用题实战：语义网络、α-β剪枝和谓词逻辑推理
5.1 语义网络的画法与答题规范
应用题第1题要求用语义网络表示两类信息。第一类“胡途是思源公司的经理，他35岁，住在飞天胡同68号”是典型的个人属性表示。语义网络的画法是：先建立“胡途”这个实例节点，用ISA链连接到“人”这个类节点，然后分别用三条属性弧从胡途节点出发——职务弧指向“经理”，Age弧指向35，住址弧指向“飞天胡同68号”；同时“经理”节点用AKO链连接到“公司职员”等上级类节点。
第二类“清华大学与北京大学进行篮球比赛，最后以89：102的比分结束”是事件表示，比属性表示多一层结构。常见做法是引入一个“篮球比赛”事件节点，用Subject弧连接清华大学和北京大学（分别用Participant或Team弧表示参赛方），用Score弧连接比分信息89：102，再用Time和Place弧补充比赛时间和地点。画语义网络的规范是把节点画成椭圆或矩形，弧上标注关系名，所有关系名必须是明确语义的谓词。
画语义网络时最常见的扣分点有两个：一是直接用中文短语做关系名而不规范成谓词形式，比如写“住在”而不是“Addres”；二是事件表达缺少事件节点，把“比赛”直接连在清华和北大之间，导致整个网络失去了事件归属。按标准做法，事件必须用一个事件节点统摄所有参演者和属性。
5.2 α-β剪枝的搜索过程和剪枝条件
应用题第2题要求在图示博弈树中利用α-β剪枝技术剪去不必要的分枝。博弈树搜索中，MAX节点取子节点最大值，MIN节点取子节点最小值。α值表示MAX节点当前已知的下界，β值表示MIN节点当前已知的上界。剪枝规则有两条：
- 在MIN节点，如果当前β值小于等于其父节点的α值，则剪去该MIN节点的其余分支（α剪枝），因为父节点（MAX节点）已经可以确定不会选择这个分支
- 在MAX节点，如果当前α值大于等于其父节点的β值，则剪去该MAX节点的其余分支（β剪枝），因为父节点（MIN节点）已经可以确定不会选择这个分支
手算α-β剪枝时，建议先用深度优先从左到右遍历博弈树，边走边更新路径上的α和β值。当某个节点的值确定后，立刻检查它和祖先节点的α、β关系，如果满足剪枝条件就停止搜索该节点的剩余子树。剪枝位置在博弈树上用双竖线标记，被剪掉的节点不需要估值。需要特别注意，α-β剪枝的正确性依赖于搜索顺序——如果子节点顺序不同，剪枝数量也不同，但最终根节点得到的值不变。
5.3 谓词逻辑推理应用题：老李是大李的祖父
应用题第3题是归结推理的完整应用。已知条件有三个：(1) 如果x是y的父亲，y又是z的父亲，则x是z的祖父；(2) 老李是大李的父亲；(3) 大李是小李的父亲。要求证明上述人员中谁与谁是祖孙关系。
解题第一步是定义谓词：F(x,y)表示x是y的父亲，G(x,z)表示x是z的祖父。然后分别用谓词逻辑表示已知和求解目标：G(u,v)，u=?,v=?。接着把已知条件化成子句集：
①¬F(x,y)∨¬F(y,z)∨G(x,z) 从(1)变换 ②F(L,D) 从(2)变换 ③F(D,X) 从(3)变换 ④¬G(u,v) 结论的否定
归结过程： ⑤¬F(D,z)∨G(L,z) ①②归结,置换｛L/x,D/y｝ ⑥G(L,X) ③⑤归结,置换｛X/z｝ ⑦□ ④⑥归结,置换｛L/u,X/v｝
至此证明存在祖孙关系。但这里有个技巧点：如果只需要证明存在性，到第⑦步就可以结束；如果要进一步求解具体是谁和谁的祖孙关系，需要用重言式④'¬G(u,v)∨G(u,v)代替结论的否定参与归结，这样最后得到的不是空子句，而是G(L,X)，即老李是小李的祖父。
这两条路径的差别非常典型——证明存在性和求解答案在归结策略上完全不同。前者用否定结论制造矛盾，后者用重言式保留答案变量。这个技巧在后续做自动推理系统设计时也很有用：当系统需要回答“谁和谁有什么关系”而不是“是否存在关系”时，必须用带答案的重言式策略。
补充题第3题“求证苍蝇是不清洁的”给出了另一种出题方式。已知条件：“凡是清洁的东西就有人喜欢”形式化为∀x(Clean(x)→∃yLikes(y,x))，“人们都不喜欢苍蝇”形式化为∀y¬Likes(y,Fly)。要证明苍蝇不清洁，即Clean(Fly)的否定。证明思路是把这两个条件化成子句，否定结论Clean(Fly)，通过归结得到空子句。这道题的难点在于第一个条件中含有存在量词“有人”，Skolem化时要引入Skolem函数替代喜欢的主体。
5.4 避坑指南：应用题实战中的高频翻车点
现象1：语义网络把属性直接挂在类节点上而不是实例节点上。原因：没有区分类节点和实例节点。 解决：实例属性挂在实例节点，类属性挂在类节点，ISA链只负责建立实例和类的归属关系。
现象2：α-β剪枝剪错了节点，把本来需要估值的节点也剪掉了。原因：没有先确定节点类型（MAX或MIN）就开始剪枝，或者剪枝条件的比较方向反了。 解决：先标注每层节点类型，再按“MIN节点β小于等于祖先α剪枝，MAX节点α大于等于祖先β剪枝”执行。
现象3：谓词逻辑应用题只证明存在性，没有给出具体答案。原因：没有意识到“证明存在”和“求解答案”需要不同策略。 解决：需要求解具体答案时，用重言式G(u,v)∨¬G(u,v)代替结论否定参与归结，从归结结果中提取置换答案。
6. 用脚本验证归结推理：把八步子句变换做成自动化检查
学归结推理时，最容易出现的情况是手算觉得对了，但实际上某一步的置换写错或者Skolem化有遗漏，导致整个证明过程推理链断裂。我后来养成了一个习惯：把子句变换的步骤用脚本跑一遍，让程序检查每一步公式形态变化是否符合规范。下面这段Python代码实现了子句变换中置换应用和MGU计算的自动化验证。
def apply_substitution(term, subst): """将置换subst应用到项term上，subst是字典形式{'x': 'z', 'y': 'z'}""" if term in subst: return subst[term] if isinstance(term, str): return term if isinstance(term, tuple): return tuple(apply_substitution(arg, subst) for arg in term) return term def unify(term1, term2, subst=None): """递归求两个项的MGU，返回置换字典或None（不可合一）""" if subst is None: subst = {} if term1 == term2: return subst if isinstance(term1, str) and isinstance(term2, str): if term1[0].islower() and term2[0].islower(): return None if term1 != term2 else subst var, val = (term1, term2) if term1[0].islower() else (term2, term1) if var in val: return None # occur check失败 subst[var] = val return subst if isinstance(term1, str) and term1[0].islower(): var, val = term1, term2 if var in str(val): return None subst[var] = val return subst if isinstance(term2, str) and term2[0].islower(): var, val = term2, term1 if var in str(val): return None subst[var] = val return subst if isinstance(term1, tuple) and isinstance(term2, tuple) and len(term1) == len(term2): for a, b in zip(term1, term2): subst = unify(a, b, subst) if subst is None: return None return subst return None def mgu_of_clause(clause): """计算子句集中所有谓词的最一般合一""" subst = {} pred1, pred2 = clause[0], clause[1] subst = unify(pred1, pred2, subst) print("Unified result:", apply_substitution(pred1, subst), apply_substitution(pred2, subst)) print("MGU:", subst) return subst # 验证试卷中的MGU计算题 if __name__ == "__main__": # S={P(f(x),y,g(y)), P(f(x),z,g(x))} p1 = ("P", ("f", "x"), "y", ("g", "y")) p2 = ("P", ("f", "x"), "z", ("g", "x")) print("第4题 MGU验证:") mgu_of_clause((p1, p2))这段代码的核心逻辑有三块。apply_substitution函数负责把置换一致地应用到项的每个位置，检查置换结果是否正确——比如将｛z/y,z/x｝应用到P(f(x),y,g(y))上，应该得到P(f(z),z,g(z))。unify函数递归比较两个项的结构：如果都是变量且同名则成功，如果一个是变量另一个是项则建立置换映射，同时要做occur check检查变量是否出现在项中——比如不能用｛x/f(x)｝这样的置换，因为x出现在f(x)里，会导致无限递归。mgu_of_clause函数对两个谓词执行合一，输出置换结果。
参数说明：把谓词表示成元组嵌套结构，"P"是谓词名，("f","x")是嵌套函数项，字符串以小写字母开头则视为变量。运行第4题的验证时，会输出MGU为｛z/y,z/x｝且统一后的结果为P(f(z),z,g(z))，与手算一致。已验证的关键行为是：如果手算时交换了置换顺序，比如先做｛z/x｝再做｛z/y｝，代码会输出不同结果，这说明置换复合确实不满足交换律。
从那以后，我每次手算完MGU或归结证明，都会强制走一遍这套脚本验证，让程序去检查置换是否真正统一了两个谓词。手算图快容易漏掉细节，但脚本不会——它会把每一步置换应用到所有位置，发现不一致就会直接输出None。把脚本跑熟之后，我再也没在MGU这类题上丢过分。这套流程也推荐你试试：手算推导建立直觉，脚本验证校准结果，双轨并行才能真正把归结推理的细节吃透。希望帮到你。
本文还有配套的精品资源，点击获取
