笔记 逻辑学导论 Week5

课程地址 https://class.coursera.org/intrologic-003/class/index

1海勃朗逻辑证明

当且仅当满足一些列前提的真值指派都能够同样满足结论时,我们说这一系列的前提能够在逻辑上蕴含这个结论。
因为海勃朗逻辑中有函数常量,因而真值指派的可能数量是无限大的。(函数可以嵌套)通过罗列各种真值指派情况的方式也是可以用来判但蕴含是否成立,但是通常需要一些限制。

2证明

海勃朗逻辑中的形式化证明同命题逻辑中类似,因为量词的存在,需要四条新的规则:

规则1Universal Introduction (UI)

UI

从任意语句到这些语句的全称量化版的语句
注v不能在φ或者任何一个当前假设中free.例如,我们通过假设p(x)获得了q(x),但是不能得出∀x.q(x),而只能先有II得到p(x)=>q(x)然后得到∀x.(p(x)=>q(x))
例:hates(jane,y)可以推出∀y.hates(jane,y),或∀x.hates(jane,y)

规则2 Universal Elimination (UE)

从一般到特殊
UE
 
注τ一定要能够替代φ中变量v
例:x.hates (jane,x)可以推出hates(jane,x)或hates(jane,y)或hates(jane,jill)

规则3 Existential Introduction (EI)

EI

注v不能在φ中出现.
例:hates(jill,jill)可以推出x.hates (x,x)或x.hates (jill,x)或y.hates (x,jill)等

规则4 Existential Elimination (EE).

EE

注:v不可出现于ψ中
例:已知x.(hates (jane,x)  ¬nicejane))和x.hates (jane,x),可得¬nice(jane))。
前提1:如果简恨任何人,则简都不算是好女孩
前提2:存在一个简恨的人
结论:简不是好女孩
一个形式化证明的示例:
给定前提1:所有人都至少爱一个人
和前提2:如果一个人是一个恋爱中的人,则所有的人都爱他;
求证:jack爱jill
ex1
实际上可以证明在给定的前提下,任何人爱任何人。
ex2

3海勃朗归结规则 Herbrand Resolution Principle

海勃朗逻辑中的归结规则同命题逻辑的命题归结规则类似,但是需要一些新的步骤。

4子句模式

海勃朗命题归结只对子句形式(clausal form)的表达可用
转换为子句模式的一般步骤:

第一步 I Implications out

φ  ψ  ¬ φ  ψ
φ  ψ  φ  ¬ψ
φ  ψ   φ  ψ )  (φ  ¬ ψ)

第二步 N negations in

¬¬φ  φ
¬(φ  ψ)  ¬φ  ¬ψ
¬(φ  ψ)  ¬φ  ¬ψ
¬ν .φ → ∃ν φ
¬ν .φ → ∀ν φ

第三步 S Standardize variables

对变量进行重命名,让每一个量词都只为一限定一个变量
x.(px) ⇒ ∃ x.q(x)) → ∀x.(px) ⇒ ∃ y.q(y))

第四步 E Existentials out

分两种情况
情况1,存在量词不在任何一个全称量词的限定中
    则:去除所有的存在量词,用一个新的常量来替代这个变量
    例x.px)  p(a)
情况2,存在量词在一个或多个全称量词的限定中
    则,因为存在量词限定的变量的值可能会受到相关全称量词的值的影响,我们用一个新的函数(以全称量词所限定的变量作为值)来替代存在量词所限定的变量。
    例:x.(px) ∧ ∃ z.q(xyz)) → ∀x.(px)  q(xyf(xy)))

第五步 A Alls out

去掉全称量词
例:x.(px)  q(xyf(xy)))  p(x)  q(xyf(xy))

第六步 D Disjunctions in

将表达式转换成conjunctive normal form
φ  ( ψ  χ )  (φ  ψ)  ( φ  χ )
(φ  ψ)  χ  (φ  χ)  ( ψ  χ )
φ  ( φ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是一个术语到变量的有限映射。
例如:{xay 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).
mgu

6归结规则

与命题逻辑中类似
resolution

factor的概念:
如果一个子句Φ中的literal的一个子集具有一个最广合一子γ,那么通过运用γ对Φ进行替换的结果 Φ'就成为是一个factor.
 

7归结推理Resolution Reasoning

同命题逻辑类似。
 
称一个resolution derivation是对一系列的子句形式前提通过有限步骤的子句终结最终得出结论的过程,其中每一个子句都要么是前提要么是通过对先前存在的子句运用归结规则所得到的子句。
reasoning

8不可满足性 Unsatisfiable

如果一系列子句形式的前提通过有限步骤的归结推理最终得到空集,则表示前提的一系列子句是不可满足的。

9逻辑蕴含

利用不可满足性知道,如果想知道一系列的前提Δ是否蕴含φ的问题,可以转变为判断Δ φ}是否是不可满足的的问题。在海勃朗逻辑中就变成将Δ φ}转变成子句形式,然后判断是否能归结推理出空集的问题。
 
以2中人人爱爱人人的例子为例:
前提为
x. y.loves(xy)
u. v.w .(loves(v,w)  loves(uv))
目标结论为
x. y.loves(xy)
即转变便为
{loves(x,f(x))}
{¬loves(v,w), loves(u,v)}
{¬loves(a,b)}
是否能归结推理出空集的问题
kkk
种种原因本周未能听完,待日后再补了。
作业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)。

Leave a Reply

Your email address will not be published. Required fields are marked *