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 -
20
MIT License
Trello MCP Server
andypost
A
security
F
license
A
quality
Enables interaction with Trello boards, lists, and cards through Model Context Protocol (MCP) tools, leveraging TypeScript for type safety and asynchronous operations.
Last updated -
5
JavaScript
MCP Server Starter
GreatAuk
A
security
A
license
A
quality
A TypeScript-based template for building Model Context Protocol servers, featuring fast testing, automated version management, and a clean structure for MCP tool implementations.
Last updated -
1
1
2
TypeScript
MIT License
MCPKit
ribeirogab
-
security
F
license
-
quality
A simple TypeScript library for creating Model Context Protocol (MCP) servers with features like type safety, parameter validation, and a minimal code API.
Last updated -
1
TypeScript
MIT License

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

Trello MCP Server

MCP Server Starter

MCPKit

Appeared in Searches

New MCP Servers

MCP directory API