命题语言Lp表达式公式集的归纳定义公式集的归纳定义公式集的归纳证明公式结构公式的语法分类辖域形式可推演命题逻辑的推演规则形式推演的定义∈规则例子Tr规则证明：A→B，B→C├A→C。证明：A→(B→C)，A→B├A→C。证明：﹁﹁A├A(﹁+)归谬律证明：A├﹁﹁A语义例子公式的语义分类逻辑推论证明：A→B，B→C╞A→C。证(1)：对于任何真假赋值v，若{A→B，B→C}v=1。可得，(A→B)v=1(i)，(B→C)v=1(ii)。若Av=1，则由(i)可得，Bv=1。再由(ii)可得，Cv=1。所以，(A→C)v=1。若Av=0，则(A→C)v=1。证明：A→B，B→C╞A→C。证(2)：设任何真假赋值v，若(A→C)v=0可得，Av=1(i)，Cv=0(ii)。若Bv=1，则由(ii)可得，(B→C)v=0。所以，{A→B，B→C}v=0。若Bv=0，则由(ii)可得，(A→B)v=0。所以，{A→B，B→C}v=0。定理范式例子翻译p：张平盗窃了机房的计算机一台。q：王磊盗窃了机房的计算机一台。r：作案时间发生在午夜之前。s：王磊的证词正确。t：午夜时机房的灯光灭了。p∨q，p→¬r，s→¬t，¬s→r，t├？(1)p，¬q├p(∈)(2)q，¬q，¬p├¬q(∈)(3)q，¬q，¬p├q(∈)(4)q，¬q├p(¬-)(2)(3)(5)p∨q，¬q├p(∨-)(1)(4)(6)p∨q，¬q，p→¬r├p(+)(5)(7)p∨q，¬q，p→¬r├p→¬r(∈)(8)p∨q，¬q，p→¬r├¬r(→-)(6)(7)(9)s→¬t，¬s→r，s，t├s(∈)(10)s→¬t，¬s→r，s，t├s→¬t(∈)(11)s→¬t，¬s→r，s，t├¬t(→-)(9)(10)(12)s→¬t，¬s→r，s，t├t(∈)(13)s→¬t，¬s→r，t├¬s(¬+)(11)(12)(14)s→¬t，¬s→r，t├¬s→r(∈)(15)s→¬t，¬s→r，t├r(→-)(13)(14)(16)p∨q，p→¬r，s→¬t，¬s→r，t，¬q├¬r(+)(8)(17)p∨q，p→¬r，s→¬t，¬s→r，t，¬q├r(+)(15)(18)p∨q，p→¬r，s→¬t，¬s→r，t├q(¬-)(16)(17)