注v不能在φ中出现.
φ ⇒ ψ → ¬ φ ∨ ψ
φ ⇐ ψ → φ ∨ ¬ψ
φ ⇔ ψ → (¬ φ ∨ ψ ) ∧ (φ ∨ ¬ ψ)
第二步 N negations in
¬¬φ → φ
¬(φ ∧ ψ) → ¬φ ∨ ¬ψ
¬(φ ∨ ψ) → ¬φ ∧ ¬ψ
¬∀ν .φ → ∃ν.¬ φ
¬∃ν .φ → ∀ν.¬ φ
第三步 S Standardize variables
对变量进行重命名，让每一个量词都只为一限定一个变量
例∀x.(p( x) ⇒ ∃ x.q(x)) → ∀x.(p( x) ⇒ ∃ y.q(y))
第四步 E Existentials out
分两种情况
情况1，存在量词不在任何一个全称量词的限定中
则：去除所有的存在量词，用一个新的常量来替代这个变量
例∃x.p( x) → p(a)
情况2，存在量词在一个或多个全称量词的限定中
则，因为存在量词限定的变量的值可能会受到相关全称量词的值的影响，我们用一个新的函数（以全称量词所限定的变量作为值）来替代存在量词所限定的变量。
例：∀x.(p( x) ∧ ∃ z.q(x, y, z)) → ∀x.(p( x) ∧ q(x, y, f(x, y)))
φ ∨ ( ψ ∧ χ ) → (φ ∨ ψ) ∧ ( φ ∨ χ )
(φ ∧ ψ) ∨ χ → (φ ∨ χ) ∧ ( ψ ∨ χ )
φ ∨ ( φ1 ∨ ... ∨ φn) → φ ∨ φ1 ∨ ... ∨ φn
(φ1 ∨ ... ∨ φn ) ∨ φ → φ 1 ∨ ... ∨ φn ∨ φ
φ ∧ ( φ1 ∧ ... ∧ φn) → φ ∧ φ1 ∧ ... ∧ φn
(φ1 ∧ ... ∧ φn ) ∧ φ → φ 1 ∧ ... ∧ φn ∧ φ
第七步 O Operators out
去除与、或运算符，转变成子句形式
φ1 ∧ ... ∧ φn → φ1
→ ...
→ φn
φ1 ∨ ... ∨ φn → {φ 1, ... , φn}
在命题逻辑中任何语句的子句形式都和原语句是逻辑上等价的，但在海勃朗逻辑中并不一定是如此。
5合一 Unification
合一是判断两个表达是否能够通过适当的变量替换而统一起来的一个过程。
一个替换substitution是一个术语到变量的有限映射。
例如：{x←a, y ←f(b), z← v}
被替换的变量构成了替换的领域domain
替换这些变量的术语则构成了替换的范围range
上例中的domain是{x,y,z}range是{a, b, v}
当且仅当range内的所有替换术语都对于领域中的变量是自由的时，称一个替换是pure的。
{x←a, y←f(b), z←x}便是一个impure的替换
如果一个替换是pure的，则同样规则替换多次的结果是一致的，如果是impure的，则可能会不一致。
给定两河或更多次替换，可能可以定义一个一次替换达到前面两次或多次替换的效果。
一个合一子unifier如果具有具有最大的广泛性，则称为mgu。对于同样的两个表达，可能有多于一个的最广合一子。
计算最广合一子的步骤：
可能性1如果两个表达是形似的，则不作任何事
可能性2如果两个表达不形似，并且都是由常量构成，则失败，无法替换
可能性3如果两个表达不形似，且其中一个表达是一个变量，
然 则：检查变量是否有一个限定，如果有，则尝试在第二个表达式中对这个限定进行统一。
否则：检查第二个表达式是否含有该变量，
如果是：则失败
如果不：则尝试对第二个表达式中的变量进行限定
可能性4剩下的情况是两个表达都是一系列的句，则对其中每一项都进行上述转变。
例：p(x,x)和p(a,y).
6归结规则
与命题逻辑中类似
factor的概念：
如果一个子句Φ中的literal的一个子集具有一个最广合一子γ，那么通过运用γ对Φ进行替换的结果 Φ'就成为是一个factor.
7归结推理Resolution Reasoning
同命题逻辑类似。
称一个resolution derivation是对一系列的子句形式前提通过有限步骤的子句终结最终得出结论的过程，其中每一个子句都要么是前提要么是通过对先前存在的子句运用归结规则所得到的子句。
8不可满足性 Unsatisfiable
如果一系列子句形式的前提通过有限步骤的归结推理最终得到空集，则表示前提的一系列子句是不可满足的。
9逻辑蕴含
利用不可满足性知道，如果想知道一系列的前提Δ是否蕴含φ的问题，可以转变为判断Δ∪{¬ φ}是否是不可满足的的问题。在海勃朗逻辑中就变成将Δ∪{¬ φ}转变成子句形式，然后判断是否能归结推理出空集的问题。
以2中人人爱爱人人的例子为例：
前提为
∀x.∃ y.loves(x, y)
∀u.∀ v.∀w .(loves(v,w) ⇒ loves(u, v))
目标结论为
{loves(x,f(x))}
{¬loves(v,w), loves(u,v)}
{¬loves(a,b)}
是否能归结推理出空集的问题
种种原因本周未能听完，待日后再补了。
作业7.5和7.6的提示：
7.5已知前提AX:(P(X)=>q(X))和EX:P(X)目标结论为EX:q(X)，只需提出假设p(X)，然后运用新规则去前提的量词限定然后运用老规则得出q(X)，再运用新规则加上存在量词限定即可，注意假设后的子证明中的结论不能直接进行UI规则，需要先用II退出子证明。
7.6最后需要用EE，因而可以直接假设前提2中去除EY后的所有内容，主要是在子证明中需要通过AE来拆分语句，核心在于证明f(X,Z)。
.png)
.png)
