萩谷　昌己：ソフトウェア科学のための論理学

概要

ソフトウェア科学を研究する計算機科学者が知っておくべき数理論理学の素養とはどのようなものだろうか。 この問いに答えるための本である。 著者は言う。命題論理を含む一階述語論理は常識である。ここは必修編となっている。 次に、様相論理や動的論理、ホーア論理を上級編として紹介している。 選択編では直観主義論理とカテゴリー（圏）について説明がある。

感想

この本では、必修編だけは真面目に勉強した。 学習のてびきでは これらを読まないなら、本書を買う価値がないとで言い切っていたからである。 毎朝ちびちびと勉強した。でもわからなかったなあ。

第２章　一階述語論理の演繹体系

ワングのアルゴリズム( Wang's algorithm ) という、トートロジ判定アルゴリズムが紹介されている。 Common Lisp の実装があったので真似てみたらできた。 これを Scheme や JavaScript で動かすのが目標である。

数式

数式表示には、ASCIIMathMLを使っている。

まりんきょ学問所 ＞ コンピュータの部屋 ＞ コンピュータの本 ＞ 萩谷　昌己：ソフトウェア科学のための論理学