袁夢霆，李清安，吳黎兵，何炎祥

（武漢大學(xué)計(jì)算機(jī)學(xué)院，湖北 武漢 430072）

0 引言

邏輯學(xué)的研究內(nèi)容涉及問題的形式化與推理，是計(jì)算機(jī)科學(xué)中的重要理論課程[1]。命題邏輯以命題為基礎(chǔ)研究形式化與推理方法，一般是邏輯學(xué)課程的入門章節(jié)。對(duì)很多學(xué)生而言，學(xué)習(xí)命題邏輯是他們第一次接觸形式化方法，再加上命題邏輯具有高度的抽象性，因此在學(xué)習(xí)過程中存在很多困難。如何激發(fā)學(xué)生對(duì)命題邏輯的學(xué)習(xí)熱情，進(jìn)而引導(dǎo)學(xué)生喜歡邏輯學(xué)與形式化方法，這是我們在邏輯學(xué)教學(xué)過程中需要解決的重要問題。

對(duì)于高度抽象的教學(xué)內(nèi)容，合適的教學(xué)方法是教學(xué)成功的關(guān)鍵因素之一。由于命題邏輯非常抽象，在課本或者以往的相關(guān)教學(xué)研究[2-4]中往往比較重視定義、定理、命題和性質(zhì)的講解，選擇的案例也是和日常生活相關(guān)的推理案例，比較偏向于數(shù)理邏輯。學(xué)生學(xué)習(xí)以后往往感覺到命題邏輯和計(jì)算機(jī)沒有相關(guān)性，只能死記硬背定理，無法和計(jì)算機(jī)領(lǐng)域的問題關(guān)聯(lián)，很難提高興趣。

針對(duì)在傳統(tǒng)命題邏輯教學(xué)過程中存在的問題，本文提出了基于建模與推理的命題邏輯教學(xué)方法，面向計(jì)算機(jī)專業(yè)的學(xué)生，緊密圍繞命題邏輯的建模與推理內(nèi)容展開教學(xué)內(nèi)容，突出命題邏輯在計(jì)算機(jī)科學(xué)中的作用，提高計(jì)算機(jī)專業(yè)學(xué)生的學(xué)習(xí)效果。

1 側(cè)重建模與推理的教學(xué)方法

為了達(dá)到良好的命題邏輯的教學(xué)效果，在講述完命題邏輯的語法和語義之后，設(shè)計(jì)一組與計(jì)算機(jī)科學(xué)緊密相關(guān)的實(shí)例，然后向?qū)W生講述建模的目標(biāo)，引導(dǎo)學(xué)生對(duì)問題進(jìn)行形式化建模，教導(dǎo)學(xué)生使用課堂講述的自然推理法對(duì)模型的性質(zhì)進(jìn)行推理，最后總結(jié)與討論建模與推理過程中碰到的問題。

1.1 案例選擇

由于命題邏輯的語法非常簡單，因此教師需要挑選一些不復(fù)雜但是又能代表計(jì)算機(jī)實(shí)際應(yīng)用的案例。案例的設(shè)計(jì)應(yīng)該考慮到覆蓋命題邏輯的理論知識(shí)點(diǎn)，同時(shí)需要估算教學(xué)與實(shí)踐的工作量，每個(gè)案例的設(shè)計(jì)按照3個(gè)學(xué)時(shí)的長度設(shè)計(jì)，使得學(xué)生能夠在聽完命題邏輯的理論課程后，快速通過實(shí)例掌握命題邏輯的建模與推理知識(shí)。

1.2 講述建模目標(biāo)

對(duì)于選定的建模實(shí)例，教師首先利用自然語言，撰寫案例的文檔，在課堂上將文檔下發(fā)給每位學(xué)生。教師先講述該實(shí)例的應(yīng)用背景，闡述如何將實(shí)際的計(jì)算機(jī)應(yīng)用簡化為該實(shí)例。接下來教師講述該案例的功能與需求，講述系統(tǒng)必須具備的性質(zhì)。通過學(xué)生的提問與討論，保證學(xué)生對(duì)該系統(tǒng)具有完整與形象的了解。

1.3 形式化建模

在學(xué)生對(duì)案例有了足夠的了解后，教師引導(dǎo)學(xué)生用命題邏輯的語法對(duì)系統(tǒng)進(jìn)行重新描述，也就是形式化。在建模過程中，引導(dǎo)學(xué)生識(shí)別系統(tǒng)中的聲明式語句與命題，體會(huì)如何使用邏輯公式描述系統(tǒng)規(guī)律。鼓勵(lì)學(xué)生對(duì)建模過程進(jìn)行開放式的討論，對(duì)不同的模型進(jìn)行對(duì)比，體會(huì)形式化過程中的優(yōu)雅、簡練、準(zhǔn)確等特點(diǎn)。

在學(xué)生完成自己的建模工作后，教師公布參考的模型，然后與學(xué)生討論建模過程中的心得，使得學(xué)生掌握基本的命題邏輯建模技巧。

1.4 性質(zhì)推理

對(duì)于已經(jīng)建好的模型，教師帶領(lǐng)學(xué)生回顧案例的文檔，列舉出模型應(yīng)該具有的性質(zhì)，并將這些性質(zhì)用命題邏輯公式描述出來，然后向?qū)W生提出問題：“如何嚴(yán)格證明模型具備這些性質(zhì)？”在學(xué)生思考與討論后，教師回顧課堂的“命題邏輯的語義”和“自然推演法”兩種性質(zhì)推理方法，讓學(xué)生自行選擇方法進(jìn)行推理。通過性質(zhì)推理，引導(dǎo)學(xué)生掌握基于語義和基于規(guī)則的兩種推理方法，能夠體會(huì)到兩種方法各自的特點(diǎn)。

1.5 總結(jié)與討論

在總結(jié)階段，教師客觀地對(duì)一些有代表性的學(xué)生模型進(jìn)行點(diǎn)評(píng)，回顧建模與推理的特點(diǎn)與難點(diǎn)，同時(shí)對(duì)照命題邏輯的主要知識(shí)點(diǎn)進(jìn)行復(fù)習(xí)，加強(qiáng)學(xué)生的學(xué)習(xí)效果。

最后組織學(xué)生討論命題邏輯建模方法的缺點(diǎn)與限制，自然而然地引出下一章謂詞邏輯的內(nèi)容，激發(fā)學(xué)生的好奇心與學(xué)習(xí)興趣。

2 教學(xué)方法應(yīng)用

這里從一個(gè)案例出發(fā)，介紹如何開展以建模與推理為目的的命題邏輯教學(xué)方法。

2.1 案例描述

使用一個(gè)兩位（2-bit）二進(jìn)制數(shù)的加法器作為案例，該實(shí)例在計(jì)算機(jī)科學(xué)中具有普遍的代表意義，同時(shí)模型不復(fù)雜，便于學(xué)生短時(shí)間理解，使用命題邏輯就足夠進(jìn)行建模與推理。

使用圖1對(duì)學(xué)生講述加法器，該加法器能夠?qū)1x0和y1y0兩個(gè)二進(jìn)制數(shù)相加，輸出兩個(gè)數(shù)相加的結(jié)果，放在z1z0中，高位的進(jìn)位被舍棄。在計(jì)算過程中，x0和y0相加的結(jié)果會(huì)產(chǎn)生進(jìn)位c，供x1和y1相加時(shí)使用。

圖1 二進(jìn)制加法器原理，其中z1z0=x1x0+y1y0

2.2 加法器的形式化建模

命題邏輯的建模過程分為兩個(gè)步驟：（1）確定原子命題的集合；（2）使用一組命題邏輯公式描述系統(tǒng)的內(nèi)在規(guī)律。

在本例中，我們令原子命題集合A={x0,x1,y0,y1,z0,z1,c}，其中一個(gè)原子命題a∈A成立表示變量a的值為1，否則為0。

而系統(tǒng)的內(nèi)在規(guī)律可以用一組邏輯公式表示：P={p0,p1,…,p9}，其中p0≡(x0∧y0→c)∧(?x0?y0→?c),p1≡(z0→((x0∧?y0)(?x0∧y0)))∧(?z0→((x0∧y0)(?x0∧?y0))),p2≡c∧x1∧y1→z1,p3≡c∧x1∧?y1→?z1,p4≡c∧?x1∧y1→?z1,p5≡c∧?x1∧?y1→z1,p6≡?c∧x1∧y1→?z1,p7≡?c∧x1∧?y1→z1,p8≡?c∧?x1∧y1→z1,p9≡?c∧?x1∧?y1→?z1。

在建模的過程中，我們和學(xué)生討論如何在此基礎(chǔ)上簡化帶進(jìn)位加法的性質(zhì)描述。

2.3 加法器的性質(zhì)推理

在學(xué)生理解加法器模型之后，我們引導(dǎo)學(xué)生驗(yàn)證模型的性質(zhì)。在本例中，我們假設(shè)要驗(yàn)證01+10=11。首先，我們引導(dǎo)學(xué)生對(duì)這個(gè)性質(zhì)進(jìn)行形式化，也就是用命題邏輯的sequent來表示該性質(zhì)：P,x0,?x1,?y0,y1z0∧z1。然后鼓勵(lì)學(xué)生采用自然推演法來證明該sequent是有效的。

該性質(zhì)的自然推演法證明過程如下（限于篇幅，該證明過程中合并了一些顯而易見的小過程）：

講解推理過程，幫助學(xué)生體會(huì)推理過程的嚴(yán)謹(jǐn)性，了解自然推演法的使用技巧，進(jìn)而靈活運(yùn)用自然推演法。

2.4 討論

在與學(xué)生討論的過程中，我們主要注意引導(dǎo)學(xué)生對(duì)以下內(nèi)容的思考：（1）命題邏輯的語法非常簡單，所以導(dǎo)致了模型性質(zhì)描述很繁冗，問學(xué)生有什么方法可以增加命題邏輯的建模復(fù)雜度。提示學(xué)生考慮在命題邏輯的基礎(chǔ)上利用恒等式擴(kuò)充語法。（2）在本例中，我們只證明了系統(tǒng)滿足01+10=11一個(gè)特定的性質(zhì)，可以引導(dǎo)學(xué)生思考如何推理所有二進(jìn)制數(shù)加法的性質(zhì)，進(jìn)而引出謂詞的概念，從而將學(xué)生引入下一章的謂詞邏輯的話題，激發(fā)學(xué)生對(duì)課堂新任務(wù)的期待與熱情。

3 結(jié)語

實(shí)踐表明，針對(duì)計(jì)算機(jī)科學(xué)相關(guān)的實(shí)例，利用命題邏輯對(duì)其進(jìn)行建模與性質(zhì)推理，能夠幫助學(xué)生更扎實(shí)地掌握命題邏輯的知識(shí)點(diǎn)，并且直觀的了解形式化的過程與技巧，充分調(diào)動(dòng)了學(xué)生對(duì)邏輯學(xué)的學(xué)習(xí)興趣，同時(shí)讓學(xué)生不再懼怕抽象的邏輯概念，能夠理論聯(lián)系實(shí)際，有利于后續(xù)章節(jié)的學(xué)習(xí)。