MCP-RoCQ

MCP-RoCQ（Coq推理服务器）

目前显示工具，但 Claude 由于某种原因无法正确使用它 - 无效语法通常似乎是问题所在，但也可能存在其他问题。

也许有更好的方法可以用 coq cli 或其他工具来解决这个问题。如果有人想尝试修复这个问题并且知道该怎么做就太好了。

MCP-RoCQ 是一个模型上下文协议服务器，通过与 Coq 证明助手集成，提供高级逻辑推理功能。它支持自动依赖类型检查、归纳类型定义和属性证明，并支持自定义策略和自动化功能。

特征

自动依赖类型检查：根据复杂的依赖类型验证术语
归纳类型定义：定义并自动验证自定义归纳数据类型
属性证明：使用自定义策略和自动化来证明逻辑属性
XML 协议集成：与 Coq 进行可靠的结构化通信
丰富的错误处理：类型错误和失败证明的详细反馈

安装

安装 Coq 平台 8.19（2024.10）

Coq 是一个形式化证明管理系统。它提供了一种用于编写数学定义、可执行算法和定理的形式化语言，并提供了一个用于机器验证证明的半交互式开发环境。

https://github.com/coq/platform

克隆此存储库：

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

cd 到 repo

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

这可能有效——我用紫外线照射它，但其中大部分可能是幻觉：

安装依赖项：

pip install -r requirements.txt

用法

该服务器提供三种主要功能：

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 -
32
MIT License
onyx-mcp-server
lupuletic
A
security
A
license
A
quality
Connect your MCP-compatible clients to Onyx AI knowledge bases for enhanced semantic search and chat capabilities. Retrieve relevant context from your documents seamlessly, enabling powerful interactions and comprehensive answers. Streamline knowledge management and improve access to information acr
Last updated -
2
25
18
MIT License
Chain of Thought MCP Server
beverm2391
-
security
F
license
-
quality
An MCP server that uses Groq's API to expose raw chain-of-thought tokens from Qwen's qwq model, enabling LLMs to think step-by-step before responding.
Last updated -
11
Calculator MCP Server
mzdz
-
security
F
license
-
quality
Provides basic arithmetic operations and advanced mathematical functions through the Model Context Protocol (MCP), with features like calculation history tracking and expression evaluation.
Last updated -

View all related MCP servers

MCP-RoCQ

MCP-RoCQ（Coq推理服务器）

目前显示工具，但 Claude 由于某种原因无法正确使用它 - 无效语法通常似乎是问题所在，但也可能存在其他问题。

特征

安装

Claude App 或 mcphost 配置的 JSON - 根据您安装 coq 和存储库的方式设置您的路径。

这可能有效——我用紫外线照射它，但其中大部分可能是幻觉：

用法

1.类型检查

2. 归纳类型

3. 财产证明

执照

Related Resources

Related MCP Servers

MCP-Logic

onyx-mcp-server

Chain of Thought MCP Server

Calculator MCP Server

Appeared in Searches

New MCP Servers

MCP directory API