MCP.so
登录

MCP-RoCQ (Coq Reasoning Server)

@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.

评论

推理 分类下的更多 MCP 服务器

🚀 Aider-MCP: AI Coding Server with Universal Auto-Detection

jacv888

Aider-MCP-Upgraded is a production-grade multi-agent AI coding system that combines Desktop Commander (DC) investigation capabilities with Aider's implementation power. Features 70%+ token reduction, modular architecture, and intelligent workflow automation through strategic agen

4

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

Deno Sandbox MCP Server

bewt85

An MCP server that allows you to run TypeScript, JavaScript, and Python code in a sandbox on your local machine using the Deno® sandbox. This server provides a controlled environment for executing code with explicit permission controls.

13

iFlytek Workflow MCP Server

iflytek

This a simple implementation of an MCP server using iFlytek. It enables calling iFlytek workflows through MCP tools.

28

🐢🚀 Node.js Sandbox MCP Server

alfonsograziano

A Node.js–based Model Context Protocol server that spins up disposable Docker containers to execute arbitrary JavaScript.

154