逻辑
语法
语义
推理系统
公理
推理规则
MP A,A->B =>B
HS A->B,B->C => A->C
命题逻辑公式
：：= BNF backus naur form 巴科斯范式 用于表示上下文无关文法的语言 规定的是推导规则(产生式)的集合
：= 定义
真值指派
原子命题指派
复合命题计算出来 ~ ∧∨ →
赋值 v(……)
~ ∧∨ → 在左边是逻辑上的运算，在右边是一元或二元运算
同态映射
真度（考点设计真度为5/16的逻辑公式）
重言式与矛盾式
|=A A是重言式
|-A A是定理
等价 ≡
逻辑等价= A ∨ B = ￢A → B, A → B = ￢(A ∧ ￢B)
充足集{~，->}{~,∨}{~,∧} {↓}
范式
合取范式，找到值为false的原子命题取值，令原子命题取值为假，先析取再合取，重言式无合取范式，如A∨(~A)
析取范式，找到值为true的原子命题取值，令原子命题取值为真，先合取再析取，矛盾式无析取范式，如A∧(~A)
证明重言式方法：真值表
证明逻辑等价方法：
求真度方法：
定理判定方法：真值表，推理方法存在MIU问题（不能在有限步骤内判断是否是定理）
命题逻辑形式系统L
公理
L1:A->(B->A)
L2:(A->(B->C))->((A->B)->(A->C))
L3: (~A->~B)->(B->A)
推理规则 ： MP规则（分离规则）
A,A->B
-----------
B
L中的证明与定理
|-（p1->p2）->(p1->p1)
假设存在A，使得A -> [（p1->p2）->(p1->p1)],找到这个A，即证明
A=p1->(p2-p1) L1
(p1->(p1->p2)) ->(p1->p1)->(P1->p2) L2 (A->(B->C))->((A->B)->(A->C))
(p1->p1)->(P1->p2)) MP A,A->B =>B
|-(A->A)
假设存在B，使得B -> (A->A),找到这个B，即证明A->A
(1)A->(A->A) L1
(2)A->((A->A)->A) L1???
(3)A → ((A → A) → A) → (A → (A → A)) → (A → A)) L2
A->A MP规则