1一阶逻辑对象、谓词与量词
闭卷重建一阶逻辑对象、谓词与量词的对象、公式、算例、算法与失败边界。
人工智能基础 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2量词次序与变量作用域
闭卷重建量词次序与变量作用域的对象、公式、算例、算法与失败边界。
3项替换与合一
闭卷重建项替换与合一的对象、公式、算例、算法与失败边界。
4一阶前向链
闭卷重建一阶前向链的对象、公式、算例、算法与失败边界。
5后向链与目标驱动
闭卷重建后向链与目标驱动的对象、公式、算例、算法与失败边界。
6一阶归结与Skolem化
闭卷重建一阶归结与Skolem化的对象、公式、算例、算法与失败边界。
7本体、开放世界与知识工程
闭卷重建本体、开放世界与知识工程的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：∀x∃y与∃y∀x通常不同；变量绑定和自由出现必须明确。；公式：∀x∃y Loves(x,y) ≠ ∃y∀x Loves(x,y)。；算例：每人爱某人可由各自爱自己满足，但未必存在人人都爱的一人。；边界：交换量词仍声称等价；替换导致变量捕获。。
对象：一阶逻辑以对象域、函数、谓词和量词表达关系结构。；公式：∀x Human(x)→Mortal(x)。；算例：域有甲乙，二者Human且Mortal时全称式真；若乙不Mortal则假。；边界：量词作用域错；把对象名当谓词。。
对象：对规则做满足前提的变量实例化，将新事实加入直到不动点。；公式：KB_{t+1}=KB_t∪Infer(KB_t)。；算例：Parent(A,B),Parent(B,C)和两跳规则推出Grandparent(A,C)。；边界：对象域无限仍盲目生成函数项；重复推导爆炸。。
对象：合一寻找使两个原子相同的最一般替换，并执行occurs check。；公式：mgu(P(x,a),P(b,y))={x/b,y/a}。；算例：P(x,a)与P(b,y)合一后均为P(b,a)。；边界：忽略occurs check得到x=f(x)无限项。。
对象：反证式一阶归结需标准化、Skolem化、CNF和合一；Skolem化保可满足性。；公式：∃y P(x,y)→P(x,f(x))（在全称x作用域下）。；算例：∀x∃y Loves(x,y)引入Skolem函数f(x)，得Loves(x,f(x))。；边界：把依赖x的存在量词换成常量；声称Skolem式逻辑等价。。
对象：后向链从查询选择能推出它的规则，把规则前提变成子目标。；公式：prove(q)→prove(p_1)…prove(p_k)。；算例：查询Mortal(Socrates)匹配Human(x)→Mortal(x)，子目标Human(Socrates)。；边界：递归规则无环检测；第一个失败规则后不试其他规则。。
对象：本体定义类、关系、约束和身份；开放世界下未能证明不等于假。；公式：unknown ≠ false。；算例：KB无Bird(Tweety)也无¬Bird(Tweety)，结论是未知而非假。；边界：数据库闭世界规则直接套入开放知识库；实体错误合并。。