软件理论基础—— 第一章命题逻辑系统L

逻辑

语法

语义

推理系统

公理

推理规则

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规则

上一篇:apache开源项目-- Usergrid


下一篇:在有大量数据时 少用In(数据会丢失) 用left join 代替