MCP-RoCQ (Coq Reasoning Server)

@angrysky56

リポジトリ

基本情報

カテゴリ

推論

トランスポート

stdio

作者

angrysky56

MCP-RoCQ について

RoCQ (Coq Reasoning Server)

#coq#claude #mcp-server

MCP-RoCQ の設定

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

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

MCP-RoCQ のツール

ツール一覧はまだありません

この掲載には表示できるツール一覧がまだありません。サーバーにツールがないという意味ではありません。対応機能はプロジェクトのドキュメントをご確認ください。

ツールは 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

よくある質問

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.

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

End-to-End Agentic AI Automation Lab

MDalamin5

This repository contains hands-on projects, code examples, and deployment workflows. Explore multi-agent systems, LangChain, LangGraph, AutoGen, CrewAI, RAG, MCP, automation with n8n, and scalable agent deployment using Docker, AWS, and BentoML.

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

NeoCoder: Neo4j-Guided AI Coding Workflow