程序验证(一):命题逻辑

Tattoo

发布日期: 2020-06-28 12:56:21 浏览量: 68
评分:
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/106418540

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

一、概念

1.1 命题逻辑

例如:

  • 一个原子(atom)是一个或为真或为假的判断

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

  • 命题公式(propositional formulas)由文字和逻辑连接符组成

1.2 合式公式

合式公式(well-formed formulas) 由以下语法得到:

举例

1.3 语义

目的:给命题逻辑赋予涵义,把布尔值赋值给(公式,解释)对,即

什么是解释?

对于一个命题公式FF,一个解释IIFF中每个命题变元映射为一个布尔值,也就是说:

满足解释

如果命题公式在解释II下值为真,那么说IIFF的满足解释(satisfying interpretation),记作:

不满足解释

如果命题公式在解释II下值为假,那么说IIFF的不满足解释(falsifying interpretation),记作:

语义的归纳定义

首先定义原子的涵义,然后根据这些定义,定义每个逻辑连接的涵义。

举例:

1.4 可满足性与永真性

一个公式FF可满足的(satisfiable)当且仅当存在一个解释II使得IFI\models F

一个公式FF永真的(valid)当且仅当对于所有解释IIIFI\models F

注意:可满足性与永真性是成对的(dual)符号,即FF是永真的当且仅当¬F\neg F是不可满足的。

如何证明可满足性?

  • 真值表穷举:蛮力搜索复杂度为2n2^n,其中nn为变元的数量

  • 演绎推理:语义讨论(Semantic Argument)

    • 假定FF为非永真的,即存在II不满足FF

    • 应用推理规则

    • 如果每一分支都得到矛盾,那么FF是永真的

    • 如果没有矛盾,且不能进一步应用推理规则,那么FF是非永真的

二、语义规则

2.1 公式

这个规则产生了分支:

例子1:

例子2:

发现矛盾,所以FF是永真的。

注意\Rightarrow 这样的双线箭头不属于命题逻辑的符号集。

三、范式(Normal Forms)

3.1 概念

一种逻辑的范式,应当:

  • 限制公式的语法(Restricts the syntax of formulas)

  • 对于此逻辑中的任意公式,范式具有等价的表达能力(Has equivalent representation for any formula in the logic)

3.2 三种主要范式

Negation Normal Form (NNF):只包含 \wedge\vee¬\neg 三个符号,且 ¬\neg 只能用于文字(literal)。

Disjunctive Normal Form (DNF):合取子句的析取。

Conjunctive Normal Form (CNF):析取子句的合取。

举例:

四、范式转化

由于主流的SAT solver(就是一个程序,输入一个公式,输出这个公式是否是可满足的,例子见一个简单的DPLL实现)一般接受CNF为输入,所以面对一个一般的公式,我们需要先把它转化为一个CNF。如何实现?等价的转换比较困难,但是我们可以采用一种逻辑上更弱的方法,即进行可满足性等价(equisatisfiability)转换。也就是说,我不要求转换后的CNF与原来的公式在所有的解释下真值都一样,我只要求若CNF可满足,则原公式可满足;若原公式可满足,则CNF可满足。

转换的方法,可采用 Tseitin 算法.

上传的附件

发送私信

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

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