人工智能导论——逻辑推理

比比叨叨

复习起来比想象的慢啊啊啊啊！挺住！一定要好好复习完。

突然想到霸王别姬里的这句话，帆神如是，陈老如是，我也要加油啊！

0. 逻辑推理概述

逻辑推理这章的重要考点必然是归结推理，20分的必考题已经在那了，除此之外还需要对其他推理方法进行掌握，能够应对选择题。

本章中推理的方法可分为如下五种：

自然演绎推理
归结演绎推理
非归结演绎推理
知识图谱
不确定推理

而根据系统的区分，推理又分为以下两类：

经典推理：采用演绎逻辑推理。从已知出发，演绎推理出结论，是从一般到个别。
非经典推理：采用归纳逻辑推理。从个别到一般。如知识图谱。

1. 自然演绎推理和归结演绎推理

区分两者之前，先明确一下定义：

自然演绎推理：从已知为真的事实出发，运用经典逻辑的推理规则推出结论。
归结演绎推理：对要证明为真公式取非，导出矛盾。

综上，归结演绎推理可看作反证法。那归结推理的书面形式要怎么写呢？

首先，归结推理需要经过以下步骤：

#mermaid-svg-6ScF2UuApcTh4gyD .label{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);fill:#333;color:#333}#mermaid-svg-6ScF2UuApcTh4gyD .label text{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .node rect,#mermaid-svg-6ScF2UuApcTh4gyD .node circle,#mermaid-svg-6ScF2UuApcTh4gyD .node ellipse,#mermaid-svg-6ScF2UuApcTh4gyD .node polygon,#mermaid-svg-6ScF2UuApcTh4gyD .node path{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-6ScF2UuApcTh4gyD .node .label{text-align:center;fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .node.clickable{cursor:pointer}#mermaid-svg-6ScF2UuApcTh4gyD .arrowheadPath{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .edgePath .path{stroke:#333;stroke-width:1.5px}#mermaid-svg-6ScF2UuApcTh4gyD .flowchart-link{stroke:#333;fill:none}#mermaid-svg-6ScF2UuApcTh4gyD .edgeLabel{background-color:#e8e8e8;text-align:center}#mermaid-svg-6ScF2UuApcTh4gyD .edgeLabel rect{opacity:0.9}#mermaid-svg-6ScF2UuApcTh4gyD .edgeLabel span{color:#333}#mermaid-svg-6ScF2UuApcTh4gyD .cluster rect{fill:#ffffde;stroke:#aa3;stroke-width:1px}#mermaid-svg-6ScF2UuApcTh4gyD .cluster text{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:12px;background:#ffffde;border:1px solid #aa3;border-radius:2px;pointer-events:none;z-index:100}#mermaid-svg-6ScF2UuApcTh4gyD .actor{stroke:#ccf;fill:#ECECFF}#mermaid-svg-6ScF2UuApcTh4gyD text.actor>tspan{fill:#000;stroke:none}#mermaid-svg-6ScF2UuApcTh4gyD .actor-line{stroke:grey}#mermaid-svg-6ScF2UuApcTh4gyD .messageLine0{stroke-width:1.5;stroke-dasharray:none;stroke:#333}#mermaid-svg-6ScF2UuApcTh4gyD .messageLine1{stroke-width:1.5;stroke-dasharray:2, 2;stroke:#333}#mermaid-svg-6ScF2UuApcTh4gyD #arrowhead path{fill:#333;stroke:#333}#mermaid-svg-6ScF2UuApcTh4gyD .sequenceNumber{fill:#fff}#mermaid-svg-6ScF2UuApcTh4gyD #sequencenumber{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD #crosshead path{fill:#333;stroke:#333}#mermaid-svg-6ScF2UuApcTh4gyD .messageText{fill:#333;stroke:#333}#mermaid-svg-6ScF2UuApcTh4gyD .labelBox{stroke:#ccf;fill:#ECECFF}#mermaid-svg-6ScF2UuApcTh4gyD .labelText,#mermaid-svg-6ScF2UuApcTh4gyD .labelText>tspan{fill:#000;stroke:none}#mermaid-svg-6ScF2UuApcTh4gyD .loopText,#mermaid-svg-6ScF2UuApcTh4gyD .loopText>tspan{fill:#000;stroke:none}#mermaid-svg-6ScF2UuApcTh4gyD .loopLine{stroke-width:2px;stroke-dasharray:2, 2;stroke:#ccf;fill:#ccf}#mermaid-svg-6ScF2UuApcTh4gyD .note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-6ScF2UuApcTh4gyD .noteText,#mermaid-svg-6ScF2UuApcTh4gyD .noteText>tspan{fill:#000;stroke:none}#mermaid-svg-6ScF2UuApcTh4gyD .activation0{fill:#f4f4f4;stroke:#666}#mermaid-svg-6ScF2UuApcTh4gyD .activation1{fill:#f4f4f4;stroke:#666}#mermaid-svg-6ScF2UuApcTh4gyD .activation2{fill:#f4f4f4;stroke:#666}#mermaid-svg-6ScF2UuApcTh4gyD .mermaid-main-font{font-family:"trebuchet ms", verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD .section{stroke:none;opacity:0.2}#mermaid-svg-6ScF2UuApcTh4gyD .section0{fill:rgba(102,102,255,0.49)}#mermaid-svg-6ScF2UuApcTh4gyD .section2{fill:#fff400}#mermaid-svg-6ScF2UuApcTh4gyD .section1,#mermaid-svg-6ScF2UuApcTh4gyD .section3{fill:#fff;opacity:0.2}#mermaid-svg-6ScF2UuApcTh4gyD .sectionTitle0{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .sectionTitle1{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .sectionTitle2{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .sectionTitle3{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .sectionTitle{text-anchor:start;font-size:11px;text-height:14px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD .grid .tick{stroke:#d3d3d3;opacity:0.8;shape-rendering:crispEdges}#mermaid-svg-6ScF2UuApcTh4gyD .grid .tick text{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD .grid path{stroke-width:0}#mermaid-svg-6ScF2UuApcTh4gyD .today{fill:none;stroke:red;stroke-width:2px}#mermaid-svg-6ScF2UuApcTh4gyD .task{stroke-width:2}#mermaid-svg-6ScF2UuApcTh4gyD .taskText{text-anchor:middle;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD .taskText:not([font-size]){font-size:11px}#mermaid-svg-6ScF2UuApcTh4gyD .taskTextOutsideRight{fill:#000;text-anchor:start;font-size:11px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD .taskTextOutsideLeft{fill:#000;text-anchor:end;font-size:11px}#mermaid-svg-6ScF2UuApcTh4gyD .task.clickable{cursor:pointer}#mermaid-svg-6ScF2UuApcTh4gyD .taskText.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-6ScF2UuApcTh4gyD .taskTextOutsideLeft.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-6ScF2UuApcTh4gyD .taskTextOutsideRight.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-6ScF2UuApcTh4gyD .taskText0,#mermaid-svg-6ScF2UuApcTh4gyD .taskText1,#mermaid-svg-6ScF2UuApcTh4gyD .taskText2,#mermaid-svg-6ScF2UuApcTh4gyD .taskText3{fill:#fff}#mermaid-svg-6ScF2UuApcTh4gyD .task0,#mermaid-svg-6ScF2UuApcTh4gyD .task1,#mermaid-svg-6ScF2UuApcTh4gyD .task2,#mermaid-svg-6ScF2UuApcTh4gyD .task3{fill:#8a90dd;stroke:#534fbc}#mermaid-svg-6ScF2UuApcTh4gyD .taskTextOutside0,#mermaid-svg-6ScF2UuApcTh4gyD .taskTextOutside2{fill:#000}#mermaid-svg-6ScF2UuApcTh4gyD .taskTextOutside1,#mermaid-svg-6ScF2UuApcTh4gyD .taskTextOutside3{fill:#000}#mermaid-svg-6ScF2UuApcTh4gyD .active0,#mermaid-svg-6ScF2UuApcTh4gyD .active1,#mermaid-svg-6ScF2UuApcTh4gyD .active2,#mermaid-svg-6ScF2UuApcTh4gyD .active3{fill:#bfc7ff;stroke:#534fbc}#mermaid-svg-6ScF2UuApcTh4gyD .activeText0,#mermaid-svg-6ScF2UuApcTh4gyD .activeText1,#mermaid-svg-6ScF2UuApcTh4gyD .activeText2,#mermaid-svg-6ScF2UuApcTh4gyD .activeText3{fill:#000 !important}#mermaid-svg-6ScF2UuApcTh4gyD .done0,#mermaid-svg-6ScF2UuApcTh4gyD .done1,#mermaid-svg-6ScF2UuApcTh4gyD .done2,#mermaid-svg-6ScF2UuApcTh4gyD .done3{stroke:grey;fill:#d3d3d3;stroke-width:2}#mermaid-svg-6ScF2UuApcTh4gyD .doneText0,#mermaid-svg-6ScF2UuApcTh4gyD .doneText1,#mermaid-svg-6ScF2UuApcTh4gyD .doneText2,#mermaid-svg-6ScF2UuApcTh4gyD .doneText3{fill:#000 !important}#mermaid-svg-6ScF2UuApcTh4gyD .crit0,#mermaid-svg-6ScF2UuApcTh4gyD .crit1,#mermaid-svg-6ScF2UuApcTh4gyD .crit2,#mermaid-svg-6ScF2UuApcTh4gyD .crit3{stroke:#f88;fill:red;stroke-width:2}#mermaid-svg-6ScF2UuApcTh4gyD .activeCrit0,#mermaid-svg-6ScF2UuApcTh4gyD .activeCrit1,#mermaid-svg-6ScF2UuApcTh4gyD .activeCrit2,#mermaid-svg-6ScF2UuApcTh4gyD .activeCrit3{stroke:#f88;fill:#bfc7ff;stroke-width:2}#mermaid-svg-6ScF2UuApcTh4gyD .doneCrit0,#mermaid-svg-6ScF2UuApcTh4gyD .doneCrit1,#mermaid-svg-6ScF2UuApcTh4gyD .doneCrit2,#mermaid-svg-6ScF2UuApcTh4gyD .doneCrit3{stroke:#f88;fill:#d3d3d3;stroke-width:2;cursor:pointer;shape-rendering:crispEdges}#mermaid-svg-6ScF2UuApcTh4gyD .milestone{transform:rotate(45deg) scale(0.8, 0.8)}#mermaid-svg-6ScF2UuApcTh4gyD .milestoneText{font-style:italic}#mermaid-svg-6ScF2UuApcTh4gyD .doneCritText0,#mermaid-svg-6ScF2UuApcTh4gyD .doneCritText1,#mermaid-svg-6ScF2UuApcTh4gyD .doneCritText2,#mermaid-svg-6ScF2UuApcTh4gyD .doneCritText3{fill:#000 !important}#mermaid-svg-6ScF2UuApcTh4gyD .activeCritText0,#mermaid-svg-6ScF2UuApcTh4gyD .activeCritText1,#mermaid-svg-6ScF2UuApcTh4gyD .activeCritText2,#mermaid-svg-6ScF2UuApcTh4gyD .activeCritText3{fill:#000 !important}#mermaid-svg-6ScF2UuApcTh4gyD .titleText{text-anchor:middle;font-size:18px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD g.classGroup text{fill:#9370db;stroke:none;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:10px}#mermaid-svg-6ScF2UuApcTh4gyD g.classGroup text .title{font-weight:bolder}#mermaid-svg-6ScF2UuApcTh4gyD g.clickable{cursor:pointer}#mermaid-svg-6ScF2UuApcTh4gyD g.classGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-6ScF2UuApcTh4gyD g.classGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD .classLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.5}#mermaid-svg-6ScF2UuApcTh4gyD .classLabel .label{fill:#9370db;font-size:10px}#mermaid-svg-6ScF2UuApcTh4gyD .relation{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-6ScF2UuApcTh4gyD .dashed-line{stroke-dasharray:3}#mermaid-svg-6ScF2UuApcTh4gyD #compositionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD #compositionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD #aggregationStart{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD #aggregationEnd{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD #dependencyStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD #dependencyEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD #extensionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD #extensionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD .commit-id,#mermaid-svg-6ScF2UuApcTh4gyD .commit-msg,#mermaid-svg-6ScF2UuApcTh4gyD .branch-label{fill:lightgrey;color:lightgrey;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD .pieTitleText{text-anchor:middle;font-size:25px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD .slice{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD g.stateGroup text{fill:#9370db;stroke:none;font-size:10px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD g.stateGroup text{fill:#9370db;fill:#333;stroke:none;font-size:10px}#mermaid-svg-6ScF2UuApcTh4gyD g.statediagram-cluster .cluster-label text{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD g.stateGroup .state-title{font-weight:bolder;fill:#000}#mermaid-svg-6ScF2UuApcTh4gyD g.stateGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-6ScF2UuApcTh4gyD g.stateGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-6ScF2UuApcTh4gyD .transition{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-6ScF2UuApcTh4gyD .stateGroup .composit{fill:white;border-bottom:1px}#mermaid-svg-6ScF2UuApcTh4gyD .stateGroup .alt-composit{fill:#e0e0e0;border-bottom:1px}#mermaid-svg-6ScF2UuApcTh4gyD .state-note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-6ScF2UuApcTh4gyD .state-note text{fill:black;stroke:none;font-size:10px}#mermaid-svg-6ScF2UuApcTh4gyD .stateLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.7}#mermaid-svg-6ScF2UuApcTh4gyD .edgeLabel text{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .stateLabel text{fill:#000;font-size:10px;font-weight:bold;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-6ScF2UuApcTh4gyD .node circle.state-start{fill:black;stroke:black}#mermaid-svg-6ScF2UuApcTh4gyD .node circle.state-end{fill:black;stroke:white;stroke-width:1.5}#mermaid-svg-6ScF2UuApcTh4gyD #statediagram-barbEnd{fill:#9370db}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-cluster rect{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-cluster rect.outer{rx:5px;ry:5px}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-state .divider{stroke:#9370db}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-state .title-state{rx:5px;ry:5px}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-cluster.statediagram-cluster .inner{fill:white}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-cluster.statediagram-cluster-alt .inner{fill:#e0e0e0}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-cluster .inner{rx:0;ry:0}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-state rect.basic{rx:5px;ry:5px}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-state rect.divider{stroke-dasharray:10,10;fill:#efefef}#mermaid-svg-6ScF2UuApcTh4gyD .note-edge{stroke-dasharray:5}#mermaid-svg-6ScF2UuApcTh4gyD .statediagram-note rect{fill:#fff5ad;stroke:#aa3;stroke-width:1px;rx:0;ry:0}:root{--mermaid-font-family: '"trebuchet ms", verdana, arial';--mermaid-font-family: "Comic Sans MS", "Comic Sans", cursive}#mermaid-svg-6ScF2UuApcTh4gyD .error-icon{fill:#522}#mermaid-svg-6ScF2UuApcTh4gyD .error-text{fill:#522;stroke:#522}#mermaid-svg-6ScF2UuApcTh4gyD .edge-thickness-normal{stroke-width:2px}#mermaid-svg-6ScF2UuApcTh4gyD .edge-thickness-thick{stroke-width:3.5px}#mermaid-svg-6ScF2UuApcTh4gyD .edge-pattern-solid{stroke-dasharray:0}#mermaid-svg-6ScF2UuApcTh4gyD .edge-pattern-dashed{stroke-dasharray:3}#mermaid-svg-6ScF2UuApcTh4gyD .edge-pattern-dotted{stroke-dasharray:2}#mermaid-svg-6ScF2UuApcTh4gyD .marker{fill:#333}#mermaid-svg-6ScF2UuApcTh4gyD .marker.cross{stroke:#333}:root { --mermaid-font-family: "trebuchet ms", verdana, arial;}#mermaid-svg-6ScF2UuApcTh4gyD {color: rgba(0, 0, 0, 0.75);font: ;}

命题改写为合取范式

求子句集

归结推理规则

归结式为空S矛盾

原命题成立

要想完成以上过程，需要考虑很多东西，接下来咱们逐个求解。

1.1 命题、谓词、谓词公式

基础不牢，地动山摇！

命题：描述观点的陈述句
谓词：可以看作描述事物关系的函数
谓词公式：使用谓词描述命题

看下面这个例子相信你就能对应上了！

1.2 合取范式、析取范式、前束范式

合取范式：命题和命题的与
析取范式：命题和命题的或
前束范式：把所有量词提取到前面，消除所有量词

将谓词公式转化为前束范式的形式叫SKOLEM化。
完成SKOLEM化需要掌握一些变化的公式。

~P=>Q 等价于 PVQ
P=>Q 等价于 ~PVQ
~(AVB) 等价于非A且非B

之后，根据量词的作用域将量词提至最前。

1.3 子句集求取

要想求子句集，首先必须得知道啥是子句集。

子句：任何文字的析取式

那么子句集也就是将一个谓词公式化为一个子句集，可以包含多个子句。

了解了这些之后，需要按照步骤将命题化为子句集。

#mermaid-svg-YHst27ua8XqwTt3P .label{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);fill:#333;color:#333}#mermaid-svg-YHst27ua8XqwTt3P .label text{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .node rect,#mermaid-svg-YHst27ua8XqwTt3P .node circle,#mermaid-svg-YHst27ua8XqwTt3P .node ellipse,#mermaid-svg-YHst27ua8XqwTt3P .node polygon,#mermaid-svg-YHst27ua8XqwTt3P .node path{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-YHst27ua8XqwTt3P .node .label{text-align:center;fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .node.clickable{cursor:pointer}#mermaid-svg-YHst27ua8XqwTt3P .arrowheadPath{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .edgePath .path{stroke:#333;stroke-width:1.5px}#mermaid-svg-YHst27ua8XqwTt3P .flowchart-link{stroke:#333;fill:none}#mermaid-svg-YHst27ua8XqwTt3P .edgeLabel{background-color:#e8e8e8;text-align:center}#mermaid-svg-YHst27ua8XqwTt3P .edgeLabel rect{opacity:0.9}#mermaid-svg-YHst27ua8XqwTt3P .edgeLabel span{color:#333}#mermaid-svg-YHst27ua8XqwTt3P .cluster rect{fill:#ffffde;stroke:#aa3;stroke-width:1px}#mermaid-svg-YHst27ua8XqwTt3P .cluster text{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:12px;background:#ffffde;border:1px solid #aa3;border-radius:2px;pointer-events:none;z-index:100}#mermaid-svg-YHst27ua8XqwTt3P .actor{stroke:#ccf;fill:#ECECFF}#mermaid-svg-YHst27ua8XqwTt3P text.actor>tspan{fill:#000;stroke:none}#mermaid-svg-YHst27ua8XqwTt3P .actor-line{stroke:grey}#mermaid-svg-YHst27ua8XqwTt3P .messageLine0{stroke-width:1.5;stroke-dasharray:none;stroke:#333}#mermaid-svg-YHst27ua8XqwTt3P .messageLine1{stroke-width:1.5;stroke-dasharray:2, 2;stroke:#333}#mermaid-svg-YHst27ua8XqwTt3P #arrowhead path{fill:#333;stroke:#333}#mermaid-svg-YHst27ua8XqwTt3P .sequenceNumber{fill:#fff}#mermaid-svg-YHst27ua8XqwTt3P #sequencenumber{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P #crosshead path{fill:#333;stroke:#333}#mermaid-svg-YHst27ua8XqwTt3P .messageText{fill:#333;stroke:#333}#mermaid-svg-YHst27ua8XqwTt3P .labelBox{stroke:#ccf;fill:#ECECFF}#mermaid-svg-YHst27ua8XqwTt3P .labelText,#mermaid-svg-YHst27ua8XqwTt3P .labelText>tspan{fill:#000;stroke:none}#mermaid-svg-YHst27ua8XqwTt3P .loopText,#mermaid-svg-YHst27ua8XqwTt3P .loopText>tspan{fill:#000;stroke:none}#mermaid-svg-YHst27ua8XqwTt3P .loopLine{stroke-width:2px;stroke-dasharray:2, 2;stroke:#ccf;fill:#ccf}#mermaid-svg-YHst27ua8XqwTt3P .note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-YHst27ua8XqwTt3P .noteText,#mermaid-svg-YHst27ua8XqwTt3P .noteText>tspan{fill:#000;stroke:none}#mermaid-svg-YHst27ua8XqwTt3P .activation0{fill:#f4f4f4;stroke:#666}#mermaid-svg-YHst27ua8XqwTt3P .activation1{fill:#f4f4f4;stroke:#666}#mermaid-svg-YHst27ua8XqwTt3P .activation2{fill:#f4f4f4;stroke:#666}#mermaid-svg-YHst27ua8XqwTt3P .mermaid-main-font{font-family:"trebuchet ms", verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P .section{stroke:none;opacity:0.2}#mermaid-svg-YHst27ua8XqwTt3P .section0{fill:rgba(102,102,255,0.49)}#mermaid-svg-YHst27ua8XqwTt3P .section2{fill:#fff400}#mermaid-svg-YHst27ua8XqwTt3P .section1,#mermaid-svg-YHst27ua8XqwTt3P .section3{fill:#fff;opacity:0.2}#mermaid-svg-YHst27ua8XqwTt3P .sectionTitle0{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .sectionTitle1{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .sectionTitle2{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .sectionTitle3{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .sectionTitle{text-anchor:start;font-size:11px;text-height:14px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P .grid .tick{stroke:#d3d3d3;opacity:0.8;shape-rendering:crispEdges}#mermaid-svg-YHst27ua8XqwTt3P .grid .tick text{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P .grid path{stroke-width:0}#mermaid-svg-YHst27ua8XqwTt3P .today{fill:none;stroke:red;stroke-width:2px}#mermaid-svg-YHst27ua8XqwTt3P .task{stroke-width:2}#mermaid-svg-YHst27ua8XqwTt3P .taskText{text-anchor:middle;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P .taskText:not([font-size]){font-size:11px}#mermaid-svg-YHst27ua8XqwTt3P .taskTextOutsideRight{fill:#000;text-anchor:start;font-size:11px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P .taskTextOutsideLeft{fill:#000;text-anchor:end;font-size:11px}#mermaid-svg-YHst27ua8XqwTt3P .task.clickable{cursor:pointer}#mermaid-svg-YHst27ua8XqwTt3P .taskText.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-YHst27ua8XqwTt3P .taskTextOutsideLeft.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-YHst27ua8XqwTt3P .taskTextOutsideRight.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-YHst27ua8XqwTt3P .taskText0,#mermaid-svg-YHst27ua8XqwTt3P .taskText1,#mermaid-svg-YHst27ua8XqwTt3P .taskText2,#mermaid-svg-YHst27ua8XqwTt3P .taskText3{fill:#fff}#mermaid-svg-YHst27ua8XqwTt3P .task0,#mermaid-svg-YHst27ua8XqwTt3P .task1,#mermaid-svg-YHst27ua8XqwTt3P .task2,#mermaid-svg-YHst27ua8XqwTt3P .task3{fill:#8a90dd;stroke:#534fbc}#mermaid-svg-YHst27ua8XqwTt3P .taskTextOutside0,#mermaid-svg-YHst27ua8XqwTt3P .taskTextOutside2{fill:#000}#mermaid-svg-YHst27ua8XqwTt3P .taskTextOutside1,#mermaid-svg-YHst27ua8XqwTt3P .taskTextOutside3{fill:#000}#mermaid-svg-YHst27ua8XqwTt3P .active0,#mermaid-svg-YHst27ua8XqwTt3P .active1,#mermaid-svg-YHst27ua8XqwTt3P .active2,#mermaid-svg-YHst27ua8XqwTt3P .active3{fill:#bfc7ff;stroke:#534fbc}#mermaid-svg-YHst27ua8XqwTt3P .activeText0,#mermaid-svg-YHst27ua8XqwTt3P .activeText1,#mermaid-svg-YHst27ua8XqwTt3P .activeText2,#mermaid-svg-YHst27ua8XqwTt3P .activeText3{fill:#000 !important}#mermaid-svg-YHst27ua8XqwTt3P .done0,#mermaid-svg-YHst27ua8XqwTt3P .done1,#mermaid-svg-YHst27ua8XqwTt3P .done2,#mermaid-svg-YHst27ua8XqwTt3P .done3{stroke:grey;fill:#d3d3d3;stroke-width:2}#mermaid-svg-YHst27ua8XqwTt3P .doneText0,#mermaid-svg-YHst27ua8XqwTt3P .doneText1,#mermaid-svg-YHst27ua8XqwTt3P .doneText2,#mermaid-svg-YHst27ua8XqwTt3P .doneText3{fill:#000 !important}#mermaid-svg-YHst27ua8XqwTt3P .crit0,#mermaid-svg-YHst27ua8XqwTt3P .crit1,#mermaid-svg-YHst27ua8XqwTt3P .crit2,#mermaid-svg-YHst27ua8XqwTt3P .crit3{stroke:#f88;fill:red;stroke-width:2}#mermaid-svg-YHst27ua8XqwTt3P .activeCrit0,#mermaid-svg-YHst27ua8XqwTt3P .activeCrit1,#mermaid-svg-YHst27ua8XqwTt3P .activeCrit2,#mermaid-svg-YHst27ua8XqwTt3P .activeCrit3{stroke:#f88;fill:#bfc7ff;stroke-width:2}#mermaid-svg-YHst27ua8XqwTt3P .doneCrit0,#mermaid-svg-YHst27ua8XqwTt3P .doneCrit1,#mermaid-svg-YHst27ua8XqwTt3P .doneCrit2,#mermaid-svg-YHst27ua8XqwTt3P .doneCrit3{stroke:#f88;fill:#d3d3d3;stroke-width:2;cursor:pointer;shape-rendering:crispEdges}#mermaid-svg-YHst27ua8XqwTt3P .milestone{transform:rotate(45deg) scale(0.8, 0.8)}#mermaid-svg-YHst27ua8XqwTt3P .milestoneText{font-style:italic}#mermaid-svg-YHst27ua8XqwTt3P .doneCritText0,#mermaid-svg-YHst27ua8XqwTt3P .doneCritText1,#mermaid-svg-YHst27ua8XqwTt3P .doneCritText2,#mermaid-svg-YHst27ua8XqwTt3P .doneCritText3{fill:#000 !important}#mermaid-svg-YHst27ua8XqwTt3P .activeCritText0,#mermaid-svg-YHst27ua8XqwTt3P .activeCritText1,#mermaid-svg-YHst27ua8XqwTt3P .activeCritText2,#mermaid-svg-YHst27ua8XqwTt3P .activeCritText3{fill:#000 !important}#mermaid-svg-YHst27ua8XqwTt3P .titleText{text-anchor:middle;font-size:18px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P g.classGroup text{fill:#9370db;stroke:none;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:10px}#mermaid-svg-YHst27ua8XqwTt3P g.classGroup text .title{font-weight:bolder}#mermaid-svg-YHst27ua8XqwTt3P g.clickable{cursor:pointer}#mermaid-svg-YHst27ua8XqwTt3P g.classGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-YHst27ua8XqwTt3P g.classGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P .classLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.5}#mermaid-svg-YHst27ua8XqwTt3P .classLabel .label{fill:#9370db;font-size:10px}#mermaid-svg-YHst27ua8XqwTt3P .relation{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-YHst27ua8XqwTt3P .dashed-line{stroke-dasharray:3}#mermaid-svg-YHst27ua8XqwTt3P #compositionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P #compositionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P #aggregationStart{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P #aggregationEnd{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P #dependencyStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P #dependencyEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P #extensionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P #extensionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P .commit-id,#mermaid-svg-YHst27ua8XqwTt3P .commit-msg,#mermaid-svg-YHst27ua8XqwTt3P .branch-label{fill:lightgrey;color:lightgrey;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P .pieTitleText{text-anchor:middle;font-size:25px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P .slice{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P g.stateGroup text{fill:#9370db;stroke:none;font-size:10px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P g.stateGroup text{fill:#9370db;fill:#333;stroke:none;font-size:10px}#mermaid-svg-YHst27ua8XqwTt3P g.statediagram-cluster .cluster-label text{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P g.stateGroup .state-title{font-weight:bolder;fill:#000}#mermaid-svg-YHst27ua8XqwTt3P g.stateGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-YHst27ua8XqwTt3P g.stateGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-YHst27ua8XqwTt3P .transition{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-YHst27ua8XqwTt3P .stateGroup .composit{fill:white;border-bottom:1px}#mermaid-svg-YHst27ua8XqwTt3P .stateGroup .alt-composit{fill:#e0e0e0;border-bottom:1px}#mermaid-svg-YHst27ua8XqwTt3P .state-note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-YHst27ua8XqwTt3P .state-note text{fill:black;stroke:none;font-size:10px}#mermaid-svg-YHst27ua8XqwTt3P .stateLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.7}#mermaid-svg-YHst27ua8XqwTt3P .edgeLabel text{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .stateLabel text{fill:#000;font-size:10px;font-weight:bold;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-YHst27ua8XqwTt3P .node circle.state-start{fill:black;stroke:black}#mermaid-svg-YHst27ua8XqwTt3P .node circle.state-end{fill:black;stroke:white;stroke-width:1.5}#mermaid-svg-YHst27ua8XqwTt3P #statediagram-barbEnd{fill:#9370db}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-cluster rect{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-cluster rect.outer{rx:5px;ry:5px}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-state .divider{stroke:#9370db}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-state .title-state{rx:5px;ry:5px}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-cluster.statediagram-cluster .inner{fill:white}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-cluster.statediagram-cluster-alt .inner{fill:#e0e0e0}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-cluster .inner{rx:0;ry:0}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-state rect.basic{rx:5px;ry:5px}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-state rect.divider{stroke-dasharray:10,10;fill:#efefef}#mermaid-svg-YHst27ua8XqwTt3P .note-edge{stroke-dasharray:5}#mermaid-svg-YHst27ua8XqwTt3P .statediagram-note rect{fill:#fff5ad;stroke:#aa3;stroke-width:1px;rx:0;ry:0}:root{--mermaid-font-family: '"trebuchet ms", verdana, arial';--mermaid-font-family: "Comic Sans MS", "Comic Sans", cursive}#mermaid-svg-YHst27ua8XqwTt3P .error-icon{fill:#522}#mermaid-svg-YHst27ua8XqwTt3P .error-text{fill:#522;stroke:#522}#mermaid-svg-YHst27ua8XqwTt3P .edge-thickness-normal{stroke-width:2px}#mermaid-svg-YHst27ua8XqwTt3P .edge-thickness-thick{stroke-width:3.5px}#mermaid-svg-YHst27ua8XqwTt3P .edge-pattern-solid{stroke-dasharray:0}#mermaid-svg-YHst27ua8XqwTt3P .edge-pattern-dashed{stroke-dasharray:3}#mermaid-svg-YHst27ua8XqwTt3P .edge-pattern-dotted{stroke-dasharray:2}#mermaid-svg-YHst27ua8XqwTt3P .marker{fill:#333}#mermaid-svg-YHst27ua8XqwTt3P .marker.cross{stroke:#333}:root { --mermaid-font-family: "trebuchet ms", verdana, arial;}#mermaid-svg-YHst27ua8XqwTt3P {color: rgba(0, 0, 0, 0.75);font: ;}

消去蕴含符

移动否定符号到最近谓词

变量标准化

消去存在量词

化为前束范式

化为合取范式

消去全称量词

消去合取

变量名

在化子句集的时候，并不需要完全按照步骤来做，只要能得到析取式的集合就是正确的。

子句与子句间合取，子句内部析取

消去全称量词：直接去掉即可
消去存在量词：代入

1.4 消解推理规则

此步骤需要利用规则消去子句。得到新子句为消解式。目的是推出为空（NIL）的消解式，并得到矛盾。

除了能通过消解推理规则证明外，也能通过消解树反演求解。

在归结过程中，使用如下策略，可以使得归结效率更高。：

语义归结：将S分成两部分，约定每部分内不允许归结，可以得到高效的归结策略。
支持集策略：每次归结只选取不同时属于S-T的子句间进行归结。
线性归结：取每次得到的消解式进行归结
单元归结
输入归结：每次归结必有一个S的子句

2. 非归结演绎推理

包括如下几种：

基于规则演绎推理：if-then推理
自然演绎推理

这里还有很多乱七八糟的，先不看，重点不在这里。

3. 知识图谱

什么是知识图谱？

知识图谱：包含多种关系的有向图。

利用知识图谱可以进行推理，其中一阶归纳推理需要掌握。

3.1 FOIL（一阶归纳推理）

FOIL：通过序贯覆盖实现规则推理。
输入：目标谓词p、p的正例、反例、背景知识
输出：p的推理规则

FOIL的算法流程如下:

#mermaid-svg-f6VSFcICnzsa4p7t .label{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);fill:#333;color:#333}#mermaid-svg-f6VSFcICnzsa4p7t .label text{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .node rect,#mermaid-svg-f6VSFcICnzsa4p7t .node circle,#mermaid-svg-f6VSFcICnzsa4p7t .node ellipse,#mermaid-svg-f6VSFcICnzsa4p7t .node polygon,#mermaid-svg-f6VSFcICnzsa4p7t .node path{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-f6VSFcICnzsa4p7t .node .label{text-align:center;fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .node.clickable{cursor:pointer}#mermaid-svg-f6VSFcICnzsa4p7t .arrowheadPath{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .edgePath .path{stroke:#333;stroke-width:1.5px}#mermaid-svg-f6VSFcICnzsa4p7t .flowchart-link{stroke:#333;fill:none}#mermaid-svg-f6VSFcICnzsa4p7t .edgeLabel{background-color:#e8e8e8;text-align:center}#mermaid-svg-f6VSFcICnzsa4p7t .edgeLabel rect{opacity:0.9}#mermaid-svg-f6VSFcICnzsa4p7t .edgeLabel span{color:#333}#mermaid-svg-f6VSFcICnzsa4p7t .cluster rect{fill:#ffffde;stroke:#aa3;stroke-width:1px}#mermaid-svg-f6VSFcICnzsa4p7t .cluster text{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:12px;background:#ffffde;border:1px solid #aa3;border-radius:2px;pointer-events:none;z-index:100}#mermaid-svg-f6VSFcICnzsa4p7t .actor{stroke:#ccf;fill:#ECECFF}#mermaid-svg-f6VSFcICnzsa4p7t text.actor>tspan{fill:#000;stroke:none}#mermaid-svg-f6VSFcICnzsa4p7t .actor-line{stroke:grey}#mermaid-svg-f6VSFcICnzsa4p7t .messageLine0{stroke-width:1.5;stroke-dasharray:none;stroke:#333}#mermaid-svg-f6VSFcICnzsa4p7t .messageLine1{stroke-width:1.5;stroke-dasharray:2, 2;stroke:#333}#mermaid-svg-f6VSFcICnzsa4p7t #arrowhead path{fill:#333;stroke:#333}#mermaid-svg-f6VSFcICnzsa4p7t .sequenceNumber{fill:#fff}#mermaid-svg-f6VSFcICnzsa4p7t #sequencenumber{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t #crosshead path{fill:#333;stroke:#333}#mermaid-svg-f6VSFcICnzsa4p7t .messageText{fill:#333;stroke:#333}#mermaid-svg-f6VSFcICnzsa4p7t .labelBox{stroke:#ccf;fill:#ECECFF}#mermaid-svg-f6VSFcICnzsa4p7t .labelText,#mermaid-svg-f6VSFcICnzsa4p7t .labelText>tspan{fill:#000;stroke:none}#mermaid-svg-f6VSFcICnzsa4p7t .loopText,#mermaid-svg-f6VSFcICnzsa4p7t .loopText>tspan{fill:#000;stroke:none}#mermaid-svg-f6VSFcICnzsa4p7t .loopLine{stroke-width:2px;stroke-dasharray:2, 2;stroke:#ccf;fill:#ccf}#mermaid-svg-f6VSFcICnzsa4p7t .note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-f6VSFcICnzsa4p7t .noteText,#mermaid-svg-f6VSFcICnzsa4p7t .noteText>tspan{fill:#000;stroke:none}#mermaid-svg-f6VSFcICnzsa4p7t .activation0{fill:#f4f4f4;stroke:#666}#mermaid-svg-f6VSFcICnzsa4p7t .activation1{fill:#f4f4f4;stroke:#666}#mermaid-svg-f6VSFcICnzsa4p7t .activation2{fill:#f4f4f4;stroke:#666}#mermaid-svg-f6VSFcICnzsa4p7t .mermaid-main-font{font-family:"trebuchet ms", verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t .section{stroke:none;opacity:0.2}#mermaid-svg-f6VSFcICnzsa4p7t .section0{fill:rgba(102,102,255,0.49)}#mermaid-svg-f6VSFcICnzsa4p7t .section2{fill:#fff400}#mermaid-svg-f6VSFcICnzsa4p7t .section1,#mermaid-svg-f6VSFcICnzsa4p7t .section3{fill:#fff;opacity:0.2}#mermaid-svg-f6VSFcICnzsa4p7t .sectionTitle0{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .sectionTitle1{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .sectionTitle2{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .sectionTitle3{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .sectionTitle{text-anchor:start;font-size:11px;text-height:14px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t .grid .tick{stroke:#d3d3d3;opacity:0.8;shape-rendering:crispEdges}#mermaid-svg-f6VSFcICnzsa4p7t .grid .tick text{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t .grid path{stroke-width:0}#mermaid-svg-f6VSFcICnzsa4p7t .today{fill:none;stroke:red;stroke-width:2px}#mermaid-svg-f6VSFcICnzsa4p7t .task{stroke-width:2}#mermaid-svg-f6VSFcICnzsa4p7t .taskText{text-anchor:middle;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t .taskText:not([font-size]){font-size:11px}#mermaid-svg-f6VSFcICnzsa4p7t .taskTextOutsideRight{fill:#000;text-anchor:start;font-size:11px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t .taskTextOutsideLeft{fill:#000;text-anchor:end;font-size:11px}#mermaid-svg-f6VSFcICnzsa4p7t .task.clickable{cursor:pointer}#mermaid-svg-f6VSFcICnzsa4p7t .taskText.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-f6VSFcICnzsa4p7t .taskTextOutsideLeft.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-f6VSFcICnzsa4p7t .taskTextOutsideRight.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-f6VSFcICnzsa4p7t .taskText0,#mermaid-svg-f6VSFcICnzsa4p7t .taskText1,#mermaid-svg-f6VSFcICnzsa4p7t .taskText2,#mermaid-svg-f6VSFcICnzsa4p7t .taskText3{fill:#fff}#mermaid-svg-f6VSFcICnzsa4p7t .task0,#mermaid-svg-f6VSFcICnzsa4p7t .task1,#mermaid-svg-f6VSFcICnzsa4p7t .task2,#mermaid-svg-f6VSFcICnzsa4p7t .task3{fill:#8a90dd;stroke:#534fbc}#mermaid-svg-f6VSFcICnzsa4p7t .taskTextOutside0,#mermaid-svg-f6VSFcICnzsa4p7t .taskTextOutside2{fill:#000}#mermaid-svg-f6VSFcICnzsa4p7t .taskTextOutside1,#mermaid-svg-f6VSFcICnzsa4p7t .taskTextOutside3{fill:#000}#mermaid-svg-f6VSFcICnzsa4p7t .active0,#mermaid-svg-f6VSFcICnzsa4p7t .active1,#mermaid-svg-f6VSFcICnzsa4p7t .active2,#mermaid-svg-f6VSFcICnzsa4p7t .active3{fill:#bfc7ff;stroke:#534fbc}#mermaid-svg-f6VSFcICnzsa4p7t .activeText0,#mermaid-svg-f6VSFcICnzsa4p7t .activeText1,#mermaid-svg-f6VSFcICnzsa4p7t .activeText2,#mermaid-svg-f6VSFcICnzsa4p7t .activeText3{fill:#000 !important}#mermaid-svg-f6VSFcICnzsa4p7t .done0,#mermaid-svg-f6VSFcICnzsa4p7t .done1,#mermaid-svg-f6VSFcICnzsa4p7t .done2,#mermaid-svg-f6VSFcICnzsa4p7t .done3{stroke:grey;fill:#d3d3d3;stroke-width:2}#mermaid-svg-f6VSFcICnzsa4p7t .doneText0,#mermaid-svg-f6VSFcICnzsa4p7t .doneText1,#mermaid-svg-f6VSFcICnzsa4p7t .doneText2,#mermaid-svg-f6VSFcICnzsa4p7t .doneText3{fill:#000 !important}#mermaid-svg-f6VSFcICnzsa4p7t .crit0,#mermaid-svg-f6VSFcICnzsa4p7t .crit1,#mermaid-svg-f6VSFcICnzsa4p7t .crit2,#mermaid-svg-f6VSFcICnzsa4p7t .crit3{stroke:#f88;fill:red;stroke-width:2}#mermaid-svg-f6VSFcICnzsa4p7t .activeCrit0,#mermaid-svg-f6VSFcICnzsa4p7t .activeCrit1,#mermaid-svg-f6VSFcICnzsa4p7t .activeCrit2,#mermaid-svg-f6VSFcICnzsa4p7t .activeCrit3{stroke:#f88;fill:#bfc7ff;stroke-width:2}#mermaid-svg-f6VSFcICnzsa4p7t .doneCrit0,#mermaid-svg-f6VSFcICnzsa4p7t .doneCrit1,#mermaid-svg-f6VSFcICnzsa4p7t .doneCrit2,#mermaid-svg-f6VSFcICnzsa4p7t .doneCrit3{stroke:#f88;fill:#d3d3d3;stroke-width:2;cursor:pointer;shape-rendering:crispEdges}#mermaid-svg-f6VSFcICnzsa4p7t .milestone{transform:rotate(45deg) scale(0.8, 0.8)}#mermaid-svg-f6VSFcICnzsa4p7t .milestoneText{font-style:italic}#mermaid-svg-f6VSFcICnzsa4p7t .doneCritText0,#mermaid-svg-f6VSFcICnzsa4p7t .doneCritText1,#mermaid-svg-f6VSFcICnzsa4p7t .doneCritText2,#mermaid-svg-f6VSFcICnzsa4p7t .doneCritText3{fill:#000 !important}#mermaid-svg-f6VSFcICnzsa4p7t .activeCritText0,#mermaid-svg-f6VSFcICnzsa4p7t .activeCritText1,#mermaid-svg-f6VSFcICnzsa4p7t .activeCritText2,#mermaid-svg-f6VSFcICnzsa4p7t .activeCritText3{fill:#000 !important}#mermaid-svg-f6VSFcICnzsa4p7t .titleText{text-anchor:middle;font-size:18px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t g.classGroup text{fill:#9370db;stroke:none;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:10px}#mermaid-svg-f6VSFcICnzsa4p7t g.classGroup text .title{font-weight:bolder}#mermaid-svg-f6VSFcICnzsa4p7t g.clickable{cursor:pointer}#mermaid-svg-f6VSFcICnzsa4p7t g.classGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-f6VSFcICnzsa4p7t g.classGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t .classLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.5}#mermaid-svg-f6VSFcICnzsa4p7t .classLabel .label{fill:#9370db;font-size:10px}#mermaid-svg-f6VSFcICnzsa4p7t .relation{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-f6VSFcICnzsa4p7t .dashed-line{stroke-dasharray:3}#mermaid-svg-f6VSFcICnzsa4p7t #compositionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t #compositionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t #aggregationStart{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t #aggregationEnd{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t #dependencyStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t #dependencyEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t #extensionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t #extensionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t .commit-id,#mermaid-svg-f6VSFcICnzsa4p7t .commit-msg,#mermaid-svg-f6VSFcICnzsa4p7t .branch-label{fill:lightgrey;color:lightgrey;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t .pieTitleText{text-anchor:middle;font-size:25px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t .slice{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t g.stateGroup text{fill:#9370db;stroke:none;font-size:10px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t g.stateGroup text{fill:#9370db;fill:#333;stroke:none;font-size:10px}#mermaid-svg-f6VSFcICnzsa4p7t g.statediagram-cluster .cluster-label text{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t g.stateGroup .state-title{font-weight:bolder;fill:#000}#mermaid-svg-f6VSFcICnzsa4p7t g.stateGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-f6VSFcICnzsa4p7t g.stateGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-f6VSFcICnzsa4p7t .transition{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-f6VSFcICnzsa4p7t .stateGroup .composit{fill:white;border-bottom:1px}#mermaid-svg-f6VSFcICnzsa4p7t .stateGroup .alt-composit{fill:#e0e0e0;border-bottom:1px}#mermaid-svg-f6VSFcICnzsa4p7t .state-note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-f6VSFcICnzsa4p7t .state-note text{fill:black;stroke:none;font-size:10px}#mermaid-svg-f6VSFcICnzsa4p7t .stateLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.7}#mermaid-svg-f6VSFcICnzsa4p7t .edgeLabel text{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .stateLabel text{fill:#000;font-size:10px;font-weight:bold;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-f6VSFcICnzsa4p7t .node circle.state-start{fill:black;stroke:black}#mermaid-svg-f6VSFcICnzsa4p7t .node circle.state-end{fill:black;stroke:white;stroke-width:1.5}#mermaid-svg-f6VSFcICnzsa4p7t #statediagram-barbEnd{fill:#9370db}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-cluster rect{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-cluster rect.outer{rx:5px;ry:5px}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-state .divider{stroke:#9370db}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-state .title-state{rx:5px;ry:5px}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-cluster.statediagram-cluster .inner{fill:white}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-cluster.statediagram-cluster-alt .inner{fill:#e0e0e0}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-cluster .inner{rx:0;ry:0}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-state rect.basic{rx:5px;ry:5px}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-state rect.divider{stroke-dasharray:10,10;fill:#efefef}#mermaid-svg-f6VSFcICnzsa4p7t .note-edge{stroke-dasharray:5}#mermaid-svg-f6VSFcICnzsa4p7t .statediagram-note rect{fill:#fff5ad;stroke:#aa3;stroke-width:1px;rx:0;ry:0}:root{--mermaid-font-family: '"trebuchet ms", verdana, arial';--mermaid-font-family: "Comic Sans MS", "Comic Sans", cursive}#mermaid-svg-f6VSFcICnzsa4p7t .error-icon{fill:#522}#mermaid-svg-f6VSFcICnzsa4p7t .error-text{fill:#522;stroke:#522}#mermaid-svg-f6VSFcICnzsa4p7t .edge-thickness-normal{stroke-width:2px}#mermaid-svg-f6VSFcICnzsa4p7t .edge-thickness-thick{stroke-width:3.5px}#mermaid-svg-f6VSFcICnzsa4p7t .edge-pattern-solid{stroke-dasharray:0}#mermaid-svg-f6VSFcICnzsa4p7t .edge-pattern-dashed{stroke-dasharray:3}#mermaid-svg-f6VSFcICnzsa4p7t .edge-pattern-dotted{stroke-dasharray:2}#mermaid-svg-f6VSFcICnzsa4p7t .marker{fill:#333}#mermaid-svg-f6VSFcICnzsa4p7t .marker.cross{stroke:#333}:root { --mermaid-font-family: "trebuchet ms", verdana, arial;}#mermaid-svg-f6VSFcICnzsa4p7t {color: rgba(0, 0, 0, 0.75);font: ;}

目标谓词作为结论

其他谓词作为约束加入推理规则

计算所得推理规则信息增益值

选取最优前提约束生成新规则

去掉与规则不符样例

不覆盖任何反例

其中，信息增益值计算方法如下:

可见，信息增益值与增加约束谓词前后的正例、反例数量均有关系。

3.2 路径排序

路径排序：路径排序是有监督学习，将实体之间的关联路径作为特征，学习目标关系的分类器，分类器可用于推理两实体间是否存在目标关系。

4. 题目解析

问题1

此题选D，编码成某种数据结构

问题2

此题选D，记住就行，PPT里没有涉及

问题3

这题C明显错误，选ABD，可用于深度学习

问题4

这题选D，对于A，当前提不成立的时候，符合命题恒为真；对于C，

作业——经典题目

1、凡是涉及程序设计(Prog)且有挑战性(Chall)的课程小张都喜欢；

2、计算机专业(Comp)的专业课程都涉及程序设计；

3、 AI是计算机专业的一门专业课程且是一门具有挑战性的课程。

请问：小张喜欢人工智能这门课程吗？

要求：定义谓词，用一阶谓词逻辑公式表示已知的事实和要证明的结论，并用归结原理证明该结论

踩坑点

混淆∩与→，命题2为推出关系。