- 课程主页: Formal Methods Foundation (csslab-ustc.github.io)
- 课程逻辑
- 课程大纲
- 考试内容: 开卷
- 命题逻辑(证明树推导, 规则使用)
- 构造逻辑(与命题逻辑区别)
- SAT(是命题逻辑部分的可满足性问题)
- Theory(谓词逻辑满足性定理)
- 符号执行/混合执行
_数学基础
计算复杂性理论
上下文无关文法
具体例子:
结构化归纳法
命题逻辑
证明系统: 自然演绎(经典命题逻辑)
基本概念
证明规则
证明–历年考题(证明规则的运用)
推导的循序是自下往上
历史考题1
考试题型: 证明题
构造逻辑
- 不能使用反证法
SAT(布尔可满足性)问题/DPLL算法
SAT是针对命题逻辑的可满足性问题
例:
穷举法
但时间增长速度快(指数级)
提出了DPLL
CNF(合取范式)
合取范式中:
- 最外层的符号都是合取
- 否定符号一定出现在原子命题前
- 不能有蕴含(->)符号
_解析和传播
不做过多解释
CNF不可解–解析推出矛盾
CNF解析不冲突–传播
DPLL
bcp通俗来说: 两个命题中有一个是原子命题(p), 另一个是含有p析取(~/否定)的复合命题, 传播得出等价的不含原子命题的新命题(q)
SAT vs. valid
SAT基于的是命题逻辑(不接受排中律, 可以用反证法)
谓词逻辑
谓词逻辑是命题逻辑的细化
新增(相对命题逻辑)的概念:
x是自由变量, y是绑定变量, 替换操作只能针对自由变量. α重命名不能让变量名冲突
计算绑定变量
计算自由变量
一个变量有可能同时是绑定变量和自由变量(例子中的y)
替换规则
输入: 命题
输出: 命题
只替换自由变量, 替换前要求解绑定/自由变量, 自由变量替换前要进行α重命名
证明系统: 自然演绎
原先的命题逻辑规则和推导方法证明系统: 自然演绎(经典命题逻辑) 在这里也适用, 这里只列出了新增的四条规则
SMT可满足性模理论
求解谓词逻辑可满足性求解
理论是谓词逻辑语法的子集
等式理论/EUF理论
线性算数(LA)理论
消元法
例子 : (考试要考消元法)
往上代入, 有一组解
说明这一组约束是可满足的
_单纯形法
_分支定界
不考
…
比特向量理论
- 有符号
- 无符号
数组理论
分类讨论: z<i / z=i / z>i
指针理论: 内存模型
地址T 值类型E 关系R 复合命题P
决策过程优化方法: