297 lines
98 KiB
JavaScript
297 lines
98 KiB
JavaScript
import{_ as n,D as l,c as h,j as s,a as i,I as k,a4 as t,o as p}from"./chunks/framework.DtvhUNIn.js";const D=JSON.parse('{"title":"程序示例——命题逻辑与模型检测","description":"","frontmatter":{},"headers":[],"relativePath":"技术资源汇总(杭电支持版)/4.人工智能/4.3.2.1程序示例——命题逻辑与模型检测.md","filePath":"技术资源汇总(杭电支持版)/4.人工智能/4.3.2.1程序示例——命题逻辑与模型检测.md"}'),e={name:"技术资源汇总(杭电支持版)/4.人工智能/4.3.2.1程序示例——命题逻辑与模型检测.md"},E=s("h1",{id:"程序示例——命题逻辑与模型检测",tabindex:"-1"},[i("程序示例——命题逻辑与模型检测 "),s("a",{class:"header-anchor",href:"#程序示例——命题逻辑与模型检测","aria-label":'Permalink to "程序示例——命题逻辑与模型检测"'},"")],-1),r=s("div",{class:"warning custom-block"},[s("p",{class:"custom-block-title"},"😋"),s("p",null,"阅读程序中涉及命题逻辑的部分，然后“玩一玩”程序！"),s("p",null,"完成习题")],-1),d={class:"tip custom-block"},y=s("p",{class:"custom-block-title"},"📥",-1),g=t(`<h2 id="sentence——父类" tabindex="-1">Sentence——父类 <a class="header-anchor" href="#sentence——父类" aria-label="Permalink to "Sentence——父类""></a></h2><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">class</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> Sentence</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(): </span><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># 父类</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> evaluate</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """计算逻辑表达式的值"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> raise</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> Exception</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"nothing to evaluate"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> formula</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回表示逻辑表达式的字符串形式。"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> ""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> symbols</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回逻辑表达式中所有命题符号的集合。"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> set</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">()</span></span>
|
||
<span class="line"><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> @</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">classmethod</span><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # @classmethod 装饰器 使得类方法可以在类上被调用 Sentence.validate(...)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> validate</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(cls, sentence):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """验证操作数是否是 Sentence 或其子类"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> not</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> isinstance</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(sentence, Sentence):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> raise</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> TypeError</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"must be a logical sentence"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> @</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">classmethod</span><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # @classmethod 装饰器 使得类方法可以在类上被调用 Sentence.parenthesize(...)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> parenthesize</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(cls, s):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """如果表达式尚未加圆括号，则加圆括号。"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> balanced</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(s):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """检查字符串是否有配对的括号。"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> count </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> 0</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> c </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> s:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> c </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> "("</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> count </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">+=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> 1</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> elif</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> c </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> ")"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> count </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"><=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> 0</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> False</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> count </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">-=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> 1</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> count </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> 0</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> not</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> len</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(s) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">or</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> s.isalpha() </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">or</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> (s[</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">0</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">] </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> "("</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> and</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> s[</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">-</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">1</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">] </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> ")"</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> and</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> balanced(s[</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">1</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">-</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">1</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">])):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> s</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> else</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">s</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">)"</span></span></code></pre></div><h2 id="symbol——命题符号类" tabindex="-1">Symbol——命题符号类 <a class="header-anchor" href="#symbol——命题符号类" aria-label="Permalink to "Symbol——命题符号类""></a></h2><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">class</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> Symbol</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;">Sentence</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __init__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, name):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """初始化命题符号"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.name </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> name</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __eq__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, other):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """定义命题符号的相等"""</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> </span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> isinstance</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(other, Symbol) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.name </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> other.name</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> ...</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> evaluate</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """命题符号在模型中赋值"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> try</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> bool</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(model[</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.name])</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> except</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> KeyError</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> raise</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> EvaluationException(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"variable </span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.name</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> not in model"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> formula</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回表示命题符号的字符串形式。"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.name</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> symbols</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回命题符号的集合。"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> {</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.name}</span></span></code></pre></div><h2 id="not——逻辑非类" tabindex="-1">Not——逻辑非类 <a class="header-anchor" href="#not——逻辑非类" aria-label="Permalink to "Not——逻辑非类""></a></h2><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">class</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> Not</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;">Sentence</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __init__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, operand):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """验证操作数是否是 Sentence 或其子类"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.validate(operand)</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.operand </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> operand</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __eq__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, other):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """定义相等"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> isinstance</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(other, Not) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.operand </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> other.operand</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> ...</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> evaluate</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """逻辑非在模型中的赋值"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> not</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.operand.evaluate(model)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> formula</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回表示逻辑非的字符串形式"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> "¬"</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> +</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.parenthesize(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.operand.formula())</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> symbols</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回逻辑非中的命题符号的集合"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.operand.symbols()</span></span></code></pre></div><h2 id="and——逻辑乘类" tabindex="-1">And——逻辑乘类 <a class="header-anchor" href="#and——逻辑乘类" aria-label="Permalink to "And——逻辑乘类""></a></h2><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">class</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> And</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;">Sentence</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __init__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">*</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">conjuncts):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> conjunct </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> conjuncts:</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """验证操作数是否是 Sentence 或其子类"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.validate(conjunct)</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.conjuncts </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> list</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(conjuncts)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __eq__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, other):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """定义相等"""</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> </span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> isinstance</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(other, And) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.conjuncts </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> other.conjuncts</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> add</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, conjunct):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """添加命题"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.validate(conjunct)</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.conjuncts.append(conjunct)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> evaluate</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """逻辑乘在模型中的赋值"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> all</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(conjunct.evaluate(model) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> conjunct </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.conjuncts)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> formula</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回表示逻辑乘的字符串形式"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> len</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.conjuncts) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> 1</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.conjuncts[</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">0</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">].formula()</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> " ∧ "</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.join([Sentence.parenthesize(conjunct.formula())</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> conjunct </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.conjuncts])</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> symbols</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """"返回逻辑乘中的所有命题符号的集合"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> set</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.union(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">*</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">[conjunct.symbols() </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> conjunct </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.conjuncts])</span></span></code></pre></div><h2 id="or——逻辑和类" tabindex="-1">Or——逻辑和类 <a class="header-anchor" href="#or——逻辑和类" aria-label="Permalink to "Or——逻辑和类""></a></h2><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">class</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> Or</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;">Sentence</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __init__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">*</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">disjuncts):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> disjunct </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> disjuncts:</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """验证操作数是否是 Sentence 或其子类"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.validate(disjunct)</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.disjuncts </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> list</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(disjuncts)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __eq__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, other):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """定义相等"""</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> </span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> isinstance</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(other, Or) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.disjuncts </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> other.disjuncts</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> ...</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> evaluate</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """逻辑和在模型中的赋值"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> any</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(disjunct.evaluate(model) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> disjunct </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.disjuncts)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> formula</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回表示逻辑和的字符串形式"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> len</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.disjuncts) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> 1</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.disjuncts[</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">0</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">].formula()</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> " ∨ "</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.join([Sentence.parenthesize(disjunct.formula())</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> disjunct </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.disjuncts])</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> symbols</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """"返回逻辑乘中的所有命题符号的集合"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> set</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.union(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">*</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">[disjunct.symbols() </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> disjunct </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.disjuncts])</span></span></code></pre></div><h2 id="implication——逻辑蕴含类" tabindex="-1">Implication——逻辑蕴含类 <a class="header-anchor" href="#implication——逻辑蕴含类" aria-label="Permalink to "Implication——逻辑蕴含类""></a></h2><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">class</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> Implication</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;">Sentence</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __init__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, antecedent, consequent):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """验证操作数是否是 Sentence 或其子类"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.validate(antecedent)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.validate(consequent)</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """前件"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.antecedent </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> antecedent</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """后件"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.consequent </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> consequent</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __eq__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, other):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """定义相等"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> (</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">isinstance</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(other, Implication)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.antecedent </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> other.antecedent</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.consequent </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> other.consequent)</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> ...</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> evaluate</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """逻辑蕴含在模型中的赋值"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> ((</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">not</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.antecedent.evaluate(model))</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> or</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.consequent.evaluate(model))</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> formula</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回表示逻辑蕴含的字符串形式"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> antecedent </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.parenthesize(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.antecedent.formula())</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> consequent </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.parenthesize(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.consequent.formula())</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">antecedent</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> => </span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">consequent</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> symbols</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """"返回逻辑蕴含中的所有命题符号的集合"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> set</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.union(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.antecedent.symbols(), </span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.consequent.symbols())</span></span></code></pre></div><h2 id="biconditional——逻辑等值类" tabindex="-1">Biconditional——逻辑等值类 <a class="header-anchor" href="#biconditional——逻辑等值类" aria-label="Permalink to "Biconditional——逻辑等值类""></a></h2><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">class</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> Biconditional</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;">Sentence</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __init__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, left, right):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """验证操作数是否是 Sentence 或其子类"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.validate(left)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.validate(right)</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.left </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> left</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.right </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> right</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> __eq__</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, other):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """定义相等"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> (</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">isinstance</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(other, Biconditional)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.left </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> other.left</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.right </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">==</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> other.right)</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> ...</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> evaluate</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self, model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """逻辑等值在模型中的赋值"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> ((</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.left.evaluate(model)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> and</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.right.evaluate(model))</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> or</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> (</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">not</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.left.evaluate(model)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> and</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> not</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.right.evaluate(model)))</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> formula</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """返回表示逻辑等值的字符串形式"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> left </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.parenthesize(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">str</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.left))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> right </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Sentence.parenthesize(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">str</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.right))</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">left</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> <=> </span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">right</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> symbols</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(self):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """"返回逻辑等值中的所有命题符号的集合"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> set</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.union(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.left.symbols(), </span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">self</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.right.symbols())</span></span></code></pre></div><h2 id="model-check-——模型检测算法" tabindex="-1">Model_check()——模型检测算法 <a class="header-anchor" href="#model-check-——模型检测算法" aria-label="Permalink to "Model_check()——模型检测算法""></a></h2><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> model_check</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(knowledge, query):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> 检查知识库是否推理蕴含查询结论。</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> >>> </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">p = Symbol("p")</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> >>> </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">q = Symbol("q")</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> >>> </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">r = Symbol("r")</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> >>> </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">knowledge = And(p, q, Implication(And(p, q), r))</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> >>> </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">knowledge.formula()</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> 'p ∧ q ∧ ((p ∧ q) => r)'</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> >>> </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">query = r</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> >>> </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">model_check(knowledge,query)</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> True</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> check_all</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(knowledge, query, symbols, model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;"> """检查给定特定模型的知识库是否推理蕴含查询结论。"""</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 如果模型已经为所有的命题符号赋值</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> not</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> symbols: </span><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># symbols 为空即所有 symbols 都在模型中被赋值</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 若模型中的知识库为真，则查询结论也必须为真</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> knowledge.evaluate(model):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> query.evaluate(model)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> True</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> else</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 递归生成并检测所有模型</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 选择其余未使用的命题符号之一</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> remaining </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> symbols.copy()</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> p </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> remaining.pop()</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 创建一个命题符号为 true 的模型</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model_true </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model.copy()</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model_true[p] </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> True</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 创建一个命题符号为 false 的模型</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model_false </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model.copy()</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model_false[p] </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> False</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 确保在两种模型中都进行蕴含推理</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> (check_all(knowledge, query, remaining, model_true) </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">and</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> check_all(knowledge, query, remaining, model_false))</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 获取知识库和查询结论中的所有命题符号</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> symbols </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> set</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">.union(knowledge.symbols(), query.symbols())</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 进行模型检测</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> return</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> check_all(knowledge, query, symbols, </span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">dict</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">())</span></span></code></pre></div><h2 id="线索游戏" tabindex="-1">线索游戏 <a class="header-anchor" href="#线索游戏" aria-label="Permalink to "线索游戏""></a></h2><p>在游戏中，一个人在某个地点使用工具实施了谋杀。人、工具和地点用卡片表示。每个类别的一张卡片被随机挑选出来，放在一个信封里，由参与者来揭开真相。参与者通过揭开卡片并从这些线索中推断出信封里必须有什么来做到这一点。我们将使用之前的模型检查算法来揭开这个谜团。在我们的模型中，我们将已知与谋杀有关的项目标记为 True，否则标记为 False。</p><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">import</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> termcolor</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">from</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> logic </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">import</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> *</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">mustard </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"ColMustard"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">plum </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"ProfPlum"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">scarlet </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"MsScarlet"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">characters </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> [mustard, plum, scarlet]</span></span>
|
||
<span class="line"></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">ballroom </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"ballroom"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">kitchen </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"kitchen"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">library </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"library"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">rooms </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> [ballroom, kitchen, library]</span></span>
|
||
<span class="line"></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knife </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"knife"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">revolver </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"revolver"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">wrench </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"wrench"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">weapons </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> [knife, revolver, wrench]</span></span>
|
||
<span class="line"></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">symbols </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> characters </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">+</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> rooms </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">+</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> weapons</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">def</span><span style="--shiki-light:#6F42C1;--shiki-dark:#B392F0;"> check_knowledge</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(knowledge):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> symbol </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> symbols:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model_check(knowledge, symbol):</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> termcolor.cprint(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">symbol</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">: YES"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">, </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> elif</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> not</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model_check(knowledge, Not(symbol)):</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"> # 模型检测无法确定知识库可以得出 Not(symbol) 即 symbol 是可能的</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> print</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">symbol</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">: MAYBE"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> else</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">:</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> termcolor.cprint(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">symbol</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">: No"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">, </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># 必须有人、房间和武器。</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knowledge </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> And(</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Or(mustard, plum, scarlet),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Or(ballroom, kitchen, library),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Or(knife, revolver, wrench)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># 初始卡牌</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knowledge.add(And(</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Not(mustard), Not(kitchen), Not(revolver)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># 未知卡牌</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knowledge.add(Or(</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Not(scarlet), Not(library), Not(wrench)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># 已知卡牌</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knowledge.add(Not(plum))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knowledge.add(Not(ballroom))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">check_knowledge(knowledge)</span></span></code></pre></div><h2 id="mastermind-游戏" tabindex="-1">Mastermind 游戏 <a class="header-anchor" href="#mastermind-游戏" aria-label="Permalink to "Mastermind 游戏""></a></h2><p>在这个游戏中，玩家一按照一定的顺序排列颜色，然后玩家二必须猜测这个顺序。每一轮，玩家二进行猜测，玩家一返回一个数字，指示玩家二正确选择了多少颜色。让我们用四种颜色模拟一个游戏。假设玩家二猜测以下顺序：</p><p><img src="https://cdn.xyxsw.site/FZCJbOzr9o4oQPx7SNGcFxTSnRd.png" alt=""></p><p>玩家一回答“二”。因此，我们知道其中一些两种颜色位于正确的位置，而另两种颜色则位于错误的位置。根据这些信息，玩家二试图切换两种颜色的位置。</p><p><img src="https://cdn.xyxsw.site/Y80wbn96sol7PUxO5fKcOA9Hnbg.png" alt=""></p><p>现在玩家一回答“零”。因此，玩家二知道切换后的颜色最初位于正确的位置，这意味着未被切换的两种颜色位于错误的位置。玩家二切换它们。</p><p><img src="https://cdn.xyxsw.site/EuXObldHcoaO74xIzZocQQKTn4k.png" alt=""></p><p>在命题逻辑中表示这一点需要我们有 (颜色的数量)$^2$个原子命题。所以，在四种颜色的情况下，我们会有命题 red0，red1，red2，red3，blue0…代表颜色和位置。下一步是用命题逻辑表示游戏规则（每个位置只有一种颜色，没有颜色重复），并将它们添加到知识库中。最后一步是将我们所拥有的所有线索添加到知识库中。在我们的案例中，我们会补充说，在第一次猜测中，两个位置是错误的，两个是正确的，而在第二次猜测中没有一个是对的。利用这些知识，模型检查算法可以为我们提供难题的解决方案。</p><div class="language-python vp-adaptive-theme"><button title="Copy Code" class="copy"></button><span class="lang">python</span><pre class="shiki shiki-themes github-light github-dark vp-code" tabindex="0"><code><span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">from</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> logic </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">import</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> *</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">colors </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> [</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">, </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"blue"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">, </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">, </span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"yellow"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">]</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">symbols </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> []</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> i </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> range</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">4</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> color </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> colors:</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> symbols.append(Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">color</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">i</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knowledge </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> And()</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># 每种颜色都有一个位置。</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> color </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> colors:</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> knowledge.add(Or(</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">color</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">0"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">color</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">1"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">color</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">2"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">color</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">3"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> ))</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># 每种颜色只有一个位置。</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> color </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> colors:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> i </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> range</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">4</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> j </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> range</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">4</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> i </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">!=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> j:</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> knowledge.add(Implication(</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">color</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">i</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Not(Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">color</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">j</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> ))</span></span>
|
||
<span class="line"><span style="--shiki-light:#6A737D;--shiki-dark:#6A737D;"># 每个位置只有一种颜色。</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> i </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> range</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">4</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">):</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> c1 </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> colors:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> c2 </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> colors:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> c1 </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">!=</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> c2:</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> knowledge.add(Implication(</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">c1</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">i</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Not(Symbol(</span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">f</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">c2</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}{</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">i</span><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">}</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> ))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knowledge.add(Or(</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> And(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red0"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"blue1"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green2"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"yellow3"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> And(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red0"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green2"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"blue1"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"yellow3"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> And(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red0"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"yellow3"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"blue1"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green2"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> And(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"blue1"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green2"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red0"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"yellow3"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> And(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"blue1"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"yellow3"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red0"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green2"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> And(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green2"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"yellow3"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red0"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)), Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"blue1"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">knowledge.add(And(</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"blue0"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"red1"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"green2"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">)),</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> Not(Symbol(</span><span style="--shiki-light:#032F62;--shiki-dark:#9ECBFF;">"yellow3"</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))</span></span>
|
||
<span class="line"><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">))</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;">print</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(knowledge.formula())</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">for</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> symbol </span><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;">in</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> symbols:</span></span>
|
||
<span class="line"><span style="--shiki-light:#D73A49;--shiki-dark:#F97583;"> if</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;"> model_check(knowledge, symbol):</span></span>
|
||
<span class="line"><span style="--shiki-light:#005CC5;--shiki-dark:#79B8FF;"> print</span><span style="--shiki-light:#24292E;--shiki-dark:#E1E4E8;">(symbol)</span></span></code></pre></div><h2 id="quiz" tabindex="-1">Quiz <a class="header-anchor" href="#quiz" aria-label="Permalink to "Quiz""></a></h2><ol><li><p>下面的问题将问你关于以下逻辑句子的问题。1.如果 Hermione 在图书馆，那么 Harry 在图书馆。2.Hermione 在图书馆里。3.Ron 在图书馆，Ron 不在图书馆。4.Harry 在图书馆。5.Harry 不在图书馆，或者 Hermione 在图书馆。6.Rom 在图书馆，或者 Hermione 在图书馆。</p><p>以下哪一个逻辑蕴含推理是正确的？</p><ol><li>$1\\vDash 4$</li><li>$5\\vDash 6$</li><li>$1\\vDash 2$</li><li>$6\\vDash 2$</li><li>$2\\vDash 5$</li><li>$6\\vDash 3$</li></ol></li><li><p>除了讲义上讨论的连接词之外，还有其他的逻辑连接词。其中最常见的是“异或”（用符号$\\oplus$表示）。表达式$A\\oplus B$表示句子“A 或 B，但不是两者都有。”以下哪一个在逻辑上等同于$A\\oplus B$？</p><ol><li>$(A ∨ B) ∧ ¬ (A ∨ B)$</li><li>$(A ∨ B) ∧ (A ∧ B)$</li><li>$(A ∨ B) ∧ ¬ (A ∧ B)$</li><li>$(A ∧ B) ∨ ¬ (A ∨ B)$</li></ol></li><li><p>设命题变量$R$为“今天下雨”，变量$C$为“今天多云”，变量$S$ 为“今天晴”。下面哪一个是“如果今天下雨，那么今天多云但不是晴天”这句话的命题逻辑表示？</p><ol><li>$(R → C) ∧ ¬S$</li><li>$R → C → ¬S$</li><li>$R ∧ C ∧ ¬S$</li><li>$R → (C ∧ ¬S)$</li><li>$(C ∨ ¬S) → R$</li></ol></li><li><p>在一阶逻辑中，考虑以下谓词符号。$Student(x)$表示“x 是学生”的谓词。$Course(x)$代表“x 是课程”的谓词，$Enrolled(x,y)$表示“x 注册了 y”的谓词以下哪一项是“有一门课程是 Harry 和 Hermione 都注册的”这句话的一阶逻辑翻译？</p><ol><li>$∀x(Course(x)∧Enrolled(Harry, x) ∧ Enrolled(Hermione, x))$</li><li>$∀x(Enrolled(Harry, x) ∨ Enrolled(Hermione, x))$</li><li>$∀x(Enrolled(Harry, x) ∧ ∀y Enrolled(Hermione, y))$</li><li>$∃xEnrolled(Harry, x) ∧ ∃y Enrolled(Hermione, y)$</li><li>$∃x(Course(x) ∧ Enrolled(Harry, x) ∧ Enrolled(Hermione, x))$</li><li>$∃x(Enrolled(Harry, x) ∨ Enrolled(Hermione, x))$</li></ol></li></ol>`,30);function F(o,c,u,C,q,B){const a=l("Download");return p(),h("div",null,[E,r,s("div",d,[y,s("p",null,[i("本节附件下载 "),k(a,{url:"https://cdn.xyxsw.site/code/2-Lecture.zip"})])]),g])}const m=n(e,[["render",F]]);export{D as __pageData,m as default};
|