命题逻辑的▣顾 命题逻辑是可靠的和完备的 命题逻辑的可靠性 若T w是有效的（可证明的），则T w成 立 命题逻辑的完备性 若Tw成立，则T w是有效的 命题逻辑的可靠性和完备性 T w有效，当且仅当 w成立
命题逻辑的回顾 • 命题逻辑是可靠的和完备的 – 命题逻辑的可靠性 若 是有效的（可证明的），则 成 立 – 命题逻辑的完备性 若 成立，则 是有效的 – 命题逻辑的可靠性和完备性 有效，当且仅当 成立
谓词逻辑的回顾 合式公式 谓词符号集合、函数符号集合 (包括常量符 号)》 -基于 来定义项集 t::=xc ft,...,t) 归纳地定义基于(， )的合适公式 φ：=P(t1,t2,,tn)1(φ)1（φvφ）1（φ∧φ）1 (中→中)1(xφ)|（目xφ） (P∈ ·自由变量、约束变量、代换
谓词逻辑的回顾 • 合式公式 – 谓词符号集合 、函数符号集合 （包括常量符 号） – 基于 来定义项集 t ::= x | c | f(t, …, t) – 归纳地定义基于（ , ）的合适公式 ::= P(t1 , t2 , …, tn ) | ( ) | ( ) | ( ) | ( → ) | (x ) | ( x ) ( P ) • 自由变量、约束变量、代换
谓词逻辑的回顾 新增推理规则（包括公理） 一项相等的证明规则 一全称量词证明规则 一存在量词证明规则 -量词间的等价规则 语义模型、可靠性、完备性 一它们都可以基于命题逻辑相应概念进行拓展 -T 中和T yw的意思与前面的一致 Ψw表示y在模型 中成立
谓词逻辑的回顾 • 新增推理规则（包括公理） – 项相等的证明规则 – 全称量词证明规则 – 存在量词证明规则 – 量词间的等价规则 • 语义模型、可靠性、完备性 – 它们都可以基于命题逻辑相应概念进行拓展 – 和 的意思与前面的一致 – 表示在模型 中成立
形式证的动机 形式验证技术由三部分组成 一用于系统建模的框架，通常是某种描述语言 一用于描述待验证性质的规范语言 一用来确立系统描述是否满足规范的验证方法 基于逻辑推理的方法 -系统描述是适当逻辑中的一组公式 待证性质的规范是另一个公式 验证就是试图通过该逻辑的公理和推理规则来证 明T
形式验证的动机 • 形式验证技术由三部分组成 – 用于系统建模的框架，通常是某种描述语言 – 用于描述待验证性质的规范语言 – 用来确立系统描述是否满足规范的验证方法 • 基于逻辑推理的方法 – 系统描述是适当逻辑中的一组公式 – 待证性质的规范是另一个公式 – 验证就是试图通过该逻辑的公理和推理规则来证 明
形式证的动机 ·形式验证技术由三部分组成 基于逻辑推理的方法 -系统描述是适当逻辑中的一组公式工 -待证性质的规范是另一个公式少 一验证就是通过该逻辑来证明 基于模型的方法 -系统由适当逻辑的某个模型 表示 -待证性质的规范仍由公式表示 验证就是计算模型是否满足中( )
形式验证的动机 • 形式验证技术由三部分组成 • 基于逻辑推理的方法 – 系统描述是适当逻辑中的一组公式 – 待证性质的规范是另一个公式 – 验证就是通过该逻辑来证明 • 基于模型的方法 – 系统由适当逻辑的某个模型 表示 – 待证性质的规范仍由公式表示 – 验证就是计算模型 是否满足（ ）