MCP-Logic

Prover9とMace4を使用した自動一階述語論理推論のためのMCPサーバーです。

機能

• 定理証明 - Prover9を使用して論理的命題を証明

• モデル探索 - Mace4を使用して有限モデルを探索

• 反例探索 - 命題が成立しない理由を提示

• 構文検証 - 有用なエラーメッセージで数式を事前検証

• 圏論的推論 - 圏論の証明を組み込みでサポート

• 命題の偶然性 - 高速な命題チェックのための純粋な分析的HCCプルーバー

• アブダクション推論 - 変分自由エネルギー（VFE）を使用して仮説をランク付け

• 自己完結型 - すべての依存関係が自動的にインストールされます

Related MCP server: warrant-mcp

クイックスタート

インストール

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設定の生成

Claude Desktopとの統合

Claude DesktopのMCP設定（claude-app-config.jsonに自動生成されます）に追加してください：

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

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

利用可能なツール

使用例

定理の証明

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

結果: ✓ 定理証明完了

命題の偶然性の分析

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

結果: 数式が偶然ではないトートロジーであることを特定し、証明トレースを返します。

反例の探索

Use the mcp-logic find-counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"

結果: P(a) は真だが P(b) は偽であるモデルが見つかり、結論が導かれないことが証明されました。

圏論的図式の検証

Use the mcp-logic 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 (8 tools)
│   ├── 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
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Test suite
├── linux-setup-script.sh      # Linux/macOS setup
├── windows-setup-mcp-logic.bat # Windows setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

v0.3.0の新機能

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

• ✅ ハイパーシーケント偶然性計算 (HCC): 総当たりモデル探索を行わずに、命題論理式の偶然性を即座に評価するための厳密な演繹チェッカーを追加しました。

• ✅ 変分自由エネルギー (VFE) エンジン: オッカムの剃刀をエレガントに満たすために、Cournot-Gaifman事前分布を使用して仮説をランク付けするアブダクション推論を実装しました。

• ✅ スマートプルーバールーティング: prove ツールは、純粋な命題クエリをHCCエンジンに、一階述語論理クエリをProver9に自動的にルーティングします。

• ✅ 設定可能なモデル探索: find_model および find_counterexample が、カスタムタイムアウトと構造化された述語/関数抽出をサポートするようになりました。

v0.2.0の新機能

強化された機能:

• ✅ Mace4によるモデル探索と反例検出

• ✅ 位置指定エラーによる詳細な構文検証

• ✅ 圏論的推論のサポート（圏論の公理、可換性の検証）

• ✅ すべてのツールからの構造化されたJSON出力

• ✅ 自己完結型のインストール（手動パス設定不要）

開発

テストの実行:

source .venv/bin/activate
pytest tests/ -v

コンポーネントの直接テスト:

python tests/test_enhancements.py

ドキュメント

• ENHANCEMENTS.md - v0.2.0機能のクイックリファレンス

• Documents/ - 詳細な分析と例

• walkthrough.md - 実装の詳細（アーティファクト内）

トラブルシューティング

「Prover9 not found」エラー:

• セットアップスクリプトを実行してください: ./linux-setup-script.sh または windows-setup-mcp-logic.bat

• ladr/bin/prover9 と ladr/bin/mace4 が存在することを確認してください

サーバーが更新されない:

• コード変更後にサーバーを再起動してください

• ログで構文エラーを確認してください

構文検証の警告:

• 述語/関数には小文字を使用してください（例: Man(x) ではなく man(x)）

• 明確にするために演算子の周りにスペースを追加してください

• すべての括弧の対応を確認してください

ライセンス

MIT

クレジット

• Prover9/Mace4: William McCune氏のLADRライブラリ

• LADRリポジトリ: laitep/ladr

• ハイパーシーケント偶然性計算 (HCC): Eugenio Orlandelli, Giannandrea Pulcini, Achille C. Varzi (2024) による「A Hypersequent Calculus for Classical Contingencies」の論理フレームワークに基づく。