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

ライセンス

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

This server cannot be installed

security - not tested

license - permissive license

quality - not tested

hybrid server

The server is able to function both locally and remotely, depending on the configuration or use case.

MCP-Logic は、AI システムに自動推論機能を提供するサーバーであり、クリーンな MCP インターフェースを介して Prover9/Mace4 を使用して論理定理の証明とモデル検証を可能にします。

Related Resources

Reddit Discussion about this server

Related MCP Servers

Deepseek Thinker MCP Server
ruixingshi
A
security
F
license
A
quality
Provides reasoning content to MCP-enabled AI clients by interfacing with Deepseek's API or a local Ollama server, enabling focused reasoning and thought process visualization.
Last updated -
1
54
24
JavaScript
think-mcp-server
marcopesani
-
security
A
license
-
quality
A minimal MCP Server that provides Claude AI models with the 'think' tool capability, enabling better performance on complex reasoning tasks by allowing the model to pause during response generation for additional thinking steps.
Last updated -
525
1
TypeScript
MIT License
Unleash Feature Flag MCP Server
ylin6
-
security
F
license
-
quality
An MCP server that allows AI assistants to programmatically manage Unleash feature flags through natural language, enabling operations like creating, updating, and retrieving feature flags across projects.
Last updated -
5
2
TypeScript
Think MCP Tool
Rai220
-
security
-
license
-
quality
An MCP server that provides a "think" tool enabling structured reasoning for AI agents, allowing them to pause and record explicit thoughts during complex tasks or multi-step tool use.
Last updated -
1
Python
MIT License

View all related MCP servers

MCP-Logic