形式的検証

命題論理

Takami Torao #命題論理
  • このエントリーをはてなブックマークに追加

概要

命題論理 (propositional logic) は、真偽値を持つ宣言文 (declarative sentence) を記号的に表現し、それらの間の論理的関係を厳密に推論するための計算可能な枠組みを提供する、コンピュータサイエンスにおける形式的推論の基礎を成す論理体系である。これは、複雑な議論を形式的な記号操作に還元することで推論の大統制を機械的に検証可能にする。自然言語における曖昧性や文脈依存性を排除し、構文論 (syntax)、意味論 (semantic)、証明論 (proof theory) という 3 つの構造によって論理的推論を数学的対象として扱う。

この理論体系は、ソフトウェア検証、ハードウェア設計、人工知能、データベース理論など、コンピュータサイエンスの広範な領域における基盤技術となっている特に、充足可能性問題 (SAT) の解法、モデル検証 (model checking)、定理証明 (theorem proving) といった実用的手法の理論的基礎を提供する。命題論理は、より表現力の高い述語理論、時相理論、様相理論への出発点であり、これらの高度な理論体系もまた命題理論の原理を継承・拡張している。

Table of Contents

  1. 概要
  2. 1. 命題理論の基礎と宣言文
    1. 1.1. 宣言文
    2. 1.2. 宣言文の例
      1. 1.2.1. 数学的命題
      2. 1.2.2. 観察可能な事象
      3. 1.2.3. 未解決の数学的予想
      4. 1.2.4. 反事実的条件文
      5. 1.2.5. 多言語における宣言文
      6. 1.2.6. 非宣言文
    3. 1.3. 形式化の必要性
      1. 1.3.1. コンピュータシステムにおける推論の必要性
    4. 1.4. 論理結合子の導入
    5. 1.5. 合成的構文と優先順位
    6. 1.6. 論理的推論の構造
  3. 2. 自然演算入門 - 命題論理の証明規則
  4. 3. 自然演算の高度な技法
  5. 4. 命題論理の形式的構文
  6. 5. 命題論理の意味論と健全性・完全性
  7. 6. 正規形と論理式の標準化
  8. 7. SAT Solver の理論と実装
  9. 参考文献

1. 命題理論の基礎と宣言文

1.1. 宣言文

原理的に真または偽の真理値を割り当てることが可能な文を宣言文 (declarative sentence) またはステートメント (statement) と呼ぶ。この真偽判定可能性 (truth-evaluability) は論理的推論の対象となる本質である。

形式理論の目的は、コンピュータサイエンスの実務において遭遇する状況を、形式的推論が可能な言語でモデル化することである。ここで「推論」とは、与えられた状況についての議論を構築することを意味し、その議論が妥当であり、厳密に防御可能であるか、あるいは機械上で実行可能であることを要求する。

宣言文は以下の性質を満たす文である:

  1. 真理値保持特性: 原理的に真 (true) または偽 (false) のいずれかの真理値を持つ。

  2. 客観的判定可能性: (少なくとも原理的には) 真偽の判定が主観に依存しない。

  3. 命題的内容: 世界の状態について何らかの主張を行う。

真理値の実際の決定可能性と、原理的な真理値保持性とは、異なる概念であることに注意。

1.2. 宣言文の例

以下に宣言文と非宣言文の例を示す。

1.2.1. 数学的命題

3 と 5 の和は 8 に等しい。

この文は数学的事実に訴えることで検証可能である。暗に 10 進数アラビア数字表記を仮定しているが、この文は明確に真である。

1.2.2. 観察可能な事象

Jane は Jack の告発に激しく反応した。

この文は検証においてより問題を含んでいる。まず Jane と Jack が誰であるかを知る必要があり、おそらくその場面を目撃した信頼できる人物の証言を得る必要がある。しかし、原理的には、我々がその場にいたならば Jane の激しい反応を観測できたであろうという直感がある。この「原理的に判定可能性」が重要である。

1.2.3. 未解決の数学的予想

2 より大きいすべての偶数は、2 つの素数の和として表すことができる (Goldbach 予想)

この文についての事実は明らかに真か偽のいずれかである。しかし、今日に至るまでこの文が真理を表現するかどうかを誰も知らない。さらに、それが真であったとしても、有限の手順でそれを示されるかすらも明らかではない。実際の真理値が問題の文によって示唆される実際の事態を反映すべきかは考慮する余地があるが、一旦この記事では、文が原理的に何らかの真理値を獲得できさえすれば宣言文として扱う。

1.2.4. 反事実的条件文

火星人が存在し、ピザを食べるなら、全員がペパロニをトッピングとして好む。

この文は一見してふざけているように見えるが、論理的には正当な宣言文である。火星人が存在してピザを食べるならば、彼らはペパロニを好むか好まないかのいずれかである (述語論理を導入すると、火星人が存在しない場合、この文は真であることがわかる)。

1.2.5. 多言語における宣言文

Albert Camus était un écrivain français. (アルベール・カミュはフランスの作家であった)

Die Würde des Menschen ist unantastbar. (人間の尊厳は不可侵である)

宣言文は自然文や人工言語を問わず、あらゆる言語で表現可能である。

1.2.6. 非宣言文

疑問文: 塩を取っていただけますか?

命令文: 位置について、用意、ドン!

願望文: 幸運があなたに訪れますように

これらの文には真理値を割り当てることができない。疑問文は情報を要求し、命令文は行動を支持し、願望文は希望を表現するが、いずれも世界の状態について真偽を判定可能な主張を行わない。

1.3. 形式化の必要性

1.3.1. コンピュータシステムにおける推論の必要性

コンピュータサイエンスでは、システムやプログラムの振る舞いについて正確な宣言文に主な関心があり、そのような文を特定するだけでなく、与えられた仕様を満たすかを検証したいと考える動機がある。したがって、以下の性質を持つ推論の計算体系を開発する必要がある。

  1. 初期化された変数などの仮定から結論を導出できる。

  2. 真理保存性: すべての仮定が真であれば、結論も真である。

  3. 信頼性: 推論的規則が健全であり、偽を導出しない。

コンピュータプログラムの任意の真の性質が与えられたとき、その性質を結論とする議論を計算体系で見つけられるかどうかがより困難である (ゴールドバッハ予想の例を参照)。論理は本質的に記号的である。すべての自然言語の宣言文の十分に大きな部分集合を記号列に翻訳する。

  1. 圧縮性: 宣言文の完全だが圧縮された符号化
  2. 機械的操作: 議論の純粋な構築に集中
  3. 自動化可能性: コンピュータによる自動的な使用操作が可能
  4. 曖昧性の排除: 自然言語の曖昧性を除去

この記号化は、宣言文を原子的 (atomic) または不可分 (indecomposable) として扱い、各原子文に記号 \(p\), \(q\), \(r\), \(\ldots\) または \(p_1,p_2,p_3,\ldots\) を割り当て、合成的方法 (compositional way) によってより複雑な文を符号化する。

1.4. 論理結合子の導入

1.5. 合成的構文と優先順位

1.6. 論理的推論の構造

2. 自然演算入門 - 命題論理の証明規則

3. 自然演算の高度な技法

4. 命題論理の形式的構文

5. 命題論理の意味論と健全性・完全性

6. 正規形と論理式の標準化

7. SAT Solver の理論と実装

参考文献

  1. Huth, Michael and Ryan, Mark. LOGIC IN COMPUTER SCIENCE: Modelling and reasoning about systems. Cambridge university press, 2004.