記号論理

年度	2006
科目名	記号論理
教員名	松原　康夫
授業概要	人間とコンピュータの間には大きな隔たりがある。これを縮めるためには、知識を入力してコンピュータが自動的に推論できるようにする必要がある。そのためにさまざまな知識の表現法が考えられたが、結局はもっとも明確な意味論と推論方法を持った記号論理が、実際によく使われている。この授業では記号論理のなかでも最も基本的な、命題論理と述語論理について基礎から理解し、真理の木（タブロー法）による証明アルゴリズムを身につける。
授業計画	概ね以下の順序に沿うが、できるだけ直観的に理解できるような例題を用いるとともに、実際に手を動かすことで、観念的な理解でなく体で覚えることを目標とする。大半の受講生が各ステップを理解してから次のステップに進みたい。 論証とは何か：日本語で記述した文を使って、どのような関係が推論または論証と呼べるのかについて考察する。 命題論理と論理式：命題論理の論理式はどのように構成されるのか、どのような場合に真となったり偽となったりするのかについて述べる。またコンピュータを構成する論理回路と論理式の関係についても述べる。 論理式の間の関係と論理式の変形：分配則、結合則、ド・モルガンの法則など基本的な法則あるいは連言標準形などを解説する。 命題論理と意味論：原子式の意味から、論理式全体としてはどのような意味を持つのかを考え、真理値表を作って真偽値を調べる方法を学ぶ。 命題論理と推論：真理の木の方法を使って、幾つかの論理式の集合から別の論理式を証明する方法を習得する。 述語論理と論理式：述語論理の論理式がどのように構成されるのかについて学ぶと共に、命題論理では表現できない日本語の文の意味を述語論理の論理式でどう表現するかを学ぶ。 述語論理と意味論：述語論理の論理式が真である、あるいは偽であるとはどういうことか、モデル論による意味を述べる。また、論理式の間の関係や標準形についても学ぶ。 述語論理と推論：述語論理における真理の木の方法を使った証明法を習得する。 その他：時間が許せば、述語論理が、原理的に決定不可能な問題を含んでいることや、第一階の述語論理では表現できない、高階の論理があること等に触れる。
評価方法	試験の成績を基本とするが、課題の提出状況等を考慮する。
教科書
参考書
メッセージ	コンピュータの世界で論理は極めて基本的なものである。これからコンピュータの世界に生きる人は、論理について基礎を理解するとともに、推論の具体的な方法について知っておくべきである。真理の木の方法は、やる気さえあれば誰でもマスターできるものである。