MCPロジック

AIシステム向けにProver9/Mace4を用いた自動推論機能を提供するMCPサーバー。このサーバーは、クリーンなMCPインターフェースを通じて論理定理証明と論理モデル検証を可能にします。

デザイン哲学

MCP-Logicは、Prover9/Mace4への堅牢なインターフェースを提供することで、AIシステムと形式論理の間のギャップを埋めます。その特徴：

AIファースト設計：AIシステムが自動推論を実行するために特別に構築されています
知識検証：知識表現と論理的含意の形式的検証を可能にする
クリーンな統合: モデルコンテキストプロトコル (MCP) エコシステムとのシームレスな統合
深層推論：ネストされた量指定子と複数の前提を持つ複雑な論理証明のサポート
実世界アプリケーション: AI知識モデルと推論チェーンの検証に特に役立ちます

特徴

自動定理証明のためのProver9とのシームレスな統合
複雑な論理式と証明のサポート
組み込みの構文検証
クリーンなMCPサーバーインターフェース
広範なエラー処理とログ記録
AIシステムに関する知識表現と推論のサポート

簡単な例

# Prove that understanding + context leads to application
result = await prove(
    premises=[
        "all x all y (understands(x,y) -> can_explain(x,y))",
        "all x all y (can_explain(x,y) -> knows(x,y))",
        "all x all y (knows(x,y) -> believes(x,y))",
        "all x all y (believes(x,y) -> can_reason_about(x,y))",
        "all x all y (can_reason_about(x,y) & knows_context(x,y) -> can_apply(x,y))",
        "understands(system,domain)",
        "knows_context(system,domain)"
    ],
    conclusion="can_apply(system,domain)"
)
# Returns successful proof!

インストール

前提条件

Python 3.10以上
UV パッケージマネージャー
リポジトリのクローンを作成するためのGit
CMake とビルドツール（LADR/Prover9 のビルド用）

設定

このリポジトリをクローンする

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

セットアップスクリプトを実行します: Windows 実行:

windows-setup-mcp-logic.bat

Linux/macOS:

chmod +x linux-setup-script.sh
./linux-setup-script.sh

セットアップスクリプト:

依存関係をチェックします（git、cmake、ビルドツール）
外部リポジトリから LADR (Prover9/Mace4) をダウンロードします: laitep/LADR
LADRライブラリをビルドして、ladr/binディレクトリにProver9バイナリを作成します。
Python仮想環境を作成する
Dockerの有無にかかわらず実行するための構成ファイルを設定します

重要: LADR ディレクトリはリポジトリ自体には含まれておらず、セットアップスクリプトまたは手動でインストールされます。

Docker の使用 - これが正しく動作するかどうかはわかりませんが、主に Claude Desktop で直接使用するために設計されています

Docker でこのスクリプトを実行したい場合:

利用可能なポートを検索します
仮想環境をアクティブ化する
インストールされたProver9への正しいパスでサーバーを実行します

# Linux/macOS
./run-mcp-logic.sh

# Windows
run-mcp-logic.bat

これらのスクリプトは、必要な環境で Docker コンテナを構築して実行します。

クロードデスクトップ統合

Claude Desktop で MCP-Logic を使用するには、次の構成を使用します。

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

「/path/to/mcp-logic」を実際のリポジトリパスに置き換えます。

利用可能なツール

証明する

Prover9 を使用して論理証明を実行します。

{
  "tool": "prove",
  "arguments": {
    "premises": [
      "all x (man(x) -> mortal(x))",
      "man(socrates)"
    ],
    "conclusion": "mortal(socrates)"
  }
}

整形式チェック

論理ステートメントの構文を検証します。

{
  "tool": "check-well-formed",
  "arguments": {
    "statements": [
      "all x (man(x) -> mortal(x))",
      "man(socrates)"
    ]
  }
}

ドキュメント

詳細な分析と例については、ドキュメントフォルダーを参照してください。

知識から応用へ：AIシステムの理解と実践的応用に関する形式的論理分析

プロジェクト構造

mcp-logic/
├── src/
│   └── mcp_logic/
│       └── server.py   # Main MCP server implementation
├── tests/
│   ├── test_proofs.py  # Core functionality tests
│   └── test_debug.py   # Debug utilities
├── Documents/          # Analysis and documentation
├── pyproject.toml      # Python package config
├── setup-script.sh     # Setup script (installs LADR & dependencies)
├── run-mcp-logic.sh    # Docker-based run script (Linux/macOS)
├── run-mcp-logic.bat   # Docker-based run script (Windows)
├── run-mcp-logic-local.sh # Local run script (no Docker)
└── README.md           # This file

注意: setup-script.sh を実行すると、Prover9 バイナリを含む「ladr」ディレクトリが作成されますが、このディレクトリはリポジトリ自体には含まれません。

発達

テストを実行します:

uv pip install pytest
uv run pytest

ライセンス

マサチューセッツ工科大学

MCP-Logic

Integrations