离散数学第四章谓词演算的推理理论-归结推理系统共51页文档
- 格式:ppt
- 大小:707.50 KB
- 文档页数:51
谓词演算的推理理论在谓词逻辑中,除了命题逻辑中的推理规则继续有效外,还有以下四条规则。
设前提Г= {A 1,A 2,…,A k }.1. 全称指定规则(全称量词消去规则)US :例1 取个体域为实数域,F(x, y): x>y, P(x)=(∃y) F(x,y), 则(∀x)P(x) ⇒P(z)=(∃y) F(z,y).而不能(∀x) P(x) ⇒P(y)=(∃y) F(y,y).其中x,y 是个体变项符号,c 为任意的个体常量.或 (∀x ) P (x ) ∴ P (y ) (∀x) P (x )∴ P (c )2 . 全称推广规则(全称量词引入规则) UG:P(x)∴ (∀x)P(x)其中x是个体变项符号,且不在前提的任何公式中自由出现.3. 存在指定规则(存在量词消去规则) ES:(∃x)P(x)∴ P(c)1)c是使P(x)为真的特定的个体常量,不是任意的.2)c不在前提中或者先前推导公式中出现或自由出现,换句话说,此c是在该推导之前从未使用过的.4. 存在推广规则(存在量词引入规则) EG:P(c)∴ ( x)P(x)其中x是个体变项符号, c是个体常项符号.谓词逻辑的推理理论由下列要素构成.1. 等价公式2. 蕴含式3. 推理规则:(1) 前提引入规则 (2) 结论引入规则(3) CP推理规则 (4)归谬论(5) US规则 (6) UG规则(7) ES规则 (8) EG规则1)在推导的过程中,可以引用命题演算中的规则P、规则T、规则CP .2)为了在推导过程中消去量词,可以引用规则US和规则ES来消去量词.3)当所要求的结论可能被定量时,此时可引用规则UG和规则EG将其量词加入.4)证明时可采用如命题演算中的直接证明方法和间接证明方法.5)在推导过程中,对消去量词的公式或公式中没含量词的子公式,完全可以引用命题演算中的基本等价公式和基本蕴涵公式.6)在推导过程中,对含有量词的公式可以引用谓词中的基本等价公式和基本蕴涵公式.7)在推导过程中,如既要使用规则US又要使用规则ES消去公式中的量词(只要有可能,我们总是先使用规则ES,再使用规则US)。