Skip to main content
Glama
enesjakozh
angrysky56

MCP-RoCQ

by angrysky56
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

MCP-RoCQ（Coq推理服务器）

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

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

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

特征

  • 自动依赖类型检查：根据复杂的依赖类型验证术语

  • 归纳类型定义：定义并自动验证自定义归纳数据类型

  • 属性证明：使用自定义策略和自动化来证明逻辑属性

  • XML 协议集成：与 Coq 进行可靠的结构化通信

  • 丰富的错误处理：类型错误和失败证明的详细反馈

Related MCP server: Chiasmus

安装

  1. 安装 Coq 平台 8.19（2024.10）

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

https://github.com/coq/platform

  1. 克隆此存储库：

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

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

  1. 安装依赖项：

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 deployed

One endpoint for every MCP toolRayrun runs every MCP server behind one URL and holds the credentials. Each call is decided per client, tool, and argument, then recorded.ray.runAd

Maintenance

ActivityInactive
ResponsivenessNo issues

Resources

Related MCP Connectors

Related MCP Servers

  • MCP-Logic

    angrysky56
    A
    license
    Not graded
    quality
    B
    maintenance
    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.
    46
    MIT

  • Chiasmus

    yogthos
    A
    license
    Not graded
    quality
    B
    maintenance
    MCP server that gives LLMs access to formal verification via Z3 and SWI-Prolog, plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results with mathematical certainty, and analyzes call graphs for reachability, dead code, and impact analysis.
    57 npm
    213
    Apache 2.0

  • rocq-piler

    scidonia
    A
    license
    Not graded
    quality
    B
    maintenance
    MCP server that bridges LLMs with the Rocq (Coq) proof assistant via LSP, enabling interactive theorem proving with AI.
    8
    Apache 2.0

  • Swarm Orchestrator

    Of-Arte
    A
    license
    Not graded
    quality
    C
    maintenance
    An MCP server that extends AI coding assistants with deterministic, algorithmic capabilities such as code analysis, fault localization, and formal verification, enabling an autonomous engineering team within the IDE.
    MIT

Appeared in Searches