第9章 論理学と形式的手法

はじめに

論理学は、正しい推論の原理を研究する学問であり、コンピュータサイエンスの理論的基盤を形成します。形式的手法は、この論理学を用いてシステムの仕様記述、設計、検証を厳密に行う技術です。本章では、命題論理から始まり、一階述語論理、時相論理、そしてプログラム検証の理論まで、段階的に学習します。

ソフトウェアの複雑性が増大する現代において、形式的手法の重要性はますます高まっています。航空機制御システム、医療機器、金融システムなど、高い信頼性が要求される分野では、数学的に厳密な検証が不可欠です。本章で学ぶ理論と技術は、これらの要求に応える基礎を提供します。

通し例: 安全なメッセージ配送基盤 「認証済みメッセージだけを配送する」「再送しても重複処理しない」「重要通知は最終的に到達する」といった要件は、自然言語のままでは曖昧です。本章では、通し例の要件を論理式と検証手続きへ落とす見方を与えます。

学習目標

• 命題論理・述語論理の構文と意味論（充足・妥当性）を説明できる
• 導出体系（自然演繹、シーケント計算等）の健全性・完全性の直観を述べられる
• 決定可能性・複雑性（SAT, QBF）と自動定理証明の基本アルゴリズムを説明できる
• Herbrand の定理や Skolem 化の役割を説明できる
• SAT/SMT ソルバの高レベル動作（DPLL/CDCL 等）を概説できる

9.1 命題論理

9.1.1 構文と意味論

定義 9.1 命題論理式の構文的定義：

1. 命題変数 p, q, r, … は論理式
2. φ, ψ が論理式なら、¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) も論理式

定義 9.2 真理値割当 \(v: \mathrm{Var} \to \{0, 1\}\) を命題変数から真理値への関数とする。

v の論理式への拡張 v̂ を帰納的に定義：

• v̂(p) = v(p)（命題変数）
• \(v̂(¬φ) = 1 - v̂(φ)\)
• \(v̂(φ ∧ ψ) = min(v̂(φ), v̂(ψ))\)
• \(v̂(φ ∨ ψ) = max(v̂(φ), v̂(ψ))\)
• \(v̂(φ → ψ) = max(1 - v̂(φ), v̂(ψ))\)
• \(v̂(φ ↔ ψ) = 1 ⟺ v̂(φ) = v̂(ψ)\)

9.1.2 論理的帰結と同値

定義 9.3

• φ が恒真式（トートロジー）⟺ すべての v で v̂(φ) = 1、記号：⊨ φ
• φ が充足可能 ⟺ ある v で v̂(φ) = 1
• φ が矛盾 ⟺ すべての v で v̂(φ) = 0

定義 9.4 \(\Sigma \models \varphi\)（\(\Sigma\) が \(\varphi\) を意味論的に含意）\(\Leftrightarrow\)

Σ のすべての式を真にする割当は φ も真にする

9.1.3 標準形

定義 9.5

• リテラル：命題変数またはその否定
• 節（clause）：リテラルの選言
• 連言標準形（CNF）：節の連言
• 選言標準形（DNF）：連言節の選言

定理 9.1 すべての論理式は等価な CNF および DNF に変換可能。

注意：CNF/DNF への機械的変換は式のサイズを指数的に増大させる場合がある（サイズ爆発）。

アルゴリズム（CNF への変換）：

1. → と ↔ を除去：φ → ψ ≡ ¬φ ∨ ψ
2. ¬ を内側に押し込む（De Morgan）
3. ∨ を ∧ の上に分配

9.1.4 命題論理の決定手続き

直観図：DPLL と CDCL の対比（学習・非年代戻り・VSIDS）

真理値表法

時間複雑度：O(2^n · \(\lvert φ\rvert\))（n は変数数）

DPLLアルゴリズム

DPLL(φ, v):
    φ' = Propagate(φ, v)  // 単位伝播
    if φ' = ⊤: return SAT
    if φ' = ⊥: return UNSAT
    l = ChooseLiteral(φ')  // 分岐変数選択
    if DPLL(φ', v ∪ {l = true}) = SAT:
        return SAT
    return DPLL(φ', v ∪ {l = false})

最適化技法：

• 単位伝播（unit propagation）
• 純リテラル削除（pure literal elimination）
• 学習節の追加（CDCL）

9.1.5 健全性と完全性

定義 9.6 証明体系が健全（sound）\(\Leftrightarrow\) \(\vdash \varphi \Rightarrow \models \varphi\)

定義 9.7 証明体系が完全（complete）\(\Leftrightarrow\) \(\models \varphi \Rightarrow \vdash \varphi\)

定理 9.2 命題論理の自然演繹は健全かつ完全である。

9.1.6 コンパクト性定理

定理 9.3（コンパクト性定理）

\(\Sigma \models \varphi\) ⟺ ある有限部分集合 \(\Sigma_0 \subseteq \Sigma\) に対して \(\Sigma_0 \models \varphi\)

証明の概要：完全性定理を用いて、構文的証明の有限性から導く。□

応用：無限のオブジェクトに関する性質を有限の近似で捉える。

9.2 一階述語論理

9.2.1 構文

定義 9.8 一階言語は以下から構成：

• 変数：x, y, z, …
• 定数記号：a, b, c, …
• 関数記号：f, g, h, …（各々アリティを持つ）
• 述語記号：P, Q, R, …（各々アリティを持つ）
• 論理記号：¬, ∧, ∨, →, ↔, ∀, ∃
• 補助記号：(, )

項の帰納的定義：

1. 変数と定数は項
2. \(t_1, \ldots, t_n\) が項で \(f\) が \(n\) 項関数なら \(f(t_1, \ldots, t_n)\) は項

論理式の帰納的定義：

1. \(t_1, \ldots, t_n\) が項で \(P\) が \(n\) 項述語なら \(P(t_1, \ldots, t_n)\) は原子式
2. φ, ψ が論理式なら ¬φ, (φ ∧ ψ) なども論理式
3. φ が論理式で x が変数なら ∀x φ, ∃x φ も論理式

9.2.2 意味論

定義 9.9 構造（解釈）\(M = (D, I)\) は：

• D：空でない領域（議論領域）
• I：解釈関数
  • 定数記号 c に対して I(c) ∈ D
  • n 項関数記号 f に対して \(I(f): D^n \to D\)
  • n 項述語記号 P に対して \(I(P) \subseteq D^n\)

定義 9.10 変数割当 \(s: \mathrm{Var} \to D\) に対する充足関係 \(M, s \models \varphi\) を定義

9.2.3 前束標準形

定理 9.4 すべての一階論理式は等価な前束標準形に変換可能：

\(Q_1 x_1 \cdots Q_n x_n\, \psi\)（\(Q_i \in \{\forall, \exists\}\)、\(\psi\) は量化子を含まない）

変換手順：

1. 束縛変数の改名
2. 量化子の外への移動

9.2.4 Skolem化

定義 9.11 Skolem化：存在量化子を除去し、新しい関数記号を導入

例：∀x∃y P(x, y) → ∀x P(x, f(x))（f は新しい Skolem 関数）

定理 9.5 \(\varphi\) が充足可能 \(\Leftrightarrow\) \(\varphi\) の Skolem 標準形が充足可能

9.2.5 完全性定理

定理 9.6（Gödelの完全性定理）

一階述語論理は健全かつ完全である：Σ ⊨ φ ⟺ Σ ⊢ φ

証明の概要： （健全性）帰納法による直接的な証明 （完全性）Henkin の方法：無矛盾な理論から構造を構成□

9.2.6 決定不能性

定理 9.7 一階述語論理の妥当性問題は決定不能である。

証明：停止問題からの還元による。□

決定可能な断片：

• 単項述語論理
• ∀∃ 形の文
• Presburger 算術

9.3 時相論理

9.3.1 線形時相論理（LTL）

定義 9.12 LTL の構文：

• 命題変数 p は LTL 式
• φ, ψ が LTL 式なら ¬φ, φ ∧ ψ も LTL 式
• φ が LTL 式なら ○φ, □φ, ◇φ, φ U ψ も LTL 式

意味論：無限列 \(\pi = s_0s_1s_2\ldots\) 上で定義

• π, i ⊨ ○φ ⟺ π, i+1 ⊨ φ（次の状態）
• π, i ⊨ □φ ⟺ ∀j ≥ i, π, j ⊨ φ（常に）
• π, i ⊨ ◇φ ⟺ ∃j ≥ i, π, j ⊨ φ（いつか）
• π, i ⊨ φ U ψ ⟺ ∃j ≥ i, (π, j ⊨ ψ ∧ ∀k(i ≤ k < j → π, k ⊨ φ))（まで）

9.3.2 計算木論理（CTL）

定義 9.13 CTL の構文：

状態式と経路式を相互再帰的に定義

• A（すべての経路で）、E（ある経路で）

CTL の基本演算子：

• AX, EX（次の状態）
• AF, EF（いつか）
• AG, EG（常に）
• AU, EU（まで）

9.3.3 モデル検査

定義 9.14 モデル検査問題：

与えられた有限状態システム M と時相論理式 φ に対して、M ⊨ φ ?

CTL モデル検査アルゴリズム

CTLCheck(M, φ):
    case φ of
        p: return {s | p ∈ L(s)}
        ¬ψ: return S \ CTLCheck(M, ψ)
        ψ1 ∧ ψ2: return CTLCheck(M, ψ1) ∩ CTLCheck(M, ψ2)
        EX ψ: return {s | ∃s', s → s' ∧ s' ∈ CTLCheck(M, ψ)}
        EF ψ: return 最小不動点 Z. CTLCheck(M, ψ) ∪ CTLCheck(M, EX Z)
        EG ψ: return 最大不動点 Z. CTLCheck(M, ψ) ∩ CTLCheck(M, EX Z)
        E[ψ1 U ψ2]: return 最小不動点 Z. CTLCheck(M, ψ2) ∪ 
                     (CTLCheck(M, ψ1) ∩ CTLCheck(M, EX Z))

時間複雑度：\(O(\lvert φ\rvert \cdot \lvert S\rvert \cdot \lvert R\rvert)\)（S：状態集合、R：遷移関係）

9.3.4 公平性

定義 9.15 公平性制約：

• 弱公平性：永続的に可能なアクションはいつか実行される
• 強公平性：無限回可能なアクションはいつか実行される

公平性を含む CTL：

• A_fair、E_fair オペレータの追加
• 公平な経路のみを考慮

9.4 プログラム検証

9.4.1 Hoare論理

定義 9.16 Hoare三つ組 \(\{P\}\ S\ \{Q\}\)：

• P：事前条件
• S：プログラム文
• Q：事後条件

意味：P が成立する状態で S を実行し、正常終了すれば Q が成立

9.4.2 推論規則

基本的な推論規則：

1. 代入規則：

   {P[e/x]} x := e {P}
   

2. 順次実行：

       前提: {P} S1 {Q}, {Q} S2 {R}
       結論: {P} S1; S2 {R}
   

3. 条件分岐：

       前提: {P ∧ B} S1 {Q}, {P ∧ ¬B} S2 {Q}
       結論: {P} if B then S1 else S2 {Q}
   

4. ループ：

   前提: {I ∧ B} S {I}
   結論: {I} while B do S {I ∧ ¬B}
   

   （I はループ不変条件）

5. 帰結規則：

   前提: P' → P, {P} S {Q}, Q → Q'
   結論: {P'} S {Q'}
   

9.4.3 最弱事前条件

定義 9.17 最弱事前条件 \(wp(S, Q)\)：

S の実行後に Q を保証する最も弱い事前条件

計算規則：

• \(wp(x := e, Q) = Q[e/x]\)
• \(wp(S_1; S_2, Q) = wp(S_1, wp(S_2, Q))\)
• \(wp(if B then S_1 else S_2, Q) = (B → wp(S_1, Q)) ∧ (¬B → wp(S_2, Q))\)
• wp(while B do S, Q) = 最小不動点（一般には計算不能）

9.4.4 プログラムの全正当性

定義 9.18

• 部分正当性：{P} S {Q} - 終了すれば Q が成立
• 全正当性：[P] S [Q] - 必ず終了し、Q が成立

停止性の証明：

• 整礎関係による順序の導入
• 各ループ反復で順序が真に減少することを示す

9.4.5 分離論理

動機：ヒープを使うプログラムの検証

新しい述語：

• emp：空ヒープ
• x ↦ v：x が v を指す単一セル
• P * Q：分離結合（disjoint union）

フレーム規則：

    {P} S {Q}
―――――――――――――――
{P * R} S {Q * R}

（S が R に言及しない変数のみを変更）

9.5 形式的仕様記述

9.5.1 代数的仕様

例 9.1 スタックの代数的仕様

sorts: Stack, Elem, Bool
operations:
    empty: → Stack
    push: Stack × Elem → Stack
    pop: Stack → Stack
    top: Stack → Elem
    isEmpty: Stack → Bool
axioms:
    isEmpty(empty) = true
    isEmpty(push(s, e)) = false
    top(push(s, e)) = e
    pop(push(s, e)) = s

9.5.2 Z記法

基本要素：

• スキーマ：状態と操作の構造化記述
• 集合論と型理論に基づく

例 9.2 カウンタの仕様

┌─ Counter ────────
│ value: ℕ
│ limit: ℕ
├────────────────
│ value ≤ limit
└────────────────

┌─ Increment ──────
│ ΔCounter
│ amount?: ℕ
├────────────────
│ value' = value + amount?
│ value' ≤ limit
└────────────────

9.5.3 時相論理による仕様

安全性（Safety）：「悪いことは起こらない」

• □(request → ◇grant)（要求にはいつか応答）

活性（Liveness）：「良いことがいつか起こる」

• □◇enabled（永遠に有効化される）

公平性（Fairness）：

• □◇request → □◇grant（無限回要求→無限回許可）

9.6 定理証明支援系

9.6.1 対話型定理証明

主要なシステム：

• Coq：帰納的構成の計算（CIC）に基づく
• Isabelle/HOL：高階論理
• Lean：依存型理論

証明の構造：

Theorem example : ∀ n : nat, n + 0 = n.
Proof.
  intros n.
  induction n.
  - reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.

9.6.2 自動定理証明

SMTソルバ：

• 理論の組み合わせ（算術、配列、ビットベクトル）
• DPLL(T)アルゴリズム

応用：

• プログラム検証
• 制約充足問題
• 最適化問題

9.6.3 証明の形式化

利点：

• 機械的検証可能性
• 証明の再利用
• 大規模な数学的開発

課題：

• 証明の記述コスト
• 自動化の限界
• 抽象化のギャップ

9.6.4 最小実行例（SAT/SMT / 定理証明）

以下は「手元で動く」最小例です。目的は (1) 充足可能性を機械判定する、(2) 短い定理を証明支援系で形式化する、の2点です。

SAT/SMT: Z3（Python）

• 例ファイル：sat_demo.py
• 必要要件：Python 3.11+、z3-solver（pip）

python3 -m venv .venv
. .venv/bin/activate
pip install z3-solver
cd docs/assets/examples/formal-methods/z3
python sat_demo.py

定理証明: Lean（Lean4）

• 例ファイル：Simple.lean
• 必要要件：Lean4 CLI（導入手順は環境に依存するため、本書では固定しない）

# Lean4 がインストール済みの環境で
cd docs/assets/examples/formal-methods/lean
lean Simple.lean

注：モデル検査の最小例は、第12章のTLA+（TLC）例も参照してください。

まとめ

• 論理は仕様・検証・自動推論の共通言語で、健全性・完全性が基盤
• SAT/SMT 技術は広範囲に応用され、理論と実装が密接にリンクする
• 問題の表現（論理形式）と決定手続きの選択が性能・適用範囲を左右

次章への橋渡し

第9章では「正しさ」や「意味」を形式化する方法を扱いました。次章からの Part IV では応用領域へ進み、まず第10章で対象を情報そのものに切り替え、不確実性と通信の限界をエントロピーで定量化します。

補助資料を併用するなら、理論の使われ方は 付録E の第9章節、理解確認は 付録F の第9章節を参照してください。

参考文献と次の一歩

• 図版の再参照: 本章の図をまとめて見返したいときは 付録H: 図版ガイドと図一覧 を参照してください。
• 標準: Michael Huth, Mark Ryan, 『Logic in Computer Science: Modelling and Reasoning about Systems』. 命題論理からモデル検査までを一貫した視点で学べる定番教科書です。
• 検証: Aaron R. Bradley, Zohar Manna, 『The Calculus of Computation』. 論理、決定手続き、形式検証の橋渡しを確認したい読者に向いています。
• モデル検査: Edmund M. Clarke, Orna Grumberg, Doron Peled, 『Model Checking』. CTL/LTL とモデル検査の標準的な参照先です。
• 出典メモ: Hoare 論理は Hoare の 1969 年論文、時相論理によるプログラム推論は Pnueli の 1977 年論文にさかのぼります。本章はそれらを SAT/SMT と検証実務へ接続する構成を取っています。
• 次の一歩: 形式仕様を並行システムへ適用するなら第12章が自然です。用語の取り違えを避けたい場合は 付録D を辞書として使ってください。

  章末問題

• 代表演習と詳細解答は 付録C（第9章） を参照。

取り組み方ガイド

迷ったら次の表の順で進め、詰まったら「主に戻る節」にある意味論・証明規則・検証手順を先に見直してください。

基礎問題

1. 以下の論理式の充足可能性を判定し、充足可能な場合はモデルを示せ： \((a) (p → q) ∧ (q → r) ∧ (r → p)\) (b) (p ∨ q ∨ r) ∧ (¬p ∨ ¬q) ∧ (¬q ∨ ¬r) ∧ (¬r ∨ ¬p)

2. 以下の一階論理式を前束標準形に変換せよ： \((a) ∀x(P(x) → ∃y Q(x, y)) ∧ ∃z R(z)\) \((b) ¬∀x∃y(P(x, y) ↔ ¬∃z Q(y, z))\)

3. 以下の Hoare 三つ組を証明せよ： \((a) \{x = n ∧ n ≥ 0\} y := 1; while x > 0 do (y := y \cdot x; x := x - 1) \{y = n!\}\) \((b) \{true\} x := a; y := b; z := x; x := y; y := z \{x = b ∧ y = a\}\)

4. CTL 式 AG(request → AF grant) の意味を説明し、 この性質を満たす/満たさない状態遷移系の例を示せ。

発展問題

1. Resolution による自動定理証明について： (a) Resolution の健全性と完全性を証明せよ (b) Horn 節に対する効率的な戦略を説明せよ

2. Büchi オートマトンと LTL の関係について： (a) LTL 式から等価な Büchi オートマトンへの変換を説明せよ (b) この変換の複雑性を解析せよ

3. 分離論理を用いて、連結リストの反転アルゴリズムを検証せよ。

4. 型理論と論理の対応（Curry-Howard 対応）について説明し、 具体例を用いて証明とプログラムの関係を示せ。

探究課題

1. 並行プログラムの検証手法について調査し、 共有メモリとメッセージパッシングそれぞれの検証技法を比較せよ。

2. 確率的モデル検査について調査し、 マルコフ連鎖上の時相論理（PCTL）とその検証アルゴリズムを説明せよ。

3. 依存型を用いたプログラム検証について調査し、 Coq や Agda での証明付きプログラミングの実例を示せ。

4. ハイブリッドシステム（連続・離散混在系）の形式的検証について調査し、 主要なアプローチと課題を論ぜよ。