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)"
]
}
}
ドキュメント
詳細な分析と例については、ドキュメントフォルダーを参照してください。
プロジェクト構造
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
ライセンス
マサチューセッツ工科大学