命題論理を実装する (C#)

// この投稿は 数学 Advent Calendar 2016 の 16 日目の記事です。

命題といえば高校数学で「かつ」「または」「ならば」などを学習すると思いますが、
この投稿では、これらを一般化、形式化した命題論理をプログラミングで表現することを目指します。
プログラミングをしない方も、適宜飛ばせばなんとか読めると思います。

用語や定義については、主に Raymond Smullyan「記号論理学: 一般化と記号化」の第 7 章「命題論理入門」に記載されているものを使い、
解説と実装をしていきます。
プログラミング言語としては C# (.NET) を利用します。

Raymond Smullyan「記号論理学: 一般化と記号化」
「記号論理学: 一般化と記号化」
高橋 昌一郎, Raymond Smullyan, 川辺 治之

 

論理結合子

任意の命題 p は、真偽値 (truth value) を持ちます。真偽値とは、真 (T) または偽 (F) です。
そして、「かつ」「または」「ならば」などを一般化した概念を論理結合子 (logical connective) と呼び、次のものがあります。

  1. 否定 (~p)
    真偽値を反転させます。
  2. 論理積 (p ∧ q)
    p および q がともに真のときに限り真です。
  3. 論理和 (p ∨ q)
    p または q のうち、少なくとも一方が真のときに真です。
  4. 含意 (p ⇒ q)
    ~p ∨ q と同義です。
  5. 同値 (p ≡ q)
    (p ⇒ q) ∧ (q ⇒ p) と同義です。計算機においては、XOR 演算の否定と同義です。

論理式

さらに、論理式を次のように定義します。

  • 命題変数 (propositional variable): 命題を表す変数。値は、真または偽となりうる。
  • 命題定数 (propositional constant): 真を表す t および偽を表す f
  • 論理式 (formula): 命題変数、命題定数、論理結合子により構成される式。

ここまでの内容をもとに、論理式を実装します。 論理結合子は、否定のみが単項で、他はすべて二項です。

式を簡単に記述できるようにするため、静的メソッドを用意します。

 

恒真式および矛盾

論理式のうち、含まれる命題変数がどのような真偽値の組合せになっても真であるものを恒真式 (tautology) と呼びます。
逆に、含まれる命題変数がどのような真偽値の組合せになっても偽であるものを矛盾論理式または矛盾 (contradiction) と呼びます。
簡単な例を挙げると、p ∨ ~p は恒真式で、p ∧ ~p は矛盾です。

論理式が恒真式あるいは矛盾であるかどうかを判定するためのメソッドは、次のように実装できます。

以上のコードをまとめて、Blaze (GitHub) というライブラリとして公開しています。 NuGet でインストールできます。

 

ライブラリを使ってみる

さて、このライブラリを利用すると、命題論理に関する定理を証明できるようになります。
実際にいくつかやってみましょう。
Visual Studio で新規のコンソール アプリケーション プロジェクトを作成して、NuGet で Blaze をインストールします。
そして次のようなコードを記述します。

恒真式であるということは、その論理式がつねに成り立つということです。
このコードを実行することで、三段論法、背理法、対偶などを証明できます。

PropositionsConsole

 

次回は、このライブラリを利用してもう少し高度な問題を解いてみます。

次回: 命題論理の複雑な問題を解く (C#)

作成したライブラリ
Blaze (GitHub)
Blaze (NuGet Gallery)

作成したサンプル
PropositionsConsole (GitHub)

バージョン情報
.NET Framework 4.5

参照
Raymond Smullyan「記号論理学: 一般化と記号化」

コメント / トラックバック1件 to “命題論理を実装する (C#)”

  1. 命題論理の複雑な問題を解く (C#) | Do Design Space Says:

    […] 前回の命題論理を実装する (C#) では命題論理を扱うためのライブラリを作成しました。 今回は、このライブラリを利用して複雑な問題をいくつか解いてみます。 […]


コメントを残す

以下に詳細を記入するか、アイコンをクリックしてログインしてください。

WordPress.com ロゴ

WordPress.com アカウントを使ってコメントしています。 ログアウト / 変更 )

Twitter 画像

Twitter アカウントを使ってコメントしています。 ログアウト / 変更 )

Facebook の写真

Facebook アカウントを使ってコメントしています。 ログアウト / 変更 )

Google+ フォト

Google+ アカウントを使ってコメントしています。 ログアウト / 変更 )

%s と連携中

%d人のブロガーが「いいね」をつけました。