MCP Logic

🚀 MCP-Logic サーバー

自動化推論能力を提供するMCPサーバーです。Prover9/Mace4を使用して、AIシステムに論理推論機能を提供します。このサーバーは、シンプルなMCPインターフェースを通じて定理証明と論理モデルの検証を実現します。

🚀 クイックスタート

MCP-Logicサーバーは、AIシステムに対して自動化推論機能を提供します。以下のセクションでは、このサーバーの機能、インストール方法、使用例などについて説明します。

✨ 主な機能

• Prover9とのシームレスな統合により、定理の自動証明をサポート
• 複雑な論理式と証明をサポート
• 組み込みの構文検証機能
• MCPプロトコルに対応したクリーンなサーバーインターフェース
• 完全なエラー処理とログ記録機能
• 知識表現とAIシステムの推論分析をサポート

📦 インストール

システム要件

• オペレーティングシステム：Linux/macOS/Windows
• メモリ：少なくとも4GB RAMを推奨
• ディスク容量：少なくとも10GBの空き容量が必要

インストール手順

# プロジェクトソースコードをダウンロード
git clone https://github.com/yourusername/mcp-logic.git
cd mcp-logic

# セットアップスクリプトを実行（システムに応じて選択）
# Linux/macOSの場合：
./setup-script.sh

# Windowsの場合：
./setup-script.bat

# インストール完了後、ladrディレクトリにProver9のバイナリファイルが生成されます

💻 使用例

基本的な使用法

# 理解とコンテキストが実際に適用できることを証明する
if __name__ == "__main__":
    knowledge = [
        "すべての人間は生命を持つ生物である。",  # 前提1：man(x) → mortal(x)
        "ソクラテスは人間である。"              # 前提2：man(socrates)
    ]
    conclusion = "ソクラテスは生命を持つ。"
    run_knowledge_to_application(knowledge, conclusion)

出力結果

すべての人間は生命を持つ生物である。  # 前提1：man(x) → mortal(x)
ソクラテスは人間である。             # 前提2：man(socrates)
結論：ソクラテスは生命を持つ。       # 結論：mortal(socrates)
証明過程：
1. 前提1によれば、人間の定義からすべての人間は生命を持つことが決まっています。
2. 前提2は、ソクラテスが人間の範疇に属することを示しています。
3. したがって、論理的な推論により、ソクラテスは生命を持つという結論が導き出されます。

利用可能なツール

1. 定理証明ツール

{
  "tool": "prove-theorem",
  "arguments": {
    "premises": [
      "すべての人間は生命を持つ生物である。",
      "ソクラテスは人間である。"
    ],
    "conclusion": "ソクラテスは生命を持つ。"
  }
}

2. 構文検証ツール

{
  "tool": "check-well-formed",
  "arguments": {
    "statements": [
      "すべての人間は生命を持つ生物である。",
      "ソクラテスは人間である。"
    ]
  }
}

📚 ドキュメント

Documentsフォルダ内の詳細な分析とサンプルを参照してください。

• 知識からの応用：AIシステムにおける理解と実際の応用に関する形式論理分析

🔧 技術詳細

プロジェクト構造

mcp-logic/
├── src/
│   └── mcp_logic/
│       └── server.py           # メインのMCPサーバー実装ファイル
├── tests/
│   ├── test_proofs.py          # 核心機能のテストケース
│   └── test_debug.py           # デバッグツールのテスト
├── Documents/                  # 分析とドキュメント資料
├── pyproject.toml              # Pythonパッケージの設定ファイル
├── setup-script.sh             # セットアップスクリプト（LADRと依存関係のインストール）
├── run-mcp-logic.sh            # Dockerを使用した実行スクリプト（Linux/macOS）
├── run-mcp-logic.bat           # Dockerを使用した実行スクリプト（Windows）
├── run-mcp-logic-local.sh      # ローカルでの実行スクリプト（Dockerなし）
└── README.md                   # このプロジェクトの説明ドキュメント

注：セットアップスクリプトを実行すると、プロジェクトディレクトリにladrフォルダが生成され、Prover9のバイナリファイルが含まれますが、このフォルダはリポジトリのバージョン管理には含まれません。

開発ガイド

テストケースの実行

uv pip install pytest
uv run pytest

📄 ライセンス

このプロジェクトはMITライセンスの下で提供されています。