邏輯推論與專家系統
布林邏輯與公理系統
想要理解甚麼是數學,最快速的捷徑是從公理系統下手,因為公理系統是數學證明的核心,理解了公理系統之後,就可以看懂數學家到底在玩甚麼遊戲了!
但是、很多數學的公理系統太過複雜,因此很難解釋,讀者往往在還沒入門之前,就已經先恍神了,所以為了讓大家很容易的理解公理系統,我們選擇了一個最簡單的數學體系,那就是布林邏輯。
布林邏輯只有兩個值,那就是 0 與 1 ,所以可以說是最簡單的數學體系了,就讓我們從布林邏輯開始,理解何謂公理系統吧!
何謂嚴格的數學證明?
當我還是個學生時,我總是困惑著如何應付老師的考試,其中一個重要的數學困擾是,老師要我們「證明」某個運算式。
最大的問題不在於我不會「證明」,因為在很多科目的證明題當中,我也都「答對了」,但是這種答對總是讓我感到極度的沒有把握,因為有時老師說「這樣的證明是對的」,但有時卻說「這樣的證明是錯的」。
更神奇的是,老師的證明永遠都是對的,他們可以突然加入一個「推論」,而這個推論的根據好像之前沒有出現過,然後他們說:「由此可證」、「同理可證」….。
直到有一天,我終於懂了。
因為課堂上老師的證明往往不是「嚴格的證明」,因為嚴格的證明通常「非常的困難」,每個證明都可以是一篇論文,甚至在很多論文當中的證明也都不是嚴格的。
所以在課堂上,老師總是可以天外飛來一筆的,跳過了某些「無聊的步驟」,奇蹟式的證明了某些定理,而這正是我所以感到困擾的原因。
一般的證明
一般而言,日常生活中的證明,通常是不嚴格的。
舉例來說,我可以「證明」某人殺了死者,因為殺死死者的兇刀上有「某人」的指紋。
但是這樣的證明並不嚴格,因為有很少的可能性是「某人摸過兇刀、但是並沒有殺人」。
所以我們總是可以看到那個「外表看似小孩,智慧卻過於常人」的「名偵探柯南」,總是天外飛來一筆的「證明」了某人是兇手,這種證明與數學證明可是完全不同的。
嚴格的證明
數學的證明通常不能是「機率式」的,例如:「我證明他 99% 殺了人」,這樣的證明稱不上是嚴格的證明。
嚴格的證明也並非結果一定要是 100% 的正確 (當然也不是說結果不正確),真正的證明是一種過程,而不是結果。
怎麼說呢?
數學其實很像程式領域的演算法,或者就像是電腦的運作過程,當我們設計出一顆 CPU 之後,你必須用該 CPU 的指令撰寫出某些函數,以便完成某個程式。
那麼,數學的 CPU 是甚麼呢?
答案是「公理系統」 (Axioms)!
只有透過公理系統,經由某種演算方式,計算出待證明定理在任何情況下都是真的,這樣才算是證明了該定理。
這些公理系統其實就是數學的 CPU 指令集。
布林代數大概是數學當中最簡單的系統了,因為布林代數的値只有兩種–「真與假」 (或者用 0 與 1 代表)。
為了說明嚴格的數學證明是如何進行的,我們將從布林代數的公理系統 (CPU?) 開始,說明如何證明布林代數的某些定理,就好像是如何用指令集撰寫程式一樣。
布林邏輯
對於單一變數 x 的布林系統而言,x 只有兩個可能的值 (0 或 1)。
對於兩個變數 x, y 的布林系統而言,(x, y) 的組合則可能有 (0,0), (0,1), (1,0), (1,1) 四種。
對於三個變數 x, y, z 的布林系統而言,(x, y, z) 的組合則可能有 (0,0, 0), (0,0,1), (0,1,0), (0,1,1), (1,0, 0), (1,0,1), (1,1,0), (1,1,1) 八種。
基本的布林邏輯運算有三種,AND (且), OR (或), NOT (反),在布林代數當中,通常我們在符號上面加一個上標橫線代表 NOT,用 $\wedge
$ 代表 AND,用 $\vee
$ 代表 OR。
但是在程式裏面,受到 C 語言的影響,很多語言用驚嘆號 !
代表 NOT,用 &
代表 AND,用 |
代表 OR。
我們以下將採用NOT,用 &
代表 AND,用 |
代表 OR,但是卻用負號 -
代表 not,來解說公理系統的作用。
假如我們想知到某個邏輯式的真值表,例如 (-x | y) 的真值表,只要透過列舉的程序就可以檢查完畢。
x | y | -x | -x|y |
---|---|---|---|
0 | 0 | 1 | 1 |
0 | 1 | 1 | 1 |
1 | 0 | 0 | 0 |
1 | 1 | 0 | 1 |
接著,我們就可以定義一些公理系統,這些「公理系統」就像是數學推理的指令集,讓我們可以推論出哪些邏輯式在這個公理系統下是真的 (定理),哪些邏輯式這個公理系統下不一定是真的。
知識庫推理系統
舉例而言,假如我們制定了一個公理系統如下所示。
公理 1: -A | B
公理 2: -B | C
公理 3: A
當我們制定完公理系統之後,這些公理就無條件地成立了,而且每一條都成立。
換句話說,上述系統裏的 (-A | B) & (-B | C) & A 這個陳述是成立的。
讓我們列出上述系統的真值表,看看這樣的公理系統代表甚麼意義?
A | B | C | -A|B | -B|C |
---|---|---|---|---|
0 | 0 | 0 | 1 | 1 |
0 | 0 | 1 | 1 | 1 |
0 | 1 | 0 | 1 | 0 |
0 | 1 | 1 | 1 | 1 |
1 | 0 | 0 | 0 | 1 |
1 | 0 | 1 | 0 | 1 |
1 | 1 | 0 | 1 | 0 |
1 | 1 | 1 | 1 | 1 |
在上述真值表中,那些不符合公理者都可以先刪除,這樣我們就得到下列的《剩餘真值表》。
A | B | C | -A|B | -B|C |
---|---|---|---|---|
1 | 1 | 1 | 1 | 1 |
結果只剩下一個可能性,也就是 A=1, B=1, C=1 。
但是在上述公理系統中,我們並沒有《規定 A=1, B=1, C=1 》,而是規定了 (-A | B)=1, (-B | C)=1, A=1 這三條公理。
但那三條公理,導出來的結果,其實就是 A=1, B=1, C=1。換句話說, B=1, C=1 在這個公理系統下,都是定理。
上述的那個系統,比較不像《數學系統》,而是一個《知識庫系統》,我們可以透過《知識庫》裏的《事實陳述》,用《真值表》的方式,刪除《不符合事實》的項目,然後在留下的世界裏尋找《符合該世界體系,卻又沒有直接說出來的事實》,這種過程基本上就是一種推理。
布林邏輯的公理系統
在布林邏輯裏,其實就隱含了一組公理系統,這個公理系統其實就是 AND, OR, NOT 的真值表定義,也就是下列的三個表格。
x | -x |
---|---|
0 | 1 |
1 | 0 |
x | y | x&y |
---|---|---|
0 | 0 | 0 |
0 | 1 | 0 |
1 | 0 | 0 |
1 | 1 | 1 |
x | y | x|y |
---|---|---|
0 | 0 | 0 |
0 | 1 | 1 |
1 | 0 | 1 |
1 | 1 | 1 |
根據 AND, OR, NOT 三個表格,我們可以建構出一些定理,舉例而言,在布林邏輯裏很有用的《迪摩根定理》就可以用真值表檢核如下:
x | y | -(x|y) | -x&-y | -(x&y) | -x|-y |
---|---|---|---|---|---|
0 | 0 | 1 | 1 | 0 | 0 |
0 | 1 | 0 | 0 | 0 | 0 |
1 | 0 | 0 | 0 | 0 | 0 |
1 | 1 | 0 | 0 | 1 | 1 |
您可以發現 -(x|y) 和 -x&-y 兩者的真值是一樣的,-(x&y) 與 (-x|-y) 兩者的真值也是一樣的。
因此、我們得到下列兩個定理:
- -(x| y) = -x & -y
- -(x & y) = -x|-y
這就是所謂的《迪摩根定理》(De Morgan’s laws)。
推論法則
但是、上述的定理是用《列舉真值表》的方式得到的,這種方式不太有效率,因為對於 n 個變數的世界而言,真值表會有 $2^n
$ 列 (在 n 比較大的時候,這真的會非常巨大,萬一有無窮多個變數,那麼根本就列不完了)。
問題是、如果不用真值表,那麼還有甚麼方法可以《找出定理》呢?
答案當然是有的、那就是用《推論法則》!
肯定前項 (Modus Poens)
舉例而言,以下是布林邏輯的一組推論法則。
前提 1: -p | q
前提 2: p
-------------------
結論: q
各位心裡應該不免納悶,為何這樣的推論法則成立呢?
其實這樣的法則,一樣是從《真值表》得來的!
我們就可以列出上述推論法則中,前提與結論的真值表如下:
p | q | -p|q |
---|---|---|
0 | 0 | 1 |
0 | 1 | 1 |
1 | 0 | 0 |
1 | 1 | 1 |
在上述真值表中,凡是無法滿足前提的列,就代表該項目違反前提,可以被刪除 (不符合前提):
在上述表格中,前兩條的 p 為 0,因此不滿足前提 2,而第三條的 -p|q
為 0,不滿足前提 1,因此符合前提的項目就只剩下了一個如下。
p | q | -p|q |
---|---|---|
1 | 1 | 1 |
在這個滿足公理系統的真值表當中,我們可以看到 q
只能是 1,也就是 q
在那兩個前提下必然為真,也就是 q 其實是該前提下的必然結論。
換句話說、從 p & (-p | q) 可以推論出 q。
如果我們把 -p|q
簡寫為 p → q
,則上述推論法則可以改寫如下,這樣的推論法則稱為 Modus Ponus (中文翻成「肯定前件」)。
前提 1: p → q
前提 2: p
------------------
結論: q
於是我們可以得到下列《代換式》,這種代換式就是一組推論法則。
p ; p → q
-----------
q
以上這組推論法則,稱為 Modus ponens ,中文可以稱為《肯定前項》!
有了上述推論法則後,我們就可以進行知識推理了,讓我們看看前面知識庫的例子。
公理 1: -A | B
公理 2: -B | C
公理 3: A
由於 -p|q
被簡寫為 p → q
,所以上述《公理》改寫如下:
公理 1: A → B
公理 2: B → C
公理 3: A
於是我們可以開始利用剛剛得到的推論法則,也就是下列這組代換式進行推理。
p ; p → q
-----------
q
如果把 p 代換為 A, q 代換為 B,那麼會得到
A ; A → B
-----------
B
也就是從《公理1》 和《公理3》可以推出 B,因此 B 在這個系統下是真的,換句話說就是定理。
同樣的我們可以從《定理》 B 與《公理 1》繼續套用推論法則,於是得到 C 也是該系統下的真理 (事實)。
B ; B → C
-----------
C
否定後項 (Modus Tollens)
當然、布林邏輯的推理法則不只《肯定前項》一種,您還可以想出很多種推理法則。
另一種正確的推理法則,是採用《否定後項》的方式,其形式如下:
p → q ; -q
-----------
-p
其中的 p → q 一樣是 -p|q 的縮寫。
假如我們有下列《公理系統》,那麼就可以反過來推論,得到 -B 與 -A 的結論。
公理 1: A → B
公理 2: B → C
公理 3: -C
推論過程如下:
公理 2: B → C
公理 3: -C
-------------
定理 1: -B
得出結論 -B ,然後繼續推論:
公理 1: A → B
定理 1: -B
-------------
定理 2: -A
得出結論 -A ,於是我們知道在該系統下,-C, -B, -A 都是真理。
歸結推論 (Resolution)
不管是《肯定前項》還是《否定後項》,都沒有辦法推論出《命題邏輯》(也就是布林邏輯+知識庫) 的所有定理。
但是在 1960 年 Davis 和 Putnam 提出了下列的 Resolution 推論法則 (中文稱為歸結推論法),經過 1965 年 John Alan Robinson 提出的 syntactical unification algorithm 改良後,得到了一個《完備》的推論法則,也就是可以推出所有定理的推論法則。
以下是 Resolution 推論法則的形式:
前提 1: -p | q
前提 2: p | r
===============
結論: q | r
我們可以用下列真值表,證明這個推論法則是對的,
p | q | r | -p|q | p|r |
---|---|---|---|---|
0 | 0 | 0 | 1 | 0 |
0 | 0 | 1 | 1 | 1 |
0 | 1 | 0 | 1 | 0 |
0 | 1 | 1 | 1 | 1 |
1 | 0 | 0 | 0 | 1 |
1 | 0 | 1 | 0 | 1 |
1 | 1 | 0 | 1 | 1 |
1 | 1 | 1 | 1 | 1 |
當我們將不符合前提的項目拿掉之後,以上的真值表就只剩以下這些項目。
p | q | r | -p|q | p|r |
---|---|---|---|---|
0 | 0 | 1 | 1 | 1 |
0 | 1 | 1 | 1 | 1 |
1 | 1 | 0 | 1 | 1 |
1 | 1 | 1 | 1 | 1 |
此時,如果我們檢查這些項目中 q|r
的真值表,會發現 q|r
為真者其結果全部為 1 ,因此 q|r
在這個前提下是真理。
p | q | r | -p|q | p|r | q|r | p|q |
---|---|---|---|---|---|---|
0 | 0 | 1 | 1 | 1 | 1 | 0 |
0 | 1 | 1 | 1 | 1 | 1 | 1 |
1 | 1 | 0 | 1 | 1 | 1 | 1 |
1 | 1 | 1 | 1 | 1 | 1 | 1 |
但是如果我們檢查這些項目中 p|q 的真值表,會發現有一項為 0 ,因此 p|q
在這個前提下並非真理。
所以 q|r
在此前提下是一個定理,但 p|q
則不是。
說明:在上述邏輯推論系統當中, -p|q
可以簡寫為 p → q
,而 p|r
則可以想成 -(-p)|r
,於是寫成 -p → r
。
於是推理法則可用箭頭的方式改寫為:
前提 1: p→q
前提 2: -p→r
===============
結論: -q→r (也就是 q|r)
透過這樣的改寫,您可以觀察到當 p=1
時 q=1
,當 p=0
時 r=1
,而 p
只有可能是 1 或 0,於是 q
與 r
兩者至少有一個成立,這也就是推論出的定理 q|r
成立的原因了。
有了 Resolution 推論法則後,我們就可以證明一些單獨用《肯定前項》和《否定後項》所無法推出的定理了,舉例而言,假如我們有一個知識庫系統,擁有下列《公理》。
公理1 : -A|B
公理2 : A|C
公理3 : -(B|C)|E
那麼我們可以用 Resolution 推論如下:
公理1 : -A|B
公理2 : A|C
================
定理1: B|C
然後再用結論 B|C 與公理3,繼續推論:
公理3 : -(B|C)|E
定理1: B|C
================
定理2: E
於是我們得到了 B|C 與 E 在該《公理系統》下都是《定理》的結論。
必須注意的是,單靠 Resolution 推論法則是無法推論出所有《定理》的, 1965 年 Robinson 提出的方法,採用《反證法》,也就是當你想證明某個定理 Q 是對的,你必須先將那個定理反過來,變成 -Q 加入《公理系統》KB,然後開始推論。
假如可以由 KB+(-Q) 推出《空子句》的話,那麼就代表 KB+(-Q) 會產生矛盾。
此時如果 KB 本身是無矛盾的,那麼就代表 -Q 與 KB 矛盾,反過來看就是 Q 為真理。
因此 Robinson 的方法是一種反證法。
我們同樣用上述的公理,但是改用 Robinson 的反證法來進行推論。
公理1 : -A|B
公理2 : A|C
公理3 : -(B|C)|E
請問 E 是否為真?
首先將 -E 加入系統,得到:
公理1 : -A|B
公理2 : A|C
公理3 : -(B|C)|E
反問句:-E
然後用下列推論:
公理3 : -(B|C)|E
待證明:-E
================
結論1: -(B|C)
接著再用推論:
公理1 : -A|B
公理2 : A|C
================
結論2: B|C
最後用推論:
結論1: -(B|C)
結論2: B|C
================
結論3:
由於上式產生了《空字句》,所以證明了 KB+(-E) 有矛盾,於是 E 是真理。
公理系統有矛盾會怎樣?
假如在布林邏輯裏,我們創造出以下這樣的公理系統。
公理 1: A
公理 2: -A
那麼會發生甚麼事呢?
根據 Robinson 的推論方法,我們先把 KB+(-Q) 放進去推論,由於 KB 本身就包含了 A 與 -A ,根據 Robinson 的推論方法可以改寫如下:
公理 1: A
公理 2: -A
反問句:-Q
於是可以推論出:
公理 1: A
公理 2: -A
================
結論:
這樣就推論出《空字句》了,於是不管 Q 是甚麼,Robinson 的方法在 KB+(-Q) 之後都會推論出《空字句》,也就是任何陳述 Q 都是對的。
如果用真值表來看,一個空無一物的真值表世界裏,任何陳述都無法被否證,所以任何陳述都可以是《定理》。(所有邏輯法則都無法被否認)
謂詞邏輯 (Predicate Logic)
在布林邏輯中,只有用來代表真假值的簡單變數,像是 A, B, C, X, Y, Z …. 等,所以邏輯算式看來通常如下:
- P & (P=>Q) => Q.
- A & B & C => D | E.
- -(A & B) <=> -A | -B.
這種布林命題邏輯裏沒有函數的概念,只有簡單的命題 (Proposition),因此布林邏輯也稱為命題邏輯 (Propositional Logic)。
而在《謂詞邏輯》(Predicate logic) 裏,則有「布林函數」的概念,因此其表達能力較強,例如以下是一些謂詞邏輯的範例。
- Parent(x,y) <= Father(x,y).
- Parent(John, Johnson).
- Ancestor(x,y) <= Parent(x,y).
- Ancestor(x,y) <= Ancestor(x,z) & Parent(z,y).
您可以看到在這種邏輯系統裏,有「布林變數」的概念 (像是 x, y, z 等等),也有函數的概念,像是 Parent(), Father(), Ancestor() 等等。
一階邏輯(First-Order Logic)
在上述這種謂詞邏輯系統中,如果我們加上 $\forall
$ (對於所有) 或 $\exists
$ (存在) 這兩個變數限定符號,而其中的謂詞不可以是變項,而必須要是常項,這種邏輯就稱為一階邏輯。
- $
\forall People(x) => Mortal(x)
$ ; 人都是會死的。 - $
People(Socrates)
$ ; 蘇格拉底是人。 - $
Mortal(Socrates)
$ ; 蘇格拉底會死。
當然、規則可以更複雜,像是以下這個範例,就說明了「存在一些人可以永遠被欺騙」。
- $
\exists x (Person(x) \wedge \forall y (Time(y) => Canfool(x,y))).
$
二階邏輯 (Second-Order Logic)
如果一階邏輯中的謂詞,放寬成可以是變項的話 (這些變項可以加上 $\forall
$ 與 $\exists
$ 等符號的約束),那就變成了二階邏輯,以下是一些二階邏輯的規則範例。
- $
\exists P (P(x) \wedge P(y)).
$ - $
\forall P \forall x (x \in P | x \notin P).
$ - $
\forall P (P(0) \wedge \forall y( P(y)=>P(succ(y)) ) => \forall y P(y) ).
$
(最後一條是《數學歸納法》規則)
對於上述這些邏輯系統而言,描述能力愈強大者,通常也愈複雜,而且《公理系統》與《推論的複雜度》也會提高,要建構出《很完美的數學體系》,難度也就愈來愈高了!
邏輯推論的程式
我們在 rlab 當中實作了兩個《邏輯推論引擎》,一個是《命题逻辑》(布林邏輯),另一種是《謂詞邏輯》,以下是其執行範例。
範例一:簡易測試
規則庫:test.kb
A<=B. B<=C&D. C<=E. D<=F. E. F. Z<=C&D&G.
執行結果:
D:\Dropbox\github\rlab\example>node kbQuery.js test.kb
["A<=B","B<=C&D","C<=E","D<=F","E","F","Z<=C&D&G",""]
rule:head=A terms=["B"]
rule:head=B terms=["C","D"]
rule:head=C terms=["E"]
rule:head=D terms=["F"]
rule:head=E terms=""
rule:head=F terms=""
rule:head=Z terms=["C","D","G"]
addFact(E)
addFact(F)
addFact(C)
addFact(D)
addFact(B)
addFact(A)
facts=["E","F","C","D","B","A"]
?-
範例二:動物世界
規則庫:animal.kb
哺乳類 <= 有毛.
哺乳類 <= 泌乳.
鳥類 <= 有羽毛.
鳥類 <= 會飛 & 生蛋.
食肉類 <= 哺乳類 & 吃肉.
食肉類 <= 有爪 & 利齒 & 兩眼前視.
有蹄類 <= 哺乳類 & 有蹄.
偶蹄類 <= 哺乳類 & 反芻.
獵豹 <= 哺乳類 & 吃肉 & 斑點.
老虎 <= 哺乳類 & 吃肉 & 條紋.
長頸鹿 <= 有蹄類 & 長腿 & 斑點.
斑馬 <= 有蹄類 & 條紋.
鴕鳥 <= 鳥類 & 長腿.
執行結果:
D:\Dropbox\github\rlab\example>node kbQuery.js animal.kb
["哺乳類 <= 有毛","哺乳類 <= 泌乳","鳥類 <= 有羽毛","鳥類 <= 會飛 & 生蛋","
食肉類 <= 哺乳類 & 吃肉","食肉類 <= 有爪 & 利齒 & 兩眼前視","有蹄類 <= 哺乳類 &
有蹄","偶蹄類 <= 哺乳類 & 反芻","獵豹 <= 哺乳類 & 吃肉 & 斑點","老虎 <= 哺乳
類 & 吃肉 & 條紋","長頸鹿 <= 有蹄類 & 長腿 & 斑點","斑馬 <= 有蹄類 & 條紋","鴕
鳥 <= 鳥類 & 長腿",""]
rule:head=哺乳類 terms=["有毛"]
rule:head=哺乳類 terms=["泌乳"]
rule:head=鳥類 terms=["有羽毛"]
rule:head=鳥類 terms=["會飛 "," 生蛋"]
rule:head=食肉類 terms=["哺乳類 "," 吃肉"]
rule:head=食肉類 terms=["有爪 "," 利齒 "," 兩眼前視"]
rule:head=有蹄類 terms=["哺乳類 "," 有蹄"]
rule:head=偶蹄類 terms=["哺乳類 "," 反芻"]
rule:head=獵豹 terms=["哺乳類 "," 吃肉 "," 斑點"]
rule:head=老虎 terms=["哺乳類 "," 吃肉 "," 條紋"]
rule:head=長頸鹿 terms=["有蹄類 "," 長腿 "," 斑點"]
rule:head=斑馬 terms=["有蹄類 "," 條紋"]
rule:head=鴕鳥 terms=["鳥類 "," 長腿"]
facts=[]
?- 有毛
addFact(有毛)
addFact(哺乳類)
facts=["有毛","哺乳類"]
?- 斑點
addFact(斑點)
facts=["有毛","哺乳類","斑點"]
?- 吃肉
addFact(吃肉)
addFact(食肉類)
addFact(獵豹)
facts=["有毛","哺乳類","斑點","吃肉","食肉類","獵豹"]
?-
您可以看到該推理程式,根據動物知識庫,在輸入《有毛、斑點、吃肉》之後推理出了符合的動物是《獵豹》。
該程式的主要部分為於下列網址,想要仔細研究的人可以參考閱讀。
- https://github.com/ccckmit/rlab/blob/master/example/kbQuery.js
- https://github.com/ccckmit/rlab/blob/master/lib/kb.js
後記
大部分的數學系統,都希望能達到這樣嚴格的程度,但可惜的是,並非所有數學系統都能完全達到這樣嚴格的程度。
舉例而言:《歐氏幾何》可以說是公理化的早期經典之作,但其中仰賴圖形輔助的證明仍然有很多,並沒有達到《完美公理化》的程度。
後來 希爾伯特 在1899年發行《幾何基礎》教材,將歐氏幾何重新用現代方式公理化,避免了一些歐幾里得公理中的弱點。
在希爾伯特在 1900 年提出的 23 個數學問題 中,就包含了很多《公理化》的相關問題,列舉如下:
- 第1題 連續統假設
- 第2題 算術公理之相容性
- 第6題 公理化物理
其中第2題是希望建構出一個《一致且完備》的算術公理體系,希望能夠建構出可證明所有算術定理的公理系統。
28年後,《歌德爾的完備定理》讓希爾伯特的這個夢想幾乎達成了,但是又過了一年,《歌德爾的不完備定理》,粉碎了希爾伯特的這個夢想!
這將會是我們下一章《計算理論》的主題。
參考文獻
- Jserv : Formal Verification
- 維基百科:命題邏輯
- 相關討論:為甚麼國中的數學證明是從「歐式幾何」開始教,而不從「布林代數」開始教呢?
- 數學中的公理化方法 (上) 吳開朗
- 數學中的公理化方法 (下) 吳開朗