程序验证(三):一阶逻辑

Tattoo

发布日期: 2020-06-29 13:49:44 浏览量: 135
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106563439

注意:原文中有部分公式书写错误,本文转载的时候,修正了这部分错误!

一、语法

1.1 逻辑符号

包括:

  • 命题连接符\wedge, \vee ,¬ \neg , \to , \leftrightarrow

  • 变元vv, yy, zz, x1x_1, x2x_2, …

  • 量词\exists, \forall

1.2 非逻辑符号(参数)

包括:

  • 常量c1c_1, c2c_2, …

  • 函数符号gg, hh, ff, f1f_1, f2f_2, …

  • 谓词符号rr, qq, pp, p1p_1, p2p_2, …
    谓词与函数符号通过元数(arity)联系起来,也就是:
    元数:一个描述参数数量的自然数
    举例:

    • =:: arity 2
    • f(a,b,c): arity 3
  • 常量:可以视为0元函数

1.3 项(term)

项是用来描述对象的表达式。定义:

  • 常量是项

  • 变量是项

  • 对于n元函数符号fff(t1,..,tn)f(t_1, .., t_n)是一个项,如果t1,..,tnt_1, .. ,t_n是项

1.4 原子公式(atom)

一阶逻辑(FOL)中的原子公式取值或为真、或为假。定义:

  • 对于\bot\top均为原子

  • 对于每个n元谓词符号ppp(t1,..,tn)p(t_1, .., t_n)是一个原子如果t1,..,tnt_1, .. , t_n是项

  • 一个文字(literal)是一个原子或它的非

1.5 公式(formula)

一个一阶逻辑公式是:

  • 一个文字

  • 使用¬,,,,\neg ,\wedge ,\vee ,\to ,\leftrightarrow连接的公式

  • 使用量词(quantifier)的公式(两种量词)

    • 全称量词 x.F[x]\forall x.F[x]: For all xx, F[x]F[x]

    • 存在量词 x.F[x]\exists x.F[x]: There exists an xx such that F[x]F[x]

    其中,xx是约束变元(quantified variable),F[x]F[x]是量词的辖域(scope),xxF[x]F[x]中被量词约束(bind)。如果FFyy没有被任何量词约束,那么它是自由(free)的

一阶逻辑公式的一些名称:

  • 一个不包含自由变量的公式是关闭的(closed)(也叫做一个句子)

  • 一个包含自由变量的公式是开放的(open)

  • 一个不包含任何变量的公式是ground

1.6 一阶逻辑表达式举例

“All cats have more days than dogs”

x,y.dog(x)cat(y)ndays(y)>ndays(x)\forall x,y.dog(x)\wedge cat(y)\to ndays(y) > ndays(x)

“The numeric array a is sorted”

i.0i<aa[i]a[i+1]\forall i.0\le i < |a|\to a[i] \le a[i+1]

“Graph G contains a triangle”

v1,v2,v3.e(v1,v2)e(v2,v3)e(v3,v1)\exists v_1 ,v_2 ,v_3 .e(v_1, v_2)\wedge e(v_2, v_3)\wedge e(v_3, v_1)

二、语义

一个一阶逻辑解构是一个对(pair)S=(D,I)S=(D,I)

  • 其中DD是论域(universe of discourse),也就是说,一个我们要讨论的对象的非空集合

  • 其中II是解释,是以下三种映射(map):

    • 从每个常量到DD中的一个值

    • 每个n元函数变量ff到n元函数:

      fI:DnDf_I:D^n \mapsto D

    • 每个n元谓词符号p到n元关系:

      pIDnp_I \subseteq D^n

一个赋值(assignment)α:VarsD\alpha : Vars\to D将每个变量映射到DD中的一个值。

举例:

x+y>zy>zxx+y > z\to y>z-x

  • 论域D=Z={..,1,0,1,..}D=Z = \lbrace .., -1,0,1, .. \rbrace

  • 解释

    • 函数符号:++Z,Z+\mapsto +{Z}, - \mapsto -{Z}

    • 谓词符号:>>Z> \mapsto >_{Z}

  • 一个可能的赋值α={x0,y1,z1}\alpha = \lbrace x\mapsto 0,y\mapsto 1, z\mapsto -1 \rbrace

2.1 项求值

给定解释II以及赋值α\alpha,我们可以计算项在DD中的值。给定一个项aaaa的值I,α(a)\langle I,\alpha \rangle (a)是:

  • 如果aa为常量:I,α(a)=I(a)\langle I,\alpha \rangle (a) = I(a)

  • 如果aa为变量:I,α(v)=α(v)\langle I,\alpha \rangle (v) = \alpha (v)

  • 如果a=f(t1,..,tn)a=f(t_1, .. , t_n)是一个函数项:I,α(f(t1,..,tn))=I(f)(I,α(t1),..,I,α(tn))\langle I,\alpha \rangle (f(t_1, .. ,t_n)) = I(f)(\langle I,\alpha \rangle (t_1),..,\langle I, \alpha \rangle (t_n))

2.2 公式求值

给定DD, II, α\alpha,令FF为一阶逻辑公式,我们有:

D,I,αF if F evaluatesto trueD,I, \alpha \models F \space if \space F \space evaluates to \space true

D,I,αF if F evaluatesto falseD,I, \alpha \nvDash F \space if \space F \space evaluates to \space false

对于原子:

D,I,α and D,I,αD,I, \alpha \models \top \space and \space D,I, \alpha \nvDash \bot

D,I,αp(t1,..,tn) iff (I,α(t1),..,I,α(tn))I(p)D,I, \alpha \models p(t_1,..,t_n) \space iff \space (\langle I, \alpha\rangle (t_1),..,\langle I, \alpha \rangle (t_n)) \in I(p)

对于复合情况下的归纳定义:

D,I,α¬F iff D,I,αFD,I,\alpha \models \neg F \space iff \space D,I,\alpha \nvDash F

D,I,αF1F2 iff D,I,αF1 and D,I,αF2D,I,\alpha \models F_1\wedge F_2 \space iff \space D,I,\alpha \models F_1 \space and \space D,I,\alpha\models F_2

D,I,αF1F2 iff D,I,αF1 or D,I,αF2D,I,\alpha \models F_1\vee F_2 \space iff \space D,I,\alpha \models F_1 \space or \space D,I,\alpha\models F_2

D,I,αF1F2 iff D,I,αF1 or IF2D,I,\alpha \models F_1 \to F_2 \space iff \space D,I,\alpha \nvDash F_1 \space or \space I\models F_2

D,I,αF1F2 iff D,I,αF1 and IF2 ,or D,I,αF1 and D,I,αF2D,I,\alpha\models F_1 \leftrightarrow F_2 \space iff \space D,I,\alpha \models F_1 \space and \space I\models F_2 \space, or \space D,I,\alpha \nvDash F_1 \space and \space D,I,\alpha \nvDash F_2

举例:

对于论域D=,D={\circ, \bullet},赋值α=x,y\alpha = {x\mapsto \bullet , y\mapsto \circ},以及II

I(a)=I(a) = \circ

I(f)=(,),(,),(,),(,)I(f) = {(\circ , \circ)\mapsto \circ ,(\circ ,\bullet)\mapsto \bullet ,(\bullet ,\circ)\mapsto \bullet ,(\bullet ,\bullet)\mapsto \circ}

I(g)=,I(g) = {\circ\mapsto\bullet ,\bullet\mapsto\circ}

I(p)=(,),(,)I(p) = {(\circ ,\bullet),(\bullet ,\bullet)}

p(a,g())=truep(a,g(\circ)) = true

p(x,f(g(x),y))p(y,g(x))=truep(x,f(g(x),y))\to p(y,g(x)) = true

2.3 量词求值

给定一个变元xx,以及一个赋值α\alpha,一个α\alphaxx变元,写作α[xc]\alpha [x\mapsto c],是这样的赋值:

  • xx外的变量都与α\alpha取值相同

  • xx赋值为某个给定的值cDc\in D,那么我们可以这样表示量词:

    全称量词:

    D,I,αx.F iff for all cD,D,I,α[xc]FD,I,\alpha \models \forall x.F \space iff \space for \space all \space c\in D,D,I,\alpha [x\mapsto c]\models F

    存在量词:

    D,I,αx.F iff there exists cD,D,I,α[xc]FD,I,\alpha \models \exists x.F \space iff \space there \space exists \space c\in D,D,I,\alpha [x\mapsto c]\models F

2.4 可满足性与永真性

一个一阶逻辑公式FF是可满足的当且仅当:存在S=(D,I)S=(D,I)以及赋值α\alpha使得D,I,αFD,I,\alpha \models F

一个一阶逻辑公式FF是永真的当且仅当:对于所有S=(D,I)S=(D,I)以及赋值α\alphaD,I,αFD,I,\alpha \models F

FF是永真的时,记作F\models F

可满足性与永真性二者是对偶的。

三、证明系统

3.1 永真性证明

类似于命题逻辑中的证明方法:

  • 假定FF不是永真的,存在II使得IFI \nvDash F

  • 应用证明规则

  • 如果没有矛盾,没有能够继续应用的证明规则,那么得出结论:FF是非永真的

  • 如果每一个分支都推出矛盾,得出结论:FF是永真的

3.2 证明规则

全称量词1

如果我们知道D,I,αx.p(x,α)D,I,\alpha\models \forall x.p(x,\alpha),那么我们得出结论:D,I,α[xb]p(x,a)D,I,\alpha [x\mapsto b]\models p(x,a)

全称量词2

这里,fresh的意思是在证明中没有用过。

如果D,I,αx.FD,I,\alpha \nvDash \forall x.F,那么我们只知道FF对于某些对象不成立,但我们不知道对哪个对象不成立。

因此,我们选择一个新的(fresh),不做假设。

存在量词1

存在量词2

不论xx映射为什么,FF都不成立。

3.3 得到矛盾

前两个前提的赋值都是α\alpha的variant,只要pp的值不同,矛盾就产生了。

例如:

举例:证明以下公式是永真的

F:(x.p(x))(y.p(y))F: (\forall x.p(x))\to (\forall y.p(y))

3.4 可靠性与完备性(soundness and completeness)

  • 可靠性:如果语义分析(semantic argument)的每一分支都得到矛盾,那么FF是永真的。也就是说,证明规则不会得到错误的结果

  • 完备性:如果FF是完备的,那么存在一个有限长的证明序列,其中每一分支都能得到矛盾。也就是说,不存在我们不能证明为永真式的永真式。这叫做指称完备性(refutational completeness)。

四、一阶逻辑的可判定性

一个判定问题当且仅当存在一个过程PP满足对于任何输入:

  • 答案为真时,停机并输出真

  • 答案为假时,停机并输出假

一阶逻辑是不可判定的(丘奇(Church)&图灵(Turing)),但一阶逻辑是半可判定的,即当FF是永真的时,程序总是终止,当FF不是永真的时,程序可能不终止。

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

93
文章数
34
评论数
最近文章
eject