计算机科学中使用的数理逻辑-期末考试题2006到2014

12006年秋季研究生课程《计算机科学中使用的数理逻辑》试卷任课教师刘西洋考试时间：1月24日上午8：30－10：30地点：西406、407、408、409、410、411（自然语言到谓词逻辑的翻译10分）1、(逻辑公式的结构20分)（1）给出命题逻辑公式(((p)↔(qr))→(rp))的语法树（10分）（2）给出一阶谓词逻辑公式x(F(b)→y(zG(y,z)H(u,x,y)))的语法树（10分）2（量词20分）基于全称量词、存在量词以及等词=或，定义以下扩展的量词：（1）存在至少2个（8分）（2）存在至多2个（7分）（3）存在恰好3个（5分）3（有限论域上一阶谓词逻辑到命题逻辑的翻译20分）45（《面向计算机科学的数理逻辑》引理4.4.1结论(i)20分）6(OBDDOBDD论文10分)→↔22007年秋季研究生课程《计算机科学中使用的数理逻辑》试卷任课教师：刘西洋考试时间：2小时地点：西大楼班级：学号：姓名：1、逻辑公式的结构（20分)（1）给出命题逻辑公式(((¬p)↔(q⋁r))→(r⋀p))的语法树（10分）（2）给出一阶谓词逻辑公式∀x(F(b)→∃y(∀zG(y,z)⋁H(u,x,y)))的语法树（10分）2、证明（20分）（1）（A→B）⋁（A→C）⊭A→(B⋀C)（10分）（2）A→(B⋁C)⊭（A→B）⋀（A→C）（10分）3、根据命题逻辑的形式推演证明下述定理（20分）（1）¬¬A⊢A（10分）（2）A⊢¬¬A（10分）4、由（Ref），（+），（→+）和下面的：如果∑⊢¬¬A，则∑⊢A.证明（¬−）.（10分）其中：（Ref）A⊢A（+）如果∑⊢A，则∑，∑’⊢A.（→+）如果∑,A⊢B,则∑⊢A→B.5、语句集{∀x∃yF(x,y),∀x¬F(x,x),∀x∀y∀z[F(x,y)⋀F(y,z)→F(x,z)]}在无限论域中是可满足的，但在有限论域中是不可满足的。（10分）6、设A∈Form（ℒp）含不同的原子公式p1,…,pn,v是真假赋值。对于i=1，…,n,令viiiipp1Ap如果否则证明：（1）Av=1⇒A1,…,An⊢A（2）Av=0⇒A1,…,An⊢¬A（只考虑A为¬B和B1→B2两种形式）（20分）32008年秋季研究生课程《计算机科学中使用的数理逻辑》试卷任课教师：刘西洋考试时间：2小时1、逻辑公式的结构（20分)（1）给出命题逻辑公式(((¬(p⋁s))↔(q⋁r))→(r⋀(p⋁s)))的语法树（5分）（2）给出（1）中命题逻辑公式共用子结构的有向无环图（10分）（3）给出一阶谓词逻辑公式∀x(F(a)→∀y(∃zG(x,y,z)⋁H(u,x,y)))的语法树（5分）2、证明（20分）（1）（A⋀B）→C⊭(A→C）⋀(B→C）（10分）（2）（A→C）⋁(B→C)⊭（A⋁B）→C（10分）3、根据命题逻辑的形式推演证明下述定理（20分）（1）如果A⊢B，则¬B⊢¬A（10分）（2）A⋀¬B⊢¬（A→B）（10分）4、证明（10分）¬∀xA（x）⊢∃x¬A（x）.5、构作语句（可以使用相等符号）使得（1）它在有一个或是两个个体的论域中是有效的，但在更大的论域中是不有效的.（7分）（2）它在有不超过三个个体的论域中是有效的，但在更大的论域中是不有效的.（8分）6、设∑是有限集，由⊢A⊨A证明∑⊢A∑⊨A（15分）42009年秋季研究生课程《计算机科学中使用的数理逻辑》试卷任课教师：刘西洋考试时间：2小时1.证明（20分）（1）（A→B）⋁（A→C）⊭A→(B⋀C)（5分）（2）(A→C)⋁(B→C)⊭(A⋁B)→C（5分）（3）∃x∀yA(x,y)╞∀y∃xA(x,y)（5分）（4）∀y∃xA(x,y)⊭∃x∀yA(x,y)（5分）2.根据命题逻辑和一阶谓词逻辑的形式推演证明下述定理（15分）（1）A→B，¬A→B⊢B（5分）（2）A→B，A→¬B⊢¬A（5分）（3）¬∃xA(x)┠┨∀x¬A(x)（5分）3.证明语句集（15分）{∀x∃yF(x,y),∀x¬F(x,x),∀x∀y∀z[F(x,y)⋀F(y,z)→F(x,z)]}在无限论域中是可满足的，但在有限论域中是不可满足的。4.基于全称量词∀、存在量词∃以及等词=或≠，定义以下扩展量词（10分）（1）存在至少2个（3分）（2）存在至多2个（3分）（3）存在恰好3个（4分）5.对于一阶谓词逻辑公式集∑和一阶谓词逻辑公式A，已知“如果∑是可满足的，则∑是协调的”，证明“如果∑⊢A，则∑⊨A”（10分）6.设∑是极大协调集，则对于任何公式A和B，证明：（10分）（1）A∧B∈∑，当且仅当A∈∑并且B∈∑（5分）（2）A→B∈∑,当且仅当A∈∑蕴涵B∈∑（5分）7.布尔函数122313123fxxxxxxxxx的BDD如图1所示。其中x1是根节点，例点1、例点2为非终节点，0、1为终节点，虚线表示取0实线表示取1。（10分）5图1函数f的BDD定义1：当沿着某个BDD的根节点向下搜索时，若每个节点在每条分支上出现的次数最多一次且变量出现的顺序相同，则把BDD称作偏序BDD（OrderedBDD）。定义2：当一个OBDD中不包含同构子图且节点的两条分支不指向同一个节点时，称这个OBDD为约简的偏序BDD（ReducedandOrderedBDD,ROBDD）问题1：对于图1，我们选取变量序为1x、2x、3x，请判断它是否为OBDD。问题2：化简OBDD为ROBDD，可以参照以下步骤：a)合并相同的终节点：合并终节点中相同的节点，使之最多只有两个终节点，取值为0、1；b)去除同构子图：对非终节点u、v，如果满足以下三个条件，则删除其中一个节点，将删除节点的所有入边指向保留节点。Low()/high()分别表示取0取1。()()()()()()VaruVarvLowuLowvHighuHighvc)删除无效节点：如果有()()LowvHighv，则删除节点v，并把它的所有入边指向()Lowv。68.SAT（BooleanSatisfactionProblem,SAT）的完备算法中DPLL算法尤其突出。请描述DPLL算法思想，并判断以下实例是否可满足，如果可满足，在图中画出算法走过的相应路径。（10分）可满足性问题：(,)CV变量集合：{,,,}Vabcd变量顺序：1234{(),(),(),()}VaVbVcVd子句：12345678()()()()()()()()cabccacdcacdcacdcacdcbcdcabccabc图2真值赋值搜索空间72010年秋季研究生课程《计算机科学中使用的数理逻辑》试卷任课教师：刘西洋考试时间：2小时9.证明（20分）1)A→(B⋁C)⊭(A→B)⋀(A→C)（5分）2)(A⋀B)→C⊭(A→C)⋀(B→C)（5分）3)∃xA(x)⋀∃xB(x)⊭∃x[A(x)⋀B(x)]（5分）4)∀xA(x)⋁∀xB(x)╞∀x[A(x)⋁B(x)]（5分）10.根据命题逻辑和一阶谓词逻辑的形式推演证明下述定理（15分）1)A→¬B⊢B→¬A（5分）2)如果A⊢B,则¬B⊢¬A（5分）3)¬∀xA(x)┠┨∃x¬A(x)（5分）11.证明（15分）()Form是协调的，当且仅当存在A，使得A。12.构作语句（可以使用相等符号）使得它在论域D中是可满足的，当且仅当：（10分）1)D有一个个体（2分）2)D有三个个体（2分）3)D有至多三个个体（3分）4)D有至少三个个体（3分）13.给出一阶谓词逻辑公式∀x(F(b)→∃y(∀zG(y,z)⋁H(u,x,y)))的语法树（10分）814.布尔函数122313123fxxxxxxxxx的BDD如图1所示。其中x1是根节点，例点1、例点2为非终节点，0、1为终节点，虚线表示取0实线表示取1。（20分）图1函数f的BDD定义1：当沿着某个BDD的根节点向下搜索时，若每个节点在每条分支上出现的次数最多一次且变量出现的顺序相同，则把BDD称作偏序BDD（OrderedBDD）。定义2：当一个OBDD中不包含同构子图且节点的两条分支不指向同一个节点时，称这个OBDD为约简的偏序BDD（ReducedandOrderedBDD,ROBDD）问题1：对于图1，我们选取变量序为1x、2x、3x，请判断它是否为OBDD。问题2：化简OBDD为ROBDD，可以参照以下步骤：d)合并相同的终节点：合并终节点中相同的节点，使之最多只有两个终节点，取值为0、1；e)去除同构子图：对非终节点u、v，如果满足以下三个条件，则删除其中一个节点，将删除节点的所有入边指向保留节点。Low()/high()分别表示取0取1。()()()()()()VaruVarvLowuLowvHighuHighvf)删除无效节点：如果有()()LowvHighv，则删除节点v，并把它的所有9入边指向()Lowv。15.对OBDD应用ITE（IF-THEN-ELSE）运算法。（10分）ITE运算特别适合OBDD，它是一种三元运算，如式（1）所示。其用统一的方式来表示布尔函数的基本运算，所有的一元、二元逻辑函数都可用ITE算法来实现。(,,)itefghfgfh式（1）问题1：例如x1+x2可以用ite(x1,1,x2)来表示，那么x1*x2用ITE如何表示？问题2：设函数f=x1+x2,g=x1*x2，例如函数f的ITE运算如图2所示（这里B无意义，仅起指代作用），那么请画出函数g的ITE运算示意图。102011年秋季研究生课程《计算机科学中使用的数理逻辑》试卷任课教师：刘西洋考试时间：2小时16.证明（20分）（1）()()()ABCACBC（5分）（2）()()()ACBCABC（5分）（3）∃x∀yA(x,y)╞∀y∃xA(x,y)（5分）（4）∀y∃xA(x,y)⊭∃x∀yA(x,y)（5分）17.根据命题逻辑和一阶谓词逻辑的形式推演证明下述定理（15分）（1）A⊢¬¬A（5分）（2）A→B，A→¬B⊢¬A（5分）（3）¬∃xA(x)┠┨∀x¬A(x)（5分）18.证明语句集（15分）{∀x∃yF(x,y),∀x¬F(x,x),∀x∀y∀z[F(x,y)⋀F(y,z)→F(x,z)]}在无限论域中是可满足的，但在有限论域中是不可满足的。19.基于全称量词∀、存在量词∃以及等词=或≠，定义以下扩展量词（10分）（1）存在至少2个（3分）（2）存在至多2个（3分）（3）存在恰好3个（4分）5．设A∈Form（ℒp）含不同的原子公式p1,…,pn,v是真假赋值。对于i=1，…,n,令viiiipp1Ap如果否则证明：（1）Av=1⇒A1,…,An⊢A（2）Av=0⇒A1,…,An⊢¬A（只考虑A为¬B和B1→B2两种形式）（20分）116.布尔函数122313123fxxxxxxxxx的BDD如图1所示。其中x1是根节点，例点1、例点2为非终节点，0、1为终节点，虚线表示取0实线表示取1。（10分）图1函数f的BDD定义1：当沿着某个BDD的根节点向下搜索时，若每个节点在每条分支上出现的次数最多一次且变量出现的顺序相同，则把BDD称作偏序BDD（OrderedBDD）。定义2：当一个OBDD中不包含同构子图且节点的两条分支不指向同一个节点时，称这个OBDD为约简的偏序BDD（ReducedandOrderedBDD,ROBDD）问题1：对于图1，我们选取变量序为1x、2x、3x，请判断它是否为OBDD。问题2：化简OBDD为ROBDD，可以参照以下步骤：g)合并相同的终节点：合并终节点中相同的节点，使之最多只有两个终节点，取值为0、1；h)去除同构子图：对非终节点u、v，如果满足以下三个条件，则删除其中一个节点，将删除节点的所有入边指向保留节点。Low()/high()分别表示取0取1。()()