MCP-RoCQ

MCP-RoCQ (Coq推論サーバー)

現在ツールが表示されていますが、何らかの理由で Claude はそれを適切に使用できません。無効な構文が一般的に問題であると思われますが、他に何か原因がある可能性もあります。

coq cli などを使って、もっと良い設定方法があるかもしれません。どなたか、この問題を解決したい方、あるいは何をしているのか分かっている方がいらっしゃいましたら、ぜひ教えてください。

MCP-RoCQは、Coq証明支援ツールとの統合により高度な論理推論機能を提供するモデルコンテキストプロトコル（MCP）サーバーです。カスタムタクティクスと自動化の両方を活用し、依存型チェック、帰納的型定義、プロパティ証明の自動化を可能にします。

特徴

自動依存型チェック:複雑な依存型に対して項を検証する
帰納的型定義:カスタム帰納的データ型を定義し、自動的に検証します
プロパティ証明: カスタム戦術と自動化を使用して論理プロパティを証明します
XMLプロトコル統合: Coqによる信頼性の高い構造化通信
豊富なエラー処理: 型エラーや失敗した証明に関する詳細なフィードバック

インストール

Coq Platform 8.19 (2024.10) をインストールする

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

https://github.com/coq/プラットフォーム

このリポジトリをクローンします:

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

リポジトリにcd

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

Claude アプリまたは 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 で実行できたが、そのほとんどは幻覚である可能性がある。

依存関係をインストールします:

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 ファイルを参照してください。

This server cannot be installed

security - not tested

license - permissive license

quality - not tested

How are these scores calculated?

local-only server

The server can only run on the client's local machine because it depends on local resources.

MCP-RoCQ は Coq 証明アシスタントと統合され、XML プロトコル通信による自動依存型チェック、帰納的型定義、プロパティ証明を可能にします。

Related Resources

Reddit Discussion about this server

Related MCP Servers

MCP-Logic
angrysky56
-
security
A
license
-
quality
MCP-Logic is a server that provides AI systems with automated reasoning capabilities, enabling logical theorem proving and model verification using Prover9/Mace4 through a clean MCP interface.
Last updated -
20
MIT License
Trello MCP Server
andypost
A
security
F
license
A
quality
Enables interaction with Trello boards, lists, and cards through Model Context Protocol (MCP) tools, leveraging TypeScript for type safety and asynchronous operations.
Last updated -
5
JavaScript
MCP Server Starter
GreatAuk
A
security
A
license
A
quality
A TypeScript-based template for building Model Context Protocol servers, featuring fast testing, automated version management, and a clean structure for MCP tool implementations.
Last updated -
1
1
2
TypeScript
MIT License
MCPKit
ribeirogab
-
security
F
license
-
quality
A simple TypeScript library for creating Model Context Protocol (MCP) servers with features like type safety, parameter validation, and a minimal code API.
Last updated -
1
TypeScript
MIT License

View all related MCP servers

MCP-RoCQ

MCP-RoCQ (Coq推論サーバー)

現在ツールが表示されていますが、何らかの理由で Claude はそれを適切に使用できません。無効な構文が一般的に問題であると思われますが、他に何か原因がある可能性もあります。

特徴

インストール

Claude アプリまたは mcphost 構成の JSON - coq とリポジトリのインストール方法に応じてパスを設定します。

これはうまくいくかもしれない。UV で実行できたが、そのほとんどは幻覚である可能性がある。

使用法

1. 型チェック

2. 帰納的型

3. 財産証明

ライセンス

Related Resources

Related MCP Servers

MCP-Logic

Trello MCP Server

MCP Server Starter

MCPKit

Appeared in Searches

New MCP Servers

MCP directory API