第一章命题逻辑

文章目录

第一章命题逻辑
- 1.1 判断语句
- 1.2 自然演绎
- 1.3 作为形式语言的命题逻辑
- 1.4 命题逻辑的语义
- 1.5 范式
- 1.6 SAT 求解机

1.1 判断语句

¬ \neg ¬ ：否定，negation
∨ \lor ∨ ：析取，disjunction
∧ \land ∧ ：合取，conjunction
→ \rightarrow → ：蕴含，implication

约定：

¬ \neg ¬ 比 ∨ \lor ∨ 和 ∧ \land ∧ 具有更高的绑定优先级
∨ \lor ∨ 和 ∧ \land ∧ 比 → \rightarrow → 具有更高的绑定优先级
蕴含 → \rightarrow → 是右结合的：形如 p → q → r p \rightarrow q \rightarrow r p→q→r 的表达式表示 p → ( q → r ) p \rightarrow (q \rightarrow r) p→(q→r)

1.2 自然演绎

矢列： ϕ 1 , ϕ 2 , ⋯ , ϕ n ⊢ ψ \phi_1, \phi_2, \cdots, \phi_n \vdash \psi ϕ1,ϕ2,⋯,ϕn⊢ψ ，表示由前提 ϕ 1 , ϕ 2 , ⋯ , ϕ n \phi_1, \phi_2, \cdots, \phi_n ϕ1,ϕ2,⋯,ϕn 得到结论 ψ \psi ψ 。

合取规则：
- 合取引入
  ϕ ψ ϕ ∧ ψ ∧ i \frac{\phi \quad \psi}{\phi \land \psi} \land i ϕ∧ψϕψ∧i
  横线上面是该规则的两个前提，横线下面是结论，横线右方是规则的名称， ∧ i \land i ∧i 读作“合取引入”；
- 合取消去
  ϕ ∧ ψ ϕ ∧ e 1 ϕ ∧ ψ ψ ∧ e 2 \frac{\phi \land \psi}{\phi} \land e_1 \qquad \frac{\phi \land \psi}{\psi} \land e_2 ϕϕ∧ψ∧e1ψϕ∧ψ∧e2
  规则 ∧ e 1 \land e_1 ∧e1 表示如果有了 ϕ ∧ ψ \phi \land \psi ϕ∧ψ 的证明，则可以通过该规则得到 ϕ \phi ϕ 的一个证明；规则 ∧ e 2 \land e_2 ∧e2 表示类似的事情；
双重否定规则
¬ ¬ ϕ ϕ ¬ ¬ e ϕ ¬ ¬ ϕ ¬ ¬ i \frac{\neg \neg \phi}{\phi} \neg \neg e \qquad \frac{\phi}{\neg \neg \phi} \neg \neg i ϕ¬¬ϕ¬¬e¬¬ϕϕ¬¬i
隐含消去规则（分离规则）
ϕ ϕ → ψ ψ → e \frac{\phi \quad \phi \rightarrow \psi}{\psi} \rightarrow e ψϕϕ→ψ→e
反证规则（MT）
ϕ → ψ ¬ ψ ¬ ϕ M T \frac{\phi \rightarrow \psi \quad \neg \psi}{\neg \phi} MT ¬ϕϕ→ψ¬ψMT
蕴含引入规则
[ ϕ ⋮ ψ ] ϕ → ψ → i \frac{ \begin{bmatrix} \phi \\ \vdots \\ \psi \end{bmatrix} }{\phi \rightarrow \psi} \rightarrow i ϕ→ψ⎣⎢⎡ϕ⋮ψ⎦⎥⎤→i
为证明 ϕ → ψ \phi \rightarrow \psi ϕ→ψ ，做临时的假定 ϕ \phi ϕ ，然后证明 ψ \psi ψ 。在证明 ψ \psi ψ 的过程中，可以使用 ϕ \phi ϕ ，以及任何其他公示。一般来讲，只有在公式 ϕ \phi ϕ 先于该位置出现，而且出现 ϕ \phi ϕ 的矩形框都没有关闭的情况下，才可以使用公式 ϕ \phi ϕ 。紧跟在关闭的矩形框后面的行必须与使用该矩形框的规则所得到的结论模式相匹配，即如果一个矩形框的第一个公式是 ϕ \phi ϕ ，最后一个公式是 ψ \psi ψ ，那么紧跟在该矩形框后面的行必须是 ϕ → ψ \phi \rightarrow \psi ϕ→ψ 。
析取规则
ϕ ϕ ∨ ψ ∨ i 1 ψ ϕ ∨ ψ ∨ i 2 ϕ ∨ ψ [ ϕ ⋮ X ] [ ψ ⋮ X ] X ∨ e \frac{\phi}{\phi \lor \psi} \lor i_1 \qquad \frac{\psi}{\phi \lor \psi} \lor i_2 \\ \frac{ \phi \lor \psi \quad \begin{bmatrix} \phi \\ \vdots \\ \mathcal X \end{bmatrix} \begin{bmatrix} \psi \\ \vdots \\ \mathcal X \end{bmatrix} }{\mathcal X} \lor e ϕ∨ψϕ∨i1ϕ∨ψψ∨i2Xϕ∨ψ⎣⎢⎡ϕ⋮X⎦⎥⎤⎣⎢⎡ψ⋮X⎦⎥⎤∨e
否定规则

矛盾是形如 ϕ ∧ ¬ ϕ \phi \land \neg \phi ϕ∧¬ϕ 或 ¬ ϕ ∧ ϕ \neg \phi \land \phi ¬ϕ∧ϕ 的表达式；公式 ⊥ \bot ⊥ 代表矛盾；矛盾可以推导出任何公式：
⊥ ϕ ⊥ e \frac{\bot}{\phi} \bot e ϕ⊥⊥e

ϕ ¬ ϕ ⊥ ¬ e [ ϕ ⋮ ⊥ ] ¬ ϕ ¬ i \frac{\phi \quad \neg \phi}{\bot} \neg e \\ \frac{ \begin{bmatrix} \phi \\ \vdots \\ \bot \end{bmatrix} }{\neg \phi} \neg i ⊥ϕ¬ϕ¬e¬ϕ⎣⎢⎡ϕ⋮⊥⎦⎥⎤¬i
派生规则

反证规则 ϕ → ψ ¬ ψ ¬ ϕ M T \frac{\phi \rightarrow \psi \quad \neg \psi}{\neg \phi} MT ¬ϕϕ→ψ¬ψMT 可以从否定规则推导得到。
- 反证法（PBC）
  [ ¬ ϕ ⋮ ⊥ ] ϕ P B C \frac{ \begin{bmatrix} \neg \phi \\ \vdots \\ \bot \end{bmatrix} }{\phi} PBC ϕ⎣⎢⎡¬ϕ⋮⊥⎦⎥⎤PBC
  ¬ ϕ \neg \phi ¬ϕ 推出矛盾，则 ϕ \phi ϕ 成立。
- 排中率（LEM）： ϕ ∨ ¬ ϕ \phi \lor \neg \phi ϕ∨¬ϕ 是真的。

逻辑等价：命题公式 ϕ \phi ϕ 和 ψ \psi ψ 是逻辑等价的，当且仅当矢列式 ϕ ⊣ ϕ \phi \dashv \phi ϕ⊣ϕ 和 ϕ ⊢ ψ \phi \vdash \psi ϕ⊢ψ 都是有效的。用 ϕ ⊣ ⊢ ψ \phi \dashv \vdash \psi ϕ⊣⊢ψ 表示。

以下六个式子逻辑等价：
¬ ( p ∧ q ) ⊣ ⊢ ¬ q ∨ ¬ p ¬ ( p ∨ q ) ⊣ ⊢ ¬ q ∧ ¬ p p → q ⊣ ⊢ ¬ q → ¬ p p → q ⊣ ⊢ ¬ p ∨ q p ∧ q → p ⊣ ⊢ r ∨ ¬ r p ∧ q → r ⊣ ⊢ p → ( q → r ) \neg (p \land q) \ \dashv \vdash \ \neg q \lor \neg p \qquad \neg (p \lor q) \ \dashv \vdash \ \neg q \land \neg p \\ p \rightarrow q \ \dashv \vdash \ \neg q \rightarrow \neg p \qquad p \rightarrow q \ \dashv \vdash \ \neg p \lor q \\ p \land q \rightarrow p \ \dashv \vdash \ r \lor \neg r \qquad p \land q \rightarrow r \ \dashv \vdash \ p \rightarrow (q \rightarrow r) ¬(p∧q) ⊣⊢ ¬q∨¬p¬(p∨q) ⊣⊢ ¬q∧¬pp→q ⊣⊢ ¬q→¬pp→q ⊣⊢ ¬p∨qp∧q→p ⊣⊢ r∨¬rp∧q→r ⊣⊢ p→(q→r)

1.3 作为形式语言的命题逻辑

合式公式定义：（使用 Bachus Naur 范式(BNF)）
ϕ : : = p ∣ ( ¬ ϕ ) ∣ ( ϕ ∧ ϕ ) ∣ ( ϕ ∨ ϕ ) ∣ ( ϕ → ϕ ) \phi ::= p \ | \ (\neg \phi) \ | \ (\phi \land \phi) \ | \ (\phi \lor \phi) \ | \ (\phi \rightarrow \phi) ϕ::=p ∣ (¬ϕ) ∣ (ϕ∧ϕ) ∣ (ϕ∨ϕ) ∣ (ϕ→ϕ)
其中 p p p 代表任意原子命题。

1.4 命题逻辑的语义

语义等价：两个式子的真值表一致，则称他们是语义等价的。如 ϕ → ψ \phi \rightarrow \psi ϕ→ψ 和 ¬ ϕ ∨ ψ \neg \phi \lor \psi ¬ϕ∨ψ 。

数学归纳法：

基本情况：自然数 1 有性质 M，即有 M(1) 的证明；
归纳步骤：如果 n 是我们假设有性质 M(n) 的自然数（归纳假设），那么，可以证明 n+1 有性质 M(n+1) ；即有一个 M(n) → M(n+1) 的证明。

串值归纳：证明 M(n+1) 不仅需要 M(n) ，而且需要合取 M ( 1 ) ∧ M ( 2 ) ∧ ⋯ ∧ M ( n ) M(1) \land M(2) \land \cdots \land M(n) M(1)∧M(2)∧⋯∧M(n) 。

结构归纳法：串值归纳法的一个特例。

合式公式的高度为 1 加上它的语法分析树中最长路径的长度。

若对所有命题 ϕ 1 , ϕ 2 , ⋯ ϕ n \phi_1, \phi_2, \cdots \phi_n ϕ1,ϕ2,⋯ϕn 都赋值为 T 的一切赋值， ψ \psi ψ 也赋值为 T，则说 ϕ 1 , ϕ 2 , ⋯ , ϕ n ⊨ ψ \phi_1, \phi_2, \cdots, \phi_n \models \psi ϕ1,ϕ2,⋯,ϕn⊨ψ 成立，称 ⊨ \models ⊨ 为语义推导关系。

对于命题逻辑公式 ϕ 1 , ϕ 2 , ⋯ , ϕ n , ψ \phi_1, \phi_2, \cdots, \phi_n, \psi ϕ1,ϕ2,⋯,ϕn,ψ ：

当且仅当 ϕ 1 , ϕ 2 , ⋯ ϕ n ⊢ ψ \phi_1, \phi_2, \cdots \phi_n \vdash \psi ϕ1,ϕ2,⋯ϕn⊢ψ 是有效的， ϕ 1 , ϕ 2 , ⋯ , ϕ n ⊨ ψ \phi_1, \phi_2, \cdots, \phi_n \models \psi ϕ1,ϕ2,⋯,ϕn⊨ψ 成立；
当且仅当 ϕ 1 , ϕ 2 , ⋯ , ϕ n ⊨ ψ \phi_1, \phi_2, \cdots, \phi_n \models \psi ϕ1,ϕ2,⋯,ϕn⊨ψ 成立， ϕ 1 , ϕ 2 , ⋯ ϕ n ⊢ ψ \phi_1, \phi_2, \cdots \phi_n \vdash \psi ϕ1,ϕ2,⋯ϕn⊢ψ 是有效的。

重言式：各种赋值情况下结果都是 T，即当且仅当 ⊨ ψ \models \psi ⊨ψ 。

若 ⊨ η \models \eta ⊨η 成立，则 ⊢ η \vdash \eta ⊢η 是有效的。换言之，若 η \eta η 是重言式，则 η \eta η 是定理。

1.5 范式

语义等价：对与命题逻辑公式 ϕ , ψ \phi,\psi ϕ,ψ ，说他们语义等价，当且仅当 ϕ ⊨ ψ \phi \models \psi ϕ⊨ψ 与 ψ ⊨ ϕ \psi \models \phi ψ⊨ϕ 成立。记为： ϕ ≡ ψ \phi \equiv \psi ϕ≡ψ 。进一步，如果 ⊨ ϕ \models \phi ⊨ϕ 成立，称 ϕ \phi ϕ 是有效的。

也可以定义 ϕ ≡ ψ \phi \equiv \psi ϕ≡ψ 是指 ⊨ ( ϕ → ψ ) ∧ ( ψ → ϕ ) \models (\phi \rightarrow \psi) \land (\psi \rightarrow \phi) ⊨(ϕ→ψ)∧(ψ→ϕ) 。

由于合理性和完备性，语义等价和逻辑等价是一致的。

合取范式：文字 L L L 或者原子 p p p ，或者原子的否定 ¬ p \neg p ¬p 。公式 C C C 如果是若干子句的合取，则是一个合取范式(conjuncitve normal form, CNF)，而每个子句 D D D 是文字的析取：
L : : = p ∣ ¬ p D : : = L ∣ L ∨ D C : : = D ∣ D ∧ C L ::= p \quad | \quad \neg p \\ D::= L \quad | \quad L \lor D \\ C ::= D \quad | \quad D \land C L::=p∣¬pD::=L∣L∨DC::=D∣D∧C

如果 ϕ \phi ϕ 是 CNF，有一个非常容易快速判断 ⊨ ϕ \models \phi ⊨ϕ 有效性的方法：检查 ϕ \phi ϕ 的所有合取 ψ k \psi_k ψk ，寻找 ψ k \psi_k ψk 中是否有这样的原子，即它们的否定也在 ψ k \psi_k ψk 中。如果所有的析取都能找到这样的匹配，那么有 ⊨ ψ \models \psi ⊨ψ 。

可满足：已知一个命题逻辑公式 ϕ \phi ϕ ，如果有一个赋值使它的赋值为 T，那么称 ϕ \phi ϕ 是可满足的。

命题逻辑 ϕ \phi ϕ 是可满足的，当且仅当 ¬ ϕ \neg \phi ¬ϕ 不是有效的。

否定范式(negation normal form, NNF)：只否定原子的公式。

CNF算法：对于一个已知输入 ϕ \phi ϕ ，总能输出等价的CNF

一个算法称为 CNF ，满足的要求：
1. 对于所有输入的命题逻辑公式，CNF 可以终止；
2. 对于每一个输入的命题逻辑公式，CNF 输出一个等价公式；
3. 所有由 CNF 计算的输出都是 CNF 形式的；
流程：
1. 先进行蕴含释放：将 ψ → η \psi \rightarrow \eta ψ→η 的蕴含用 ¬ ψ ∨ η \neg \psi \lor \eta ¬ψ∨η 代替；
2. 转换为否定范式；
3. 分析情况：
  - 如果 ψ \psi ψ 是一个文字，由 CNF 的定义，CNF 输出 ψ \psi ψ ；
  - 如果 ϕ = ϕ 1 ∧ ϕ 2 \phi = \phi_1 \land \phi_2 ϕ=ϕ1∧ϕ2 ，对每个 ϕ i \phi_i ϕi ，循环地调用 CNF ，分别得到输出 η i \eta_i ηi ，最后得到输入 ϕ \phi ϕ 作为 CNF 地输出 η i ∧ η 2 \eta_i \land \eta_2 ηi∧η2 ；
  - 如果 ϕ = ϕ 1 ∨ ϕ 2 \phi = \phi_1 \lor \phi_2 ϕ=ϕ1∨ϕ2 ，对每个 ϕ i \phi_i ϕi ，循环地调用 CNF ，分别得到输出 η i \eta_i ηi ，使用分配率，将合取的析取转换为析取的合取；

伪代码：

function CNF(φ):
/* 前置条件： φ是蕴含释放，并且是NNF模式 */
/* 后置条件： CNF(φ) 计算 ψ 的等价 */
begin functioncaseφ 是文字: return φφ 是 φ1 and φ2: return CNF(φ1) and CNF(φ2)φ 是 φ1 or φ2: return DISTR(CNF(φ1), CNF(φ2))end case
end functionfunction NNF
/* 前置条件： φ 是无蕴含的 */
/* 后置条件： NNF(φ) 计算 φ 的 NNF */
begin functioncaseφ 是 一个文字 : φφ 是 not not φ1 : return NNF(φ1)φ 是 φ1 and φ2 : return NNF(φ1) and NNF(φ2)φ 是 φ1 or φ2 : return NNF(φ1) or NNF(φ2)φ 是 not(φ1 and φ2) : return NNF(not φ1) or NNF(not φ2)φ 是 not(φ1 or φ2) : return NNF(not φ1) and NNF(not φ2)end case
end functionfunction DISTR
/* 前置条件： ŋ1 和 ŋ2 是 CNF 形式 */
/* 后置条件： DIST(ŋ1, ŋ2)，计算 ŋ1 or ŋ2 的 CNF */
begin functioncaseŋ1 是 ŋ11 and ŋ12 : return DISTR(ŋ11, ŋ2) and DISTR(ŋ12, ŋ2)ŋ2 是 ŋ21 and ŋ22 : return DISTR(ŋ1 or ŋ21) and DISTR(ŋ1 or ŋ22)否则(=没有合取) : return ŋ1 or ŋ2end case
end function

霍恩公式：逻辑公式 ϕ \phi ϕ ，如果它可以用下列语法作为 H H H 的实例产生：
P : : = ⊥ ( 不可满足的公式 ) ∣ ⊤ ( 重言式 ) ∣ p A : : = P ∣ P ∧ A C : : = A → P H : : = C ∣ C ∧ H P ::= \bot (不可满足的公式) \quad | \quad \top(重言式) \quad | \quad p \\ A ::= P \quad | \quad P \land A \\ C ::= A \rightarrow P \\ H ::= C \quad | \quad C \land H P::=⊥(不可满足的公式)∣⊤(重言式)∣pA::=P∣P∧AC::=A→PH::=C∣C∧H
C 的每一个实例称为霍恩子句。

判断一个霍恩公式 ϕ \phi ϕ 可满足性算法：

如果它出现在 ϕ \phi ϕ 中，标记为 ⊤ \top ⊤ ；
如果 ϕ \phi ϕ 的合取 P 1 ∧ P 2 ∧ ⋯ ∧ P k i → P ′ P_1 \land P_2 \land \cdots \land P_{k_i} \rightarrow P' P1∧P2∧⋯∧Pki→P′ 中所有 P j ( 1 ≤ j ≤ k i ) P_j(1 \le j \le k_i) Pj(1≤j≤ki) 都被标记，那么标记 P ′ P' P′ ，重复2。否则（=没有合取 P 1 ∧ P 2 ∧ ⋯ ∧ P k i → P ′ P_1 \land P_2 \land \cdots \land P_{k_i} \rightarrow P' P1∧P2∧⋯∧Pki→P′ 中所有 P j ( 1 ≤ j ≤ k i ) P_j(1 \le j \le k_i) Pj(1≤j≤ki) 都被标记），继续3；
如果 ⊥ \bot ⊥ 被标记，输出”霍恩公式 ϕ \phi ϕ 不是可满足的“，停止。否则，继续4；
输出”霍恩公式 ϕ \phi ϕ 是可满足的“，停止。

1.6 SAT 求解机

线性求解机：

把公式翻译为合适的片段： ϕ : : = p ∣ ( ¬ ϕ ) ∣ ( ϕ ∧ ϕ ) \phi ::= p \quad | \quad (\neg \phi) \quad | \quad (\phi \land \phi) ϕ::=p∣(¬ϕ)∣(ϕ∧ϕ)

然后共享语法分析树的共同子式，使树成为一个有向无环图(Directed acyclic graph, DGA)。

递归地定义这种转换：
T ( p ) = p T ( ¬ ϕ ) = ¬ T ( ϕ ) T ( ϕ 1 ∧ ϕ 2 ) = T ( ϕ 1 ) ∧ T ( ϕ 2 ) T ( ϕ 1 ∨ ϕ 2 ) = ¬ ( ¬ T ( ϕ 1 ) ∧ ¬ T ( ϕ 2 ) T ( ϕ 1 → ϕ 2 ) = ¬ ( T ( ϕ 1 ) ∧ ¬ T ( ϕ 2 ) ) T(p) = p \quad \quad T(\neg \phi) = \neg T(\phi) \\ T(\phi_1 \land \phi_2) = T(\phi_1) \land T(\phi_2) \quad \quad T(\phi_1 \lor \phi_2) = \neg (\neg T(\phi_1) \land \neg T(\phi_2) \\ T(\phi_1 \rightarrow \phi_2) = \neg( T(\phi_1) \land \neg T(\phi_2)) T(p)=pT(¬ϕ)=¬T(ϕ)T(ϕ1∧ϕ2)=T(ϕ1)∧T(ϕ2)T(ϕ1∨ϕ2)=¬(¬T(ϕ1)∧¬T(ϕ2)T(ϕ1→ϕ2)=¬(T(ϕ1)∧¬T(ϕ2))
ϕ \phi ϕ 是可满足的，当且仅当 T ( ϕ ) T(\phi) T(ϕ) 是可满足的；使 ϕ \phi ϕ 为真的赋值集合等于使 T ( ϕ ) T(\phi) T(ϕ) 为真的赋值集合。

线性 SAT 求解机的运行时间关于 T ( ϕ ) T(\phi) T(ϕ) 的 DAG 大小是线性的。

线性 SAT 求解机对形如 ¬ ( ϕ 1 ∧ ϕ 2 ) \neg (\phi_1 \land \phi_2) ¬(ϕ1∧ϕ2) 的所有公式都失效。

三次求解机：

对于没有标记的节点，分别做两个独立的计算来检验该节点：

只对该节点增加 T 标记来确定哪些临时标记是被强制的；
只对该节点增加 F 标记来确定哪些临时标记是被强制的。

如果两种运算都得到矛盾约束，那么算法停止，报告 T ( ϕ ) T(\phi) T(ϕ) 是不可满足的；否则对两种运算都得到同样标记的所有节点接受相同的标记作为永久标记。

用同样的方法进一步检验未标记的节点，直到发现矛盾的永久标记节点；或检测了所有目前尚未标记的节点而没有发现任何共享的标记，报告这些标记作为可满足性的一个证据，终止算法。

三次求解机的运行时间是关于 T ( ϕ ) T(\phi) T(ϕ) 的 DAG 大小的立方。

【面向计算机科学的数理逻辑系统建模与推理笔记】命题逻辑相关推荐

【学习笔记】面向计算机科学的数理逻辑：系统建模与推理 (C1命题逻辑)
Content Chapter 1 命题逻辑逻辑符号证明规则作为形式语言的命题逻辑命题逻辑的语义范式 SAT求解机 Chapter 1 命题逻辑逻辑符号 negation: ¬ p \ne ...
计算机科学与数理逻辑答案,面向计算机科学的数理逻辑答案
2.2.2 若A∈Atom(L p),则n=0,m=1,m = n+1成立. 若B.C∈Form(L p),B中出现∧,∨,→, 的次数为n1次,出现原子公式的次数为m1次,m1= n1+1,C中出现 ...
【面向计算机的数理逻辑/软件理论基础笔记】一阶谓词逻辑系统的证明理论，包含演绎定理、可证等价关系和完备性定理
一阶形式系统KLK_\mathcal{L}KL 一阶形式系统KLK_\mathcal{L}KL是指由一阶语言L\mathcal{L}L以及下面的公理和推理规则组成: 公理集: (K1):A→(B→ ...
TensorRT C++ 批量推理笔记
batch为1时,如下: void* buffers[2]; buffers[inputIndex] = inputbuffer; buffers[outputIndex] = outputBuffe ...
学习Simulink（主要面向电力电子和电力系统分析）笔记（长期更新）
电力电子(弱电)和电力系统的分析(强电)的仿真是离不开Matlab中的Simulink,这里来记录一下学习的进程电气专业Simulink学习笔记一.打开Simulink 二.打开库进行元件选择二 ...
DR-CAN的动态系统建模与分析学习笔记（3）拉普拉斯变换的收敛域(ROC)与逆变换(ILT)
1.是否可积即是否收敛(如果可收敛,面积/拉氏值即为收敛域) (1)收敛的条件:e^(-jwt)积分为振荡函数 (2)常系数线性微分方程对应线性时不变系统,其分析步骤有三: (3)拉氏逆变换(ILT) ...
通信系统建模与仿真笔记2
转载请注明出处 simulink 建立系统模型:输入两个不同频率.振幅的正.余弦信号,输出它们的和看图 1.启动simulink 2.选择模块sine wave(2个).add.scope 选择两个 ...
面向交易的日内高频量化交易平台笔记
1. 本次讲座介绍. 长江证券金融工程部邀请了北京知象科技创始人,对其量化交易系统(股票.期货)进行了简单的介绍以及推广. 2.本次讲座主要设计的内容. 针对股票日内高频量化交易平台.本次讲座只cov ...
离散数学复习笔记——命题逻辑——永真蕴含式

【面向计算机科学的数理逻辑系统建模与推理笔记】命题逻辑

第一章命题逻辑

文章目录

1.1 判断语句

1.2 自然演绎

1.3 作为形式语言的命题逻辑

1.4 命题逻辑的语义

1.5 范式

1.6 SAT 求解机

【面向计算机科学的数理逻辑系统建模与推理笔记】命题逻辑相关推荐

最新文章

热门文章

【面向计算机科学的数理逻辑 系统建模与推理 笔记】命题逻辑

第一章 命题逻辑

文章目录

1.1 判断语句

1.2 自然演绎

1.3 作为形式语言的命题逻辑

1.4 命题逻辑的语义

1.5 范式

1.6 SAT 求解机

【面向计算机科学的数理逻辑 系统建模与推理 笔记】命题逻辑相关推荐

最新文章

热门文章

【面向计算机科学的数理逻辑系统建模与推理笔记】命题逻辑

第一章命题逻辑

【面向计算机科学的数理逻辑系统建模与推理笔记】命题逻辑相关推荐