形式化建模与分析方法-笔记

第五章

命题逻辑

定义

定义3-1 对事物作出确定判断的陈述句称为命题。
当符号P表示一个确定命题时，该符号称为命题常元。
当符号P表示任意一个命题时，该符号称为命题变元。
原子命题：原子命题是不能再细分的命题
复合命题：原子命题通过命题联结词构造的命题。
（命题联结词：非 合取 析取 蕴含 等价）
定义3-7
命题公式也称为合式公式、公式，递归方式定义如下：
（1）单个命题变元和命题常元是一个命题公式；
（2）P和Q是命题公式， ¬P、P∧Q、P∨Q、P→Q、P↔Q也是命题公式；
（3）有限次应用上述2条规则得到的符号串也是命题公式。
定义3-8
如果命题公式G中含有n个命题变元\(P_1、P_2⋯、P_n\)，称G为n元命题公式，可以表示为\(G(P_1、P_2⋯、P_n)\)。
给\(P_1、P_2⋯、P_n\)分别指定相应的真值，称为对公式G的一种指派或解释。
若指定的一组值使得G真值为1，则称这组值为G的成真指派。
若使得G的真值为0，则称这组值为G的成假指派。
定义3-10
命题公式G，P_1、P_2…是G中的所有命题变元，那么：
（1）如果命题公式G在所有指派下真值为1，称公式G为永真式或重言式。
（2）如果命题公式G在所有指派下真值为0，称公式G为永假式或矛盾式。
（3） 如果命题公式G在有些指派下真值为1，有些指派下真值为0，称公式G为可满足式。

公式

1. 双重否定律：¬¬G=G
2. 幂等律：G=G∨G，G=G∧G
3. 交换律：G∨H=H∨G，G∧H=H∧G
4. 结合律：(G∨H)∨S = G∨(H∨S)，(G∧H)∧S = G∧(H∧S)
5. 分配律：G∧(H∨S)=(G∧H)∨(G∧S)，G∨(H∧S)= (G∨H)∧(G∨S)
6. 德摩根律：¬(G∧H)=¬G∨¬H，¬(G∨H)=¬G∧¬H
7. 吸收律：G∧(G∨H)= G，G∨(G∧H)=G
8. 零律：G∨1=1，G∧0=0
9. 同一律：G∨0=G，G∧1=G
10. 排中律：G∨¬G=1
11. 矛盾律：G∧¬G=0
12. 蕴涵等值式：G→H =¬G∨H
13. 等价等值式：G↔H =(G→H)∧(H→G)
14. 假言移位： G→H =¬H→¬G
15. 归谬律: (G→H)∧(G→¬H) = ¬G
    

谓词逻辑

程序正确性证明

• Floyd前后断言法
• Floyd良序集法
• Hoare公理化方法
• Dijkstra最弱前置法