MCP Rocq

🚀 MCP-RoCQ（Coq 推論サーバー）

MCP-RoCQは、Coq証明アシスタントと統合することで、高度な論理推論機能を提供するモデルコンテキストプロトコルサーバーです。自動化された依存型チェック、帰納型定義、およびカスタム戦略と自動化を使用した属性証明をサポートしています。

🚀 クイックスタート

現在、表示ツールは動作していますが、Claudeが正常に動作しない場合があります。これは、構文エラーまたはその他の問題が原因である可能性があります。Coq CLIを設定するより良い方法があるかもしれません。

✨ 主な機能

• 自動化された依存型チェック：複雑な依存型の項を検証します。
• 帰納型定義：カスタム帰納データ型を定義し、自動的に検証します。
• 属性証明：カスタム戦略と自動化を使用して論理属性を証明します。
• XMLプロトコル統合：Coqとの信頼性の高い構造化通信を実現します。
• 豊富なエラー処理：詳細な型エラーと証明失敗のフィードバックを提供します。

📦 インストール

1. Coqプラットフォーム8.19（2024.10）をインストールします。

Coqは形式証明管理システムです。数学的定義、実行可能なアルゴリズム、および定理を記述するための正式な言語を提供し、機械検査証明の半対話的開発環境を提供します。

https://github.com/coq/platform

2. このリポジトリをクローンします：

git clone https://github.com/angrysky56/mcp-rocq.git

リポジトリディレクトリに移動します。

uv venv
./venv/Scripts/activate
uv pip install -e .

3. 依存関係をインストールします。

pip install -r requirements.txt

JSON設定例（Claudeアプリケーションまたはmcphost設定用）——実際のインストールパスに合わせて設定してください。

    "mcp-rocq": {
      "command": "uv",
      "args": [
        "--directory",
        "F:/GithubRepos/mcp-rocq",
        "run",
        "mcp_rocq",
        "--coq-path",
        "F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe",
        "--lib-path",
        "F:/Coq-Platform~8.19~2024.10/lib/coq"
      ]
    },

💻 使用例

基本的な使用法

1. 型チェック

{
    "tool": "type_check",
    "args": {
        "term": "<チェック対象の項>",
        "expected_type": "<期待される型>",
        "context": ["関連モジュール"]
    }
}

2. 帰納型定義

{
    "tool": "define_inductive",
    "args": {
        "name": "Tree",
        "constructors": [
            "Leaf : Tree",
            "Node : Tree -> Tree -> Tree"
        ],
        "verify": true
    }
}

3. 属性証明

{
    "tool": "prove_property",
    "args": {
        "property": "<属性の陳述>",
        "tactics": ["<戦略のシーケンス>"],
        "use_automation": true
    }
}

📄 ライセンス

このプロジェクトはMITライセンスの下で公開されています。詳細はLICENSEファイルを参照してください。