0.7 相關資料
本章中的騎士與惡棍問題所使用的邏輯形式稱作演算邏輯(calculational logic)，其主要精神是將命題邏輯與述語邏輯表達為適合用於等式推導與演算的形式。
Gries and Schneider [2003] 認為大部分形式邏輯系統是為了研究邏輯本身的特性而設計，而演算邏輯則是為了以邏輯解決問題而開發的。
演算邏輯由程式語言學者們於 80 年代初期漸漸發展出來。
Gries and Schneider [2003] 將此歸功於 Roland Backhouse, Edsger W. Dijkstra, Wim H.J. Feijen, David Gries, Carel S. Scholten, 以及 Netty van Gasteren 等人。他們的共同研究主題是以形式方法開發程式。
Dijkstra and Scholten [1990] 將演算邏輯用於指令式程式語言的語意中。
本章中的騎士與惡棍問題由 Backhouse [2003] 中節錄而來。
這是一本介紹以形式方式構思演算法以解決問題的教科書。
本章只用到了 (<=>) 一個運算子，該書中則有更完整的介紹。
Gries and Schneider [October 22, 1993] 則是一本以演算邏輯為基礎的離散數學教科書。
「讓符號為你工作」這句口號可在 Dijkstra 的許多著作中見到（例如 Dijkstra and van Gasteren [1986] , Dijkstra [2000]）。 Dijkstra [2004] 寫道： 「設計程式的人最好把程式當作精巧的算式。 而我們知道只有一種設計精巧算式的可靠方法：用符號操作來推導它。 我們得讓符號為我們工作，因為這是已知唯一在大尺度下仍可行的方法。」 Misra 則在 1988 年 Marktoberdorf 暑期課程的演講 [Misra 1989] 中虛構了一個故事： 使用羅馬數字的羅馬人被推銷比較易於演算的印度-阿拉伯數字系統，卻不以為然地說「我們已經有奴隸為我們工作了！」 % We also know that, while from an operational point of view a program can be nothing but an abstract symbol manipulator, the designer had better regard the program as a sophisticated formula. And we also know that there is only one trustworthy way for the design of sophisticated formulae, viz. derivation by means of symbol manipulation. We have to let the symbols do the work, for that is the only known technique that scales up.
希臘與瑪雅數字的例子取自 Mazur [2014]。 該書對於種種符號的演進有更詳盡的介紹。