离散数学2：命题逻辑的推理

文章目录

什么是有效的结论？
如何判断推理是否正确？
- 判断前提与结论所组成的蕴涵式是否为重言式
- 构造证明

什么是有效的结论？

若前提为k个命题公式：A1,A2,A3,...,AkA_1,A_2,A_3,...,A_kA1,A2,A3,...,Ak，结论为命题公式BBB，对命题公式赋值时，前提和结论的取值情况有以下4种：

A1∧A2∧...∧AkA_1\land A_2\land ...\land A_kA1∧A2∧...∧Ak为0，BBB为0
A1∧A2∧...∧AkA_1\land A_2\land ...\land A_kA1∧A2∧...∧Ak为0，BBB为1
A1∧A2∧...∧AkA_1\land A_2\land ...\land A_kA1∧A2∧...∧Ak为1，BBB为0
A1∧A2∧...∧AkA_1\land A_2\land ...\land A_kA1∧A2∧...∧Ak为1，BBB为1

根据定义，只要不出现第3种情况，推理就是正确的，结论就是有效的。
即推理正确当且仅当A1∧A2∧...∧Ak→B是重言式A_1\land A_2\land ...\land A_k\rightarrow B是重言式A1∧A2∧...∧Ak→B是重言式，记为：A1∧A2∧...∧Ak⇒BA_1\land A_2\land ...\land A_k\Rightarrow BA1∧A2∧...∧Ak⇒B.
注意：推理正确并不能保证结论一定成立，因为前提可能就不成立。

与用A⇔BA \Leftrightarrow BA⇔B表示A↔BA\leftrightarrow BA↔B是重言式类似，用A⇒BA \Rightarrow BA⇒B表示A→BA\rightarrow BA→B是重言式。
‘⇔’‘\Leftrightarrow’‘⇔’和‘⇒’‘\Rightarrow’‘⇒’不是逻辑联结词，只是用来表示某种重言式的一种方法。

如何判断推理是否正确？

若A→BA\rightarrow BA→B推理正确，即A→BA\rightarrow BA→B重言，则公式可写为：A⇒BA\Rightarrow BA⇒B.

判断推理是否正确有两种方法

证明该蕴含式是否为重言式
构造证明法

判断前提与结论所组成的蕴涵式是否为重言式

即证明A→B⇔1A\rightarrow B\Leftrightarrow 1A→B⇔1

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

是重言式

不是重言式

推理对应的蕴涵式

推理正确

找出成假赋值

推理错误

等值演算法只能用来证明蕴涵式是重言式，对于不正确的推理，应先等值演算到一定步骤，将推理的形式结构化简，使其容易观察出成假赋值，举出成假赋值 即可说明不重言，推理错误。或者也可接着等值演算化简后的式子，求出其主析取范式，据此判断其不重言。

构造证明

当前提和结论都是比较复杂的命题公式或者所包含的命题变元很多时，构造证明是更有效的推理方法。
推理的形式结构中A1,A2,...,AkA_1, A_2, ..., A_kA1,A2,...,Ak为前提, 结论为BBB, 若能用以上推理规则, 构造出证明序列, 序列的最后公式为BBB, 则说明此推理正确, BBB是A1,A2,...,AkA_1, A_2, ..., A_kA1,A2,...,Ak的逻辑结论.

构造证明的格式:
前提：
结论：
证明：
           ①…  （前提引入）
           ②      （…）
           ③      （…）

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

存在多个蕴涵式

蕴涵式

假言推理

拒取式

假言三段论

析取式

构造性二难,破坏性二难

合取式

化简!!!

否定式

拒取式

析取三段论

前提中无,结论中有

一定存在附加

如果要证明的结论为蕴涵式形式，则考虑使用附加前提法。

附加前提法的优点在于：增加了一个条件（附加前提引入），简化了证明目标

如果要证明的结论为单个文字或为析取式形式，则考虑使用归谬法。

归谬法的优点也是增加了条件（否定结论引入）（尤其是在结论为析取式的情况下），改变了证明思路。

常用置换：

p→(q→r)⇔q→(p→r)p\rightarrow (q\rightarrow r) \Leftrightarrow q\rightarrow (p\rightarrow r)p→(q→r)⇔q→(p→r)
p↔qp\leftrightarrow qp↔q （前提引入）
(p→q)∧(q→p)(p\rightarrow q)\land(q\rightarrow p)(p→q)∧(q→p) （置换）
p→qp\rightarrow qp→q （化简）
p→q⇔¬q→¬pp\rightarrow q \Leftrightarrow \neg q \rightarrow \neg pp→q⇔¬q→¬p
p∨q⇔¬p→qp\vee q \Leftrightarrow \neg p\rightarrow qp∨q⇔¬p→q