MCP-Logic

MCP-Logic

Prover9、Mace4、および組み込みの推論用LLMを使用した、一階論理の自動推論を行うMCPサーバーです。

機能

• 定理証明 - Prover9で論理式を証明します
• モデル探索 - Mace4で有限モデルを探索します
• 反例の探索 - 論理式が帰結しない理由を示します
• 構文検証 - 有用なエラーメッセージとともに、数式を事前検証します
• カテゴリ的推論 - 圏論の証明を組み込みでサポートします
• 命題論理の充足可能性 - 命題論理を高速に検査する、純粋に解析的なHCC証明器です
• アブダクション推論 - 変分自由エネルギー（VFE）を使用して仮説を順位付けします
• 🤖 Logic Advisor（新機能） - 組み込みのTwIL-LM3推論用LLMが、論理問題を最初から最後まで解きます。平易な英語で質問するだけです
• 自己完結型 - 依存関係はすべて自動的にインストールされます

クイックスタート

インストール

Linux/macOS：

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
./linux-setup-script.sh

Windows：

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
windows-setup-mcp-logic.bat

セットアップスクリプトは、以下を自動的に実行します。

• LADR（Prover9 + Mace4）をダウンロードしてビルドします
• Python仮想環境を作成します
• すべての依存関係をインストールします
• Claude Desktopの設定を生成します

Logic Advisorを有効にする（任意）

組み込みのLogic Advisorは、ローカルの30億パラメーターのLLM（TwIL-LM3 Q8）を使用して、論理問題を最初から最後まで解きます。インストールするには、セットアップスクリプトを実行してください。

Linux/macOS：

./setup-advisor.sh

Windows：

setup-advisor.bat

スクリプトは以下を自動的に実行します。

• GPUを検出します — NVIDIAのCUDA（Linux/Windows）、Apple SiliconのMetal（macOS）を使用するか、CPUに切り替えます
• 適切なアクセラレーションバックエンドで llama-cpp-python をコンパイルします
• モデルをダウンロードします（約3.3 GB、初回のみ）。保存先は ~/.cache/mcp-logic/models/ です

venvの有効化は不要です — セットアップスクリプトは仮想環境を自動管理する uv を使用します。すべての uv run および uv pip install --directory コマンドは、事前に有効化しなくてもプロジェクトの .venv を対象にします。

手動インストール（上級者向け）

セットアップスクリプトを使わず、手動でインストールする場合：

Linux（NVIDIA GPU）：

CMAKE_ARGS="-DGGML_CUDA=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

macOS（Apple Silicon）：

CMAKE_ARGS="-DGGML_METAL=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

Windows（NVIDIA GPU、PowerShell）：

$env:CMAKE_ARGS="-DGGML_CUDA=on"
uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

CPUのみ（すべてのプラットフォーム）：

uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

モデルは初回使用時に自動ダウンロードされます。事前に手動でダウンロードすることもできます。

uv run --directory . python -c "
from huggingface_hub import hf_hub_download
hf_hub_download('webAI-Official/TwIL-LM3', 'TwIL-LM3-Q8_0.gguf',
                revision='5d90f3a3251e142fc5cc6b42a62b175fdb0d4ccd',
                local_dir='$HOME/.cache/mcp-logic/models',
                local_dir_use_symlinks=False)
"

プラットフォームの互換性

プラットフォーム	GPUアクセラレーション	備考
Linux（x86_64）	✅ CUDA（NVIDIA）	CUDA Toolkit + nvidia-smi が必要です
macOS（Apple Silicon）	✅ Metal	ARM64ネイティブのPythonを推奨します
macOS（Intel）	⚠️ Metal（制限あり）	動作しますが、Apple Siliconより遅くなります
Windows（x86_64）	✅ CUDA（NVIDIA）	CUDA Toolkit + Visual Studio Build Tools が必要です
すべてのプラットフォーム	✅ CPU	常に動作します。低速です（30億パラメーターのモデルではクエリごとに約10～20秒）

Claude Desktopとの連携

Claude DesktopのMCP設定（claude-app-config.json に自動生成）に追加します。

{
  "mcpServers": {
    "mcp-logic": {
      "command": "uv",
      "args": [
        "--directory",
        "/absolute/path/to/mcp-logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
      ]
    }
  }
}

重要： /absolute/path/to/mcp-logic を実際のリポジトリのパスに置き換えてください。

決定論的なソルバーのみのテストを行う場合、またはオプションのAdvisor依存関係がインストールされていない場合は、"--no-advisor" を追加してください。モデルは遅延読み込みされるため、通常の prove および find_model 呼び出しでGPUメモリを消費することはありません。

Codexとの連携

絶対パスを指定して、stdioサーバーをグローバルに登録します。

codex mcp add mcp-logic -- \
  /absolute/path/to/mcp-logic/.venv/bin/mcp_logic \
  --prover-path /absolute/path/to/mcp-logic/ladr/bin

codex mcp get mcp-logic で保存されたコマンドを確認してください。サーバーを追加または変更した後は、Codexを再起動して、次のセッションでツールが読み込まれるようにしてください。

利用可能なツール

ツール	目的
ask_logic_advisor 🤖	平易な英語で論理問題を解く（最初から最後まで）
prove	Prover9 を使って命題を証明する
check_well_formed	詳細なエラー情報を付けて数式の構文を検証する
find_model	前提を満たす有限モデルを見つける
find_counterexample	命題が導かれないことを示す反例を見つける
verify_commutativity	圏論的図式の可換性を表す FOL を生成する
get_category_axioms	圏・関手・群・モノイドの公理を取得する
check_contingency	HCC prover を使って真理関数的な偶然性を確認する
abductive_explain	観察に対して VFE を最小化する説明を見つける

使用例

Logic Advisor に質問する（最も簡単）

自然言語で質問するだけで、アドバイザーが形式化し、ソルバーを実行して結果を説明します：

Use ask_logic_advisor with:
question: "Is it true that if all humans are mortal and Socrates is human,
           then Socrates is mortal?"

結果： アドバイザーは FOL に変換し、Prover9 で定理を証明して、次のように返します：

「はい、ソクラテスは死すべき存在です。この証明は、すべての人間は死すべき存在であるという全称前提と、ソクラテスが人間であるという事実から導かれます。」

透明性を確保するため、使用した形式化とソルバーの生の出力も応答に含まれます。

定理を証明する（直接）

Use the prove tool with:
premises: ["all x (man(x) -> mortal(x))", "man(socrates)"]
conclusion: "mortal(socrates)"

結果： ✓ 定理が証明されました

命題論理の偶然性を分析する

Use the check_contingency tool with:
formula: "(p -> q) | (q -> p)"

結果： 数式が非偶然的な恒真式であると判定し、証明トレースを返します。

反例を見つける

Use the find_counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"

結果： P(a) は真だが P(b) は偽となるモデルが見つかり、結論が導かれないことを示します。

圏論的図式を検証する

Use the verify_commutativity tool with:
path_a: ["f", "g"]
path_b: ["h"]
object_start: "A"
object_end: "C"

結果： f∘g = h を証明するための FOL の前提と結論です。

ローカルでの実行

Claude Desktop の代わりに、サーバーを直接実行します：

Linux/macOS：

./run_mcp_logic.sh

Windows：

run_mcp_logic.bat

プロジェクト構成

mcp-logic/
├── src/mcp_logic/
│   ├── server.py              # Main MCP server (9 tools)
│   ├── logic_advisor.py       # Onboard TwIL-LM3 agentic solver
│   ├── mace4_wrapper.py       # Mace4 model finder
│   ├── syntax_validator.py    # Formula syntax validation
│   ├── categorical_helpers.py # Category theory utilities
│   ├── hcc_prover.py          # Hypersequent Contingency Calculus prover
│   ├── vfe_engine.py          # Variational Free Energy abductive engine
│   ├── formula_ast.py         # Propositional logic AST and parser
│   └── fol_ast.py             # First-order AST, parser, and transformations
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Unit, solver integration, and MCP stdio tests
├── linux-setup-script.sh      # Linux/macOS core setup
├── windows-setup-mcp-logic.bat # Windows core setup
├── setup-advisor.sh           # Linux/macOS advisor setup
├── setup-advisor.bat          # Windows advisor setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

Logic Advisor の詳細

ask_logic_advisor ツールは、3 フェーズのエージェント型パイプラインを使用します：

  Natural Language Question
         │
         ▼
  ┌─────────────────────┐
  │ 1. FORMALIZE        │  TwIL-LM3 translates to FOL
  │    (LLM call)       │  → {"tool":"prove", "premises":[...], ...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 2. EXECUTE          │  Runs actual Prover9/Mace4/HCC
  │    (Solver call)    │  → {"result":"proved", "proof":...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 3. INTERPRET        │  TwIL-LM3 explains the result
  │    (LLM call)       │  → Plain English answer
  └─────────────────────┘

• モデル：TwIL-LM3（パラメーター数 3B、形式推論向けにファインチューニング済み）
• 量子化：Q8_0 GGUF（ディスク上で約 3.3 GB、VRAM 約 3.5 GB）
• 遅延読み込み：モデルはサーバーの起動時ではなく、最初のクエリ時に読み込まれます
• ライセンス：webAI Non-Commercial License v1.0（非商用利用のみ）

必要なリソース

シナリオ	VRAM	推論速度
NVIDIA GPU（CUDA）	約 3.5 GB	LLM 呼び出しあたり約 1～3 秒
Apple Silicon（Metal）	約 3.5 GB	LLM 呼び出しあたり約 2～5 秒
CPU のみ	0（RAM を使用）	LLM 呼び出しあたり約 10～20 秒

v0.4.0 の新機能

Logic Advisor を内蔵：

• ✅ ask_logic_advisor ツール：平易な英語で論理問題を解きます。内蔵の TwIL-LM3 LLM が自動で形式化し、ソルバーを実行して結果を解釈します
• ✅ クロスプラットフォームの GPU セットアップ：CUDA（NVIDIA）または Metal（Apple Silicon）を自動検出し、それに応じてコンパイルします
• ✅ モデルの遅延読み込み：アドバイザーが初めて呼び出されるまで VRAM を使用しません
• ✅ 自動ダウンロード：モデルは初回使用時に HuggingFace からダウンロードされます

v0.3.0 の新機能

認知アーキテクチャの強化：

• ✅ 超シークエント条件計算（HCC）： 総当たりのモデル化を行わずに、命題論理式の条件を即座に評価するための厳密な演繹チェッカーを追加しました。
• ✅ 変分自由エネルギー（VFE）エンジン： 独断的でない Cournot-Gaifman 事前分布を使用して仮説を順位付けし、オッカムの剃刀を優雅に満たす、アブダクション推論を実装しました。
• ✅ スマート証明ルーティング： prove ツールは、純粋な命題論理のクエリを HCC エンジンへ、一階述語論理のクエリを Prover9 へ自動的にルーティングします。
• ✅ 設定可能なモデルファインダー： find_model と find_counterexample で、カスタムタイムアウトと構造化された述語／関数の抽出がサポートされるようになりました。
• ✅ 決定可能な断片の検索： BSR および安全に制限された単項理論では、完全な 1..model_bound 検索を実行します。no_model_found の応答が絶対的なものとなるのは、コンテキストで許可された PROVED または REFUTED のステータスがある場合に限られます。BOUNDED_NO_MODEL の応答では、有限範囲に基づく留保が維持されます。
• ✅ 理論を考慮したアドバイザールーティング： ソルバーの選択では、英語のキーワード照合ではなく、混合算術や未解釈述語を含む、解析済みの論理式の構造に従います。
• ✅ 変数スコープのリント： check_well_formed は、暗黙の全称量化や未使用の束縛変数について警告しますが、正当な Prover9 の論理式は拒否しません。

v0.2.0 の新機能

機能強化：

• ✅ Mace4 によるモデル発見と反例検出
• ✅ 位置ごとのエラーを含む詳細な構文検証
• ✅ カテゴリ的推論のサポート（圏論の公理、可換性の検証）
• ✅ すべてのツールからの構造化 JSON 出力
• ✅ 自己完結型のインストール（手動でのパス設定は不要）

開発

テストフィクスチャは、バンドルされた ladr/bin/prover9 と ladr/bin/mace4 を自動的に検出します。通常のチェックアウトでは LADR_PATH は不要です。

テストスイート全体を実行します：

.venv/bin/python -m pytest tests/ -q

サーバーを起動し、MCP ツール呼び出しを通じて Prover9 と Mace4 の両方を実行する、エンドツーエンドの MCP stdio テストのみを実行します：

.venv/bin/python -m pytest tests/test_mcp_stdio_integration.py -q

制限付きプロセスサンドボックスでは、LADR バイナリの起動は許可されても、処理の進行が妨げられることがあり、誤解を招く 30 秒または 60 秒のタイムアウトが発生します。ソルバーを使用するテストはそのようなサンドボックスの外で実行してください。ソルバーのタイムアウトを延長して対処しないでください。

ドキュメント

• mcp_logic_agent.md - エージェントガイド（ツールリファレンス＋ワークフロー）
• ENHANCEMENTS.md - v0.2.0 の機能のクイックリファレンス
• Documents/ - 詳細な分析と例

トラブルシューティング

「Prover9 not found」エラー：

• セットアップスクリプトを実行します：./linux-setup-script.sh または windows-setup-mcp-logic.bat
• ladr/bin/prover9 と ladr/bin/mace4 が存在することを確認します

ロジックアドバイザーが動作しない場合：

• アドバイザーのセットアップを実行します：./setup-advisor.sh または setup-advisor.bat
• GPU の検出を確認します：nvidia-smi（Linux／Windows）または system_profiler SPDisplaysDataType（macOS）
• CPU モードを強制します：./setup-advisor.sh --cpu
• モデルが存在することを確認します：ls ~/.cache/mcp-logic/models/TwIL-LM3-Q8_0.gguf
• 不要な場合は無効にします：サーバー引数に --no-advisor を追加します

「llama-cpp-python」のビルドに失敗する場合：

• Linux：ビルドツールをインストールします：sudo apt-get install build-essential cmake
• macOS：Xcode ツールをインストールします：xcode-select --install
• Windows：「Desktop development with C++」ワークロードを含む Visual Studio Build Tools をインストールします
• CUDA：CUDA Toolkit がインストールされ、nvcc が PATH に含まれていることを確認します

サーバーが更新されない場合：

• コードを変更した後にサーバーを再起動します
• ログに構文エラーがないか確認します

構文検証の警告：

• 述語／関数には小文字を使用します（例：Man(x) ではなく man(x)）
• 明確にするため、演算子の前後にスペースを入れます
• すべての括弧の対応を確認します

ライセンス

MIT（mcp-logic サーバー）

注記： 論理アドバイザーで使用される TwIL-LM3 モデルは、webAI Non-Commercial License v1.0 のライセンスに基づいています。このため、アドバイザー機能は非商用利用に限定されます。mcp-logic サーバーのコア機能（prove、find_model など）は引き続き MIT ライセンスであり、アドバイザーなしで商用利用できます。

クレジット

• Prover9/Mace4：William McCune の LADR ライブラリ
• LADR リポジトリ：laitep/ladr
• TwIL-LM3：webAI — 形式論理向けにファインチューニングされた 3B 推論モデル
• Hypersequent Contingency Calculus（HCC）：Eugenio Orlandelli、Giannandrea Pulcini、Achille C. Varzi（2024）による「A Hypersequent Calculus for Classical Contingencies」に基づいています。