谓词逻辑合式公式及解释
标签:
杂谈 |
分类: 系统分析师 |
重点:(1) 掌握合式公式的概念,
(2) 掌握量词的辖域,约束变项,自由变项的概念,
(3) 掌握逻辑有效式,矛盾式,可满足式的概念。
1、字母表。
(1)个体常项: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image003.gif ;
(2)个体变项: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image004.gif ;
(3)函数符号: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image005.gif ;
(4)谓词符号: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image006.gif ;
(5)量词符号: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image007.gif ;
(6)联结词符: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image008.gif ;
(7)括号和逗号:( ,), , 。
2、项的递归定义。
(1) 个体常项和变项是项。
(2) 若 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image009.gif 是任意 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image010.gif 元函数, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image011.gif 是项,则 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image012.gif 是项。
(3) 只有有限次地使用(1)、(2)生成的符号串才是项。
其中 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image013.gif 是字母表中没有的符号,这里表示任意函数。
例如: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image014.gif
http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image015.gif 等都是项。
3、原子公式。
设 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image016.gif 是任意的 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image010.gif 元谓词, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image011.gif 是项,则称 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image017.gif 为原子公式。
4、合式公式的递归定义。
(1) 原子公式是合式公式;
(2) 若 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image018.gif 是合式公式,则 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image019.gif 也是合式公式;
(3) 若 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image020.gif 是合式公式,则 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image021.gif 也是合式公式;
(4) 若 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image018.gif 是合式公式,则 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image022.gif 也是合式公式;
(5) 只有有限次地应用(1)-(4)构成的符号串才是合式公式(也称谓词公式),简称公式。
5、约束出现,自由出现。
在合式公式 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image022.gif 中,称 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 为指导变项,称 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image018.gif 为相应量词的辖域,在辖域中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 的所有出项称为约束出现(即 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 受相应量词指导变项的约束), http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image018.gif 中不是约束出现的其它变项的出现称为自由出现。 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image024.gif
例1、指出下列各合式公式中的指导变项,量词的辖域,个体变项的自由出现和约束出现。
(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image025.gif
解: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image026.gif 中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image027.gif 为指导变项, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image028.gif 的辖域为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image029.gif ,其中 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image027.gif 是约束出现, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 是自由出现, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image025.gif 中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 是指导变项, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image030.gif 的辖域为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image031.gif , http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image032.gif 都是约束出现。
(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image033.gif
解: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image034.gif 中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 为指导变项, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image028.gif 的辖域为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image035.gif , http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 是约束出现的, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image036.gif 中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image032.gif 都是自由出现的,因此,在整个公式中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 是约束出现,又是自由出现, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image027.gif 是自由出现。
(3) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image037.gif
解:在 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image038.gif 中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image032.gif 为指导变项,量词的辖域为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image039.gif , http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image032.gif 约束出现, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image040.gif 自由出现,在 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image041.gif 中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 为指导变项, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image028.gif 的辖域为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image029.gif , http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 约束出现, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image027.gif 自由出现,在整个公式中, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image023.gif 是约束出现, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image027.gif 是约束出现,又是自由出现, http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image040.gif 是自由出现。
闭式(封闭的合式公式)——无自由出现的个体变项的合式公式。
换名规则——将量词辖域中的约束变项及对应的指导变项同时更换成公式中未出现的变项,公式的其余部分不变。
例如: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image025.gif 换成 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image042.gif
代替规则——将公式中的自由变项(所有出现)更换成公式中未出现的变项。
例如: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image037.gif
换成 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image043.gif
对公式中各种变项(个体变项,函数变项,谓词变项),指定特殊的常项去代替,就构成了公式的一个解释。
1、解释 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image044.gif 由以下4部分组成:
(1) 非空个体域 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image045.gif ;
(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image045.gif 中一部分特定元素;
(3) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image045.gif 上一些特定的函数;
(4) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image045.gif 上一些特定的谓词。
例2、给定解释 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image046.gif 如下:
1) 个体域为自然数集合 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image047.gif
2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image047.gif 中特定元素 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image048.gif
3) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image047.gif 上特定函数 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image049.gif
4) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image047.gif 上特定谓词 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image050.gif 为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image051.gif 。
在解释 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image046.gif 下,下面哪些公式为真?哪些公式为假?
(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image052.gif ;
(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image053.gif ;
(3) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image054.gif ;
(4) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image055.gif ;
(5) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image056.gif
解:在解释 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image046.gif 下,公式分别化为:
(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image057.gif 真值为0
(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image058.gif 真值为1
(3) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image059.gif 真值为1
(4) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image060.gif 真值为0
(5) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image061.gif 真值不确定(不是命题)
2、逻辑有效式(永真式),矛盾式(永假式),可满足式。
逻辑有效式——在任何解释下都取值为真的合式公式。
矛盾式——在任何解释下都取值为假的合式公式。
可满足式——至少存在一种解释使其取值为真的合式公式。
对命题公式,有多种方法可判断其类型,可是对逻辑公式,却没有一种可行的办法。只有某些特殊的公式可判断。
还有一些公式,可以利用命题公式的结论。
代换实例——设 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image062.gif 是含 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image010.gif 个命题变项 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image063.gif 的命题公式,将 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image010.gif 个谓词 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image064.gif 取代 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image063.gif 所得的谓词公式称为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image062.gif 的代换实例。
例如: http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image065.gif 等都是 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image066.gif 的代换实例。
注意到命题公式中重言式,矛盾式的代换实例在谓词公式中仍是重言式(逻辑有效式),矛盾式。
例3、判断下列公式中哪些是逻辑有效式,哪些是矛盾式。
(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image067.gif ;
(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image068.gif ;
(3) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image069.gif ;
(4) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image070.gif ;
解:(1) 设 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image044.gif 是任意的解释,设其个体域为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image045.gif 。若存在 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image071.gif , http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image072.gif 为假,则 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image073.gif 为假,从而 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image067.gif 为真;若对任意 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image074.gif ,都有 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image035.gif 为真,则 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image075.gif 均为真,所以 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image067.gif 为真。由以上,原公式是逻辑有效的。
(2) 原公式是命题公式 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image076.gif 的代换实例,而且 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image077.gif (重言式),所以原公式是逻辑有效的。
(3) 原公式是命题公式 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image078.gif 的代换实例,而且 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image079.gif (重言式),所以原公式是逻辑有效的。
(4) 原公式是命题公式 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image080.gif 的代换实例,而且 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/22.files/image081.gif (矛盾式),所以原公式是矛盾式。

加载中…