MCP-RoCQ (Coq Reasoning Server)

Name: MCP-RoCQ (Coq Reasoning Server)
Author: angrysky56

@angrysky56

リポジトリ

MCP-RoCQ (Coq Reasoning Server) について

RoCQ (Coq Reasoning Server)

#coq #claude #mcp-server

基本情報

カテゴリ

推論

トランスポート

stdio

公開者

angrysky56

設定

以下の設定を使って、このサーバーを MCP 対応クライアントに追加してください。

{
  "mcpServers": {
    "mcp-rocq": {
      "command": "uv",
      "args": [
        "venv"
      ]
    }
  }
}

ツール

ツールは検出されませんでした

ツールは README から自動的に抽出されます。メンテナーは ## Tools という見出しの下に記載することで、このタブに反映できます。

概要

What is MCP-RoCQ?

MCP-RoCQ is a Model Context Protocol server that provides advanced logical reasoning capabilities through integration with the Coq proof assistant. It enables automated dependent type checking, inductive type definitions, and property proving with both custom tactics and automation.

How to use MCP-RoCQ?

Install the Coq Platform 8.19 (2024.10), clone the repository, set up a uv virtual environment, install the package with uv pip install -e ., and configure the server with the --coq-path and --lib-path arguments in your MCP client JSON. The server exposes three tools: type_check, define_inductive, and prove_property.

Key features of MCP-RoCQ

Automated dependent type checking
Inductive type definition with verification
Property proving using custom tactics and automation
XML protocol integration for structured communication with Coq
Rich error handling for type errors and failed proofs

Use cases of MCP-RoCQ

Verify terms against complex dependent types in Coq
Define and automatically verify custom inductive data types
Prove logical properties using automated or custom tactic sequences

FAQ from MCP-RoCQ

What does MCP-RoCQ integrate with?

It integrates with the Coq proof assistant (Coq Platform 8.19, 2024.10 release) through the coqtop executable and Coq library paths.

What dependencies are required?

You need the Coq Platform 8.19, Python, uv, and the cloned repository. A JSON configuration example shows paths to coqtop.exe and the Coq library directory.

What tools does the server provide?

Three main tools: type_check (verify a term against an expected type), define_inductive (define and verify inductive types), and prove_property (prove a logical statement using tactics and optional automation).

Is the server fully functional?

The README notes that while tools are shown, Claude may not use them properly due to invalid syntax, and the author suggests others may want to fix the setup. The server is experimental and contributions are welcome.

How is communication with Coq handled?

The server uses XML protocol integration for reliable structured communication with Coq.

「推論」の他のコンテンツ

n8n Workflow Builder MCP Server

salacoste

AI-powered n8n workflow automation through natural language. MCP server enabling Claude AI & Cursor IDE to create, manage, and monitor workflows via Model Context Protocol. Multi-instance support, 17 tools, comprehensive docs. Build workflows conversationally without manual JSON

229