计算机数理逻辑-一阶逻辑-归结

1. atom vs literal vs term

a: $p$
- 在一阶逻辑下得到扩展
l: $p$ $\lnot{p}$
- 注意扩展到命题逻辑中时，$P$就可以带上函数和谓词
  - In propositional calculus a literal is simply a propositional variable or its negation.
  - In predicate calculus a literal is an atomic formula or its negation, where an atomic formula is a predicate symbol applied to some terms, ${\displaystyle P(t_{1},\ldots ,t_{n})}$ with the terms recursively defined starting from constant symbols, variable symbols, and function symbols. For example, ${\displaystyle \neg Q(f(g(x),y,2),x)}$ is a negative literal with the constant symbol 2, the variable symbols x, y, the function symbols f, g, and the predicate symbol Q.
t: $v$ $f^{n}$ $a$
- 注意term是变量而非字面量，如x+y，而不是p+q

Let s and t be two terms (or atoms), A unifier of s and t is a substitition σ that makes the two identical, formally
- sσ = tσ

σ is a most general unifier of s and t, denoted mgu(s, t),

Input: An equational system E
Goal: Determine if E is unifiable, and if it is, to read off mgu
Output: Equational system E’ in solved form, or ⊥ (for not unifiable)
Perform the following transformations on the set of equations as long as any one of them is applicable:
- 注意一定要用到不能用为止，一般结果会是左式由带有同一变量的右式表达，例如：
  - $x=y$
  - $z=f(y)$

Transform t=x, where t is not a variable, to x=t. 变量换到左侧，非变量换到右边
Erase the equation x=x. 消除相等式
Let t′=t″ be an equation where t′, t″ are not variables. “非变量=非变量”的情况
1. If the outermost function symbols of t′ and t″ are not identical, terminate the algorithm and report not unifiable. 如果t′和t″的最外层函数符号不一致，则终止算法，并报告不可合一
2. Otherwise, replace the equation $f(t_1^{‘},…t_k^{‘})=f(t_1^{‘’},…t_k^{‘’})$ by the k equations $t_1^{‘}=t_1^{‘’},…t_k^{‘}=t_k^{‘’}$ . 否则替换
Let x=t be an equation such that x has another occurrence in the set. 同一变量多次出现
1. If x occurs in t and x differs from t, terminate the algorithm and report not unifiable
2. Otherwise, transform the set by replacing all occurrences of x in other equations by t. 否则，通过将其他方程中所有出现的x替换为t来转换这个集合
3. rule 4 also called the occurs-check

example

example

The unifiability of ${ p(f(x)),g(y),p(f(f(a))),g(z) }$ is expressed by the set of term equations
- ${ f(x)=f(f(a)), g(y)=g(z) }$

A set of term equations is in solved form iff:
- All equations are of the form $x_i =t_i$ where x i is a variable.
- Each variable $x_i$ that appears on the left-hand side of an equation does not appear elsewhere in the set.
A set of equations in solved form defines a substitution:
- ${ x_1\leftarrow{t_1},…,x_n\leftarrow{t_n} }$

也就是说必须是用term来替代变量，而不是单纯的用其他变量来rename

A selection function is a mapping
- $S : C\rightarrowtail{}$ (multi-)set of occurrences of negative literals in C

example

A literal L is (strictly) maximal wrt. a general clause C
- iff ∃ gr. σ s.t. Lσ and $C_σ$ are ground and for all L’ in $C_σ$: $L_σ\geq{L’}$ ($L_σ>{L’}$)