MCP-RoCQ (Coq Reasoning Server)

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

現在、ツールは表示されますが、何らかの理由で Claude はうまく使えません。一般的には構文が無効であることが原因のようですが、ほかにも問題があるかもしれません。

coq cli などを使って設定する、もっとよい方法があるかもしれません。 詳しい方で、修正を試してくださる方がいれば助かります。

MCP-RoCQ は、Coq 証明アシスタントとの統合を通じて高度な論理推論機能を提供する Model Context Protocol サーバーです。自動化された依存型チェック、帰納型の定義、カスタムタクティクと自動化による性質の証明が可能になります。

機能

• 自動依存型チェック：複雑な依存型に対して項を検証します
• 帰納型の定義：カスタム帰納データ型を定義し、自動的に検証します
• 性質の証明：カスタムタクティクと自動化を使って論理的性質を証明します
• XML プロトコル統合：Coq と信頼性の高い構造化通信を行います
• 詳細なエラー処理：型エラーや証明の失敗について、詳しいフィードバックを提供します

インストール

1. Coq Platform 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 .

Claude App または mcphost の設定用 JSON。Coq とリポジトリのインストール先に合わせてパスを設定してください。

    "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"
      ]
    },

これはうまくいくかもしれません。uv で動作させましたが、この内容の大部分は幻覚かもしれません：

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

pip install -r requirements.txt

使用方法

このサーバーは、主に次の 3 つの機能を提供します：

1. 型チェック

{
    "tool": "type_check",
    "args": {
        "term": "<term to check>",
        "expected_type": "<type>",
        "context": ["relevant", "modules"] 
    }
}

2. 帰納型

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

3. 性質の証明

{
    "tool": "prove_property",
    "args": {
        "property": "<statement>",
        "tactics": ["<tactic sequence>"],
        "use_automation": true
    }
}

ライセンス

このプロジェクトは MIT ライセンスのもとでライセンスされています。詳細については LICENSE ファイルをご覧ください。