《逻辑学程序设计与prolog》由会员分享，可在线阅读，更多相关《逻辑学程序设计与prolog（52页珍藏版）》请在金锄头文库上搜索。
1、逻辑学程序设计与Prolog,2012年 2月 ,S的可满足性化简,主要思想：根据情况cases分解S的可满足性。 对应于为真的情况； 对应于 为真的情况；因此将S的可满足性化简为：少掉一个命题字母的 和 的问题。一直这样简化下去，生成一个以公式为节点的二叉树，每一层消去一个文字。该树的每一条路径都对应着一个指派。 如果所有路径都已一个包含空子句的句子结束则S是不可以满足的； 否则，要么存在一条无穷路径，要么存在一条路径是以空公式结束。,例子：,如何提高搜索的效率、限制搜索空间判断S的可满足性是NP完全问题一是通过终结无望路径上的搜索二是制定替代路径上的次序,加细消解或精炼消解,T-消解是指父
2、子句均非重言式式的消解。 是在消解下的闭包T 消解的可靠性T消解的完全性：证明基本上同前。忽略重言式,T-消解,令A为一个指派，A-消解是指父子句之中至少有一个在A下为假的消解。（如果所有的父子句在A下都为真，那么消解式也为真。而没有在A下失败的子句，就不能期望得到不可解性。） 是在消解下的闭包。这有称为语义消解。A-消解的完全性：对于任意的A和S，如果SUNSAT，则 。,A-消解,假设我们已经给所有的命题字母编了索引。对于有序消解，我们想通常那样来定义有序消解的闭包 ， 特殊的地方在于当的索引号高于C1和C2中任意命题字母的索引号时，只允许 1 和 2 进行消解；UNSAT 的递归定义：1
3、）如果 ;2) 如果没有命题字母的索引小于出现在S中的p的索引号， ， ， 那么 ;有序消解的完全性：如果S是不可以满足的，则存在S的一个有序消解反驳。,有序消解,定义：C的从S出发的线性消解演绎或证明是指满足C= n+1 以及下列条件的有序对序列, . : （1） 0 以及每个 ，要么是S中的元素，要么是某个ji的 ； （2）每个 +1 (ix,例 3.3 某些人对某些食物过敏,3.1.2 谓词公式定义1 (1) 个体常元和个体变元都是项。 (2) 设f是n元函数符号,若t1,t2,tn是项,则f(t1,t2,tn)是项。 (3) 只有有限次使用(1), (2)得到的符号串才是项。,定义2
4、设P为n元谓词符号，t1,t2,tn为项，则P(t1,t2,tn)称为原子谓词公式，简称原子公式或者原子。从原子谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。下面我们给出谓词公式的严格定义，即谓词公式的生成规则。,紧接于量词之后被量词作用(即说明)的谓词公式称为该量词的辖域。例如： (1) xP(x)。(2) x(H(x)G(x, y)。(3) xA(x)B(x)。 其中(1)中的P(x)为x的辖域, (2)中的H(x)G(x, y)为x的辖域, (3)中的A(x)为x的辖域, 但B(x)并非x的辖域。,量词后的变元如 x, y中的x,y称为量词的指导变元(或作用变元), 而在一个
5、量词的辖域中与该量词的指导变元相同的变元称为约束变元, 其他变元(如果有的话)称为自由变元, 例如(2)中的x为约束变元, 而y为自由变元, (3)中A(x)中的x为约束变元, 但B(x)中的x为自由变元。例如(3),一个变元在一个公式中既可约束出现, 又可自由出现, 但为了避免混淆, 通常通过改名规则, 使得一个公式中一个变元仅以一种形式出现。,约束变元的改名规则如下： (1) 对需改名的变元, 应同时更改该变元在量词及其辖域中的所有出现。 (2) 新变元符号必须是量词辖域内原先没有的, 最好是公式中也未出现过的。例如公式 xP(x)Q(x)可改为 yP(y)Q(x), 但两者的意义相同。
6、在谓词前加上量词, 称作谓词中相应的个体变元被量化, 例如xA(x)中的x被量化, yB(y)中y被量化。如果一个谓词中的所有个体变元都被量化, 则这个谓词就变为一个命题。例如, 设P(x)表示“x是素数”,则 xP(x), xP(x)就都是命题。这样我们就有两种从谓词(即命题函数)得到命题的方法：一种是给谓词中的个体变元代入个体常元, 另一种就是把谓词中的个体变元全部量化。,把上面关于量化的概念也可以推广到谓词公式。于是，我们便可以说，如果一个公式中的所有个体变元都被量化，或者所有变元都是约束变元（或无自由变元），则这个公式就是一个命题。特别地，我们称 xA(x)为全称命题， xA(x)为特
7、称命题。对于这两种命题，当个体域为有限集时（设有n个元素），有下面的等价式：xA(x) A(a1)A(a2)A(an)xA(x) A(a1)A(a2)A(an)这两个式子也可以推广到个体域为可数无限集。,定义4 设A为如下形式的谓词公式： B1B2Bn 其中Bi(i=1,2,n)形如L1L2Lm，Lj(j=1,2,m)为原子公式或其否定，则A称为合取范式。例如：(P(x)Q(y)(乛P(x)Q(y)R(x,y)(乛Q(y)乛R(x,y)就是一个合取范式。,定义5 设A为如下形式的命题公式：B1B2Bn其中Bi(i=1,2,n)形如L1L2Lm，Lj(j=1,2,m)为原子公式或其否定，则A称为
8、析取范式。例如：(P(x)乛Q(y)R(x,y)(乛P(x) Q(y)(乛P(x)R(x,y)就是一个析取范式。,下面我们所关心的是如何证明S的不可满足性。首先给出一些准备知识。谓词的解释：人为地指派给谓词的含义。一个谓词一般可有无穷多种不同的解释，解释既是表示的知识。每种解释由下列基本部分组成： （1）一组基本区域Di，i=1,n （2）每个常量都是某个Di中的一个元素。 （3）每个变量都是在某个Di中的取值。 （4）每个m目函数都是一个映射： Di1 Di2Dim Dim+1（对于j=k，可以有Dij =Dik ） （5）每个m目谓词都是一个映射 Di1 Di2Dim (T, F),我们用
9、wff代表谓词公式，以I代表一种解释。 永真：I，wff（I）=T 可满足：I，wff（I）=T， I为此公式的一个模型 不可满足（永假）：I， wff（I）=F 非永真：I，wff（I）=F I为此公式的一个反模型 完备性： 在谓词演算的范围内，给定一个公理集，又给定一组推导规则，其中每个规则可以把一个永真公式变成为一个永真公式，则此公理集和推导规则集合在一起构成一个演绎系统，由公理集出发，经过推导规则的推演而得到的合式一定是永真的，反之不一定，即永真的公式不一定能从一个演绎系统推导出来，如果在某个确定的范围内，任何永真公式都可有一个演绎系统推导出来，则称此演绎系统对于该范围来说是完备的。,Gdel 给出了有关演绎系统完备性的两个主要结果： 1对于二阶谓词演算，不存在完备的演绎系统 2对于一阶谓词演算，存在着完备的演绎系统 当然命题演算也存在着完备的演绎系统。 可解性（可判定性）：一类问题称为是可解的或可判定的，当且仅当存在一个算法，该算法应用于该类中任一问题时，可在有限步内停止，并在停止时给出正确的解答。否则，称为不可解的。,
