第3章确定性推理方法案例.ppt

3.1 推理的基本概念 冲突：已知事实可与知识库中的多条知识匹配 冲突消解 按针对性排序 按事实新鲜性排序 按匹配度排序 按条件个数排序 3.2 自然演绎推理 命题公式及其等价式 （1）双重否定律： （2）交换律： （3）结合律： （4）分配律： （5）摩根定律： ~(P∨Q)?~P∧~Q ~(P∧Q)?~P∨~Q 3.2 自然演绎推理 命题公式及其等价式 （6）吸收律： （7）补余律: （8）连词化归律: （9）量词转换律: （10）量词分配律: P-Q)?(P∧Q) ∨(~Q∧~P) 3.2 自然演绎推理 永真蕴含式 （1）化简式： （2）附加式： （3）析取三段论： （4）假言推理： （5）拒取式： 3.2 自然演绎推理 永真蕴含式 （6）假言三段论： （7）二难推理： （8）全称固化： 其中，y是个体域中的任一个体，依此可消去谓词公式中的全称量词。 （9）存在固化： 其中，y是个体域中某一个可以使 P(y)为真的个体，依此可消去谓词公式中的存在量词。 3.3 谓词公式转换为子句集 文字: 原子公式或其否定 子句: 文字的析取式 谓词: 子句的合取式 3.3 谓词公式转换为子句集 文字: 原子公式或其否定 子句: 文字的析取式 谓词: 子句的合取式 消去连接词“→”和“?” 把否定符号“～”移到每个谓词符号的前面 变量标准化（使不同量词约束的变量有不同的名字） 引入Skolem函数消去存在量词 化为前束形（使所有全称量词在公式最前面） 化为Skolem标准形（子句的合取式） 略去全称量词 断开合取式得到子句集 变量名标准化 3.3 谓词公式转换为子句集 3.4 消解原理 消解原理 (Robinson Theorem) 命题逻辑中的归结原理: 如果C1和C2为真，则C12为真 推论1: C1,C2?S, 则S{C1|C12, C2|C12}不可满足?S不可满足 推论2: C1,C2?S, 则S?{C12}不可满足?S不可满足 C1: P?Q C2: ?P?R C12: Q?R 3.4 消解原理 消解原理 (Robinson Theorem) 谓词逻辑中的归结原理: 如果C1和C2为真，则C12为真 推论1: C1,C2?S, 则S{C1|C12, C2|C12}不可满足?S不可满足 推论2: C1,C2?S, 则S?{C12}不可满足?S不可满足 C1: P(x)?Q(x) C2: ?P(a)?R(y) C12: Q(a)?R(y) 3.5 归结反演 归结反演 (1)将已知前提表示为谓词F (2)将待证明结果表示为谓词Q (3)将谓词公式F??Q化为子句集S (4)应用归结原理对S中的子句进行归结，直至出现空子句，则证明Q为真 推理示例 知识库 天使只说真话不说假话 魔鬼只说假话不说真话 凡人有时候说真话有时候说假话 事实 A, B, C三人分别是天使、魔鬼和凡人 A说“我不是天使”。 B说“我不是魔鬼”。 C说“我不是凡人” 问题：请问谁是天使，谁是魔鬼，谁是凡人？ 3.5 归结反演 归结反演: 可能产生大量不必要的归结式 控制策略 删除无用子句 限制子句的归结范围 案例研究: 故障推理 (USB驱动安装错误) ∨ (USB口损坏) ? (USB口无法使用) (设置了静音) ∨ (音频设备错误) ? (没有声音) (音频设备被禁用) ∨ (声卡驱动安装错误) ∨ (病毒程序破坏了音频服务) ∨ (声卡硬件损坏) ∨ (扬声器硬件损坏) ? (音频设备错误) 人工智能推理领域学术刊物 重要国际期刊 International Journal of Approximate Reasoning, Elsevier (/international-journal-of-approximate-reasoning/) IF: 1.729 Journal of Automated Reasoning, Springer (/journal/10817) IF: 0.567 人工智能推理领域学术刊物 重要国际会议 International Joint Conference on Automated Reasoning (IJCAR), / Internat