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

更新时间：2023-10-14 08:13:01 阅读量：综合文库文档下载

说明：文章内容仅供预览，部分内容可能不全。下载后的文档，内容与下面显示的完全一致。下载之前请确认下面内容是否您想要的，是否完整无缺。

数理逻辑推荐度：
相关推荐

数理逻辑复习提纲

（请按照下面的内容复习，有问题随时到我的办公室答疑）命题逻辑语法的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)的公式是否是可满足的。