入門！論理学

形式手法における検証法は2通りある。

1. 仕様を「定理」とみなし、「公理」と「推論規則」を使って証明する方法。
2. 仕様を「モデル」として構築し、要求として与えられる条件を満たす可能性を計算機上で探索する方法。

1つめの方法に用いるツールは「定理証明系」と呼ばれ、Event-Bも定理証明系のツールである。2つめの方法はモデル検査ともよばれる。ソフト開発者にとってモデル検査は理解しやすいと思う。モデルの構築はプログラムを作るのに近い。その形式手法の言語を覚え、ツールを使いこなすことさえできるようになれば割と習得しやすいと思う。
それに対し、1つめ「定理証明系」は形式手法言語やツールを使いこなすことの難しさに加え、数理論理学の知識が求められる。命題論理、述語論理、証明とはなんぞや、集合論といったことについて知っていることが前提として求められている。
現場のソフト開発者が、このようなスキルをサブセットとして持っていることはあまりないだろう。実際、自分も大学でPrologや論理回路の講座でかじった程度でしかない。そのような知識を持っていなくともソフトウェアを作ることはできる。定理証明系のツールが流行らないのはこの点が問題なんだろうな。
というわけで今更ながら論理学からおさらいしている。コンピュータサイエンス自体は数理論理学の恩恵を多大に受けているのに、そこでソフトを作っている人は数理論理学をあまりわかってないとは何とも皮肉な話。

入門!論理学 (中公新書)

上記の本は論理学の本。論理学なのに記号がほとんど出てこない。しかも、縦読みである。入門と書いてあるが実際に初心者が読むにはハードルが高いと思う。お堅い本で勉強しようとしたが押し寄せる記号の波にうちのめされてしまった人にこそ読んでほしい本。お堅い本の隣にこの本をおいて併せて読み進めていくと互いに補い合い理解が深まると思う。 ちなみに、数理論理学については以下のサイトが参考になる。

Introduction to Mathematical Logic