数理逻辑 复习提纲（11级）

数理逻辑 复习提纲

（请按照下面的内容复习，有问题随时到我的办公室答疑） 命题逻辑语法的BNF范式及其解释。 命题逻辑的可靠性和完全性定理. 谓词逻辑语法的BNF范式及其解释。

线性时态逻辑的语法的的BNF范式及其解释。 分支时态逻辑的语法的的BNF范式及其解释。 谓词逻辑的可靠性和完全性定理. 谓词逻辑的不可判定性

Horn formula 的定义及其可满足性算法.. 线性和立方SAT solver局限性。

一阶逻辑和高阶逻辑在语法和表达能力差别？

一阶谓词逻辑的项和公式是如何定义的，写出他们的BNF范式并解释之。 解释常用的线性时态逻辑公式的含义。 解释常用的分支时态逻辑公式的含义。 程序的部分正确定性证明规则。 简单的程序部分正确性证明。 了解Model Checker 和NuSMV。

会用命题逻辑的自然演绎系统规则推导简单的命题逻辑公式。 会用谓词逻辑逻的自然演绎系统规则推导简单的谓词逻辑公式。

二

命题逻辑语法的BNF范式及其解释。

??p|(??)|?(??)|?(??)?|?( ? P代表任意原子命题，：：=右边的?和每一次出现都表示任何已经构造好的公式。 命题逻辑的可靠性和完全性定理.

设?1,?2,...,?n和?是命题逻辑公式。若?1,?2,...,?n|??成立时，?1,?2,...,?n|??成立，则是可靠的。

若?1,?2,...,?n|??成立时，?1,?2,...,?n|??成立，则是完全的。 谓词逻辑语法的BNF范式及其解释。

:P(t,t2,...)?|(??)?|( ?:?1nt,???)?|(??)?|(?x?)|?x()|p(??是)1?n元的谓 ?其中

词符号，ti是F上的项，x是变量。在：：=的右边，?的每次出现都表示由上述规则构造出来的任意公式。

线性时态逻辑的语法的的BNF范式及其解释。

?:?:?|(??)p||??(?)|?(??)?|?(?)?|(?X ???)F|(?G)|(?U)|?(?W)?|(?R其中P是取自某原子集atoms的任意命题原子。连接词X,F,G,U,R和W称为时态连接词。 分支时态逻辑的语法的的BNF范式及其解释。

?::??|(??)|p|(??)|(???)|(???)|(???)|AX?|EX?|AF?|EF?|AG?|EG?|A[?U?]|E[?U?] 此处p取遍原子公式的集合。每个CTL时态连接词都是一对符号。对中的第一个是A或E。A是“沿所有路径”（无一例外），E的含义是“沿至少（存在）一条路径”（可能）。

谓词逻辑的可靠性和完全性定理. 谓词逻辑的不可判定性

谓词逻辑中的有效性问题是不可判定的：不存在对任意给定的?，判定|=?是否成立的程序。波斯特

Horn formula 的定义及其可满足性算法.

霍恩(Horn)公式是命题逻辑公式?，如果它可以用下列语法作为H的实例产生： P:??:|?(? A:?:p|P? C::?A?p H:?:C|C? H)p|

A Function HORN(?)

/* 前置条件：?是霍恩公式*/

/* 后置条件： HORN(?)判定?的可满足性*/ Begin function

标记所有在?中出现的（??）；

While ?中合取p1?p2?...?pik?p'的所有pj都被标记时，do标记p' End while

If ?被标记 then return “不是可满足的”， Else return “可满足的” End function

线性和立方SAT solver局限性。

无法判定形如?(?1??2)的公式是否是可满足的。

一阶逻辑和高阶逻辑在语法和表达能力差别？

一阶逻辑指：命题逻辑和谓词逻辑。高阶逻辑指将量词不仅应用于变量，而且应用于谓词符号而产生的二阶逻辑，如果对关系的关系取量词，就可以得到三阶逻辑，等等。

阶：只刻画个体性质或关系的谓词是一阶谓词，从而公式的形式看，一阶谓词只作用到个体变量或个体常量上。当对谓词变量进行量化时，就进入了高阶谓词逻辑的范围了。

谓词逻辑比命题逻辑有更强大的表达能为，它有谓词，函数符号和量词符号。但这是以牺牲有效性，可满足性和可证明性的不可判定性为代价的。而谓词不能表达可达性，高阶逻辑可以表达，但高阶逻辑在像完备性和紧密性这样的典型结果可能很快就不再成立。而且一个朴素的高阶逻辑在元逻辑级上可能是不相容的。

一阶谓词逻辑的项和公式是如何定义的，写出他们的BNF范式并解释之。 项定义如下：

任何变量都是项；

若c?F是零元函数，则c是项。

若t1,t2,...,tn是项，且f?F的元n>0，则f(t1,t2,...,tn)是项。 没有其它形式的项。

用backus naur范式，可以写：

t::?x|c|f(t1,t2,...,tn)，其中x取遍F中的零元函数符号，f取遍F中的元n>0的符号。 解释常用的线性时态逻辑公式的含义。 解释常用的分支时态逻辑公式的含义。 程序的部分正确定性证明规则。

???C??????C2???Composition

???C1;C2???1??[E/x]?x?E???Assignment

???B?C1???????B?C2???Lf_statement

???ifB{C1}else??????B?C???Partial_while ???whileB{C}????B?|?AR???;???C???;|?AR???''???C???''Implied

简单的程序部分正确性证明。 了解Model Checker 和NuSMV。

NuSMV(有时简称SMV)提供描述一种用图来描述的模型的语言，而且可以直接验证基于这个模型的LTL(或CTL)公式的有效性。SMV的输入是由描述模型的程序和一些规范(时态逻辑公式)组成。若规范成立，它产生输出“真”，否则显示一个迹，表明为什么关于程序所表示的模型该规范是假的。

会用命题逻辑的自然演绎系统规则推导简单的命题逻辑公式。 会用谓词逻辑逻的自然演绎系统规则推导简单的谓词逻辑公式。