MCP-RoCQ (Coq Reasoning Server)

基本能力

产品定位

MCP-RoCQ是一个专注于形式化验证和逻辑推理的服务，通过集成Coq证明助手提供高级逻辑推理能力。

核心功能

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

适用场景

• 形式化验证
• 逻辑推理和证明
• 编程语言理论研究
• 依赖类型系统开发

工具列表

1. type_check：检查术语是否符合预期类型
2. define_inductive：定义归纳类型并验证
3. prove_property：证明逻辑属性

常见问题解答

• 安装问题：确保正确安装Coq Platform 8.19
• 语法错误：检查输入是否符合Coq语法
• 路径配置：确保在配置文件中正确设置Coq路径

使用教程

使用依赖

1. 安装Coq Platform 8.19 (2024.10)

安装教程

1. 克隆仓库

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

1. 进入仓库目录并创建虚拟环境

uv venv
./venv/Scripts/activate
uv pip install -e .

1. 安装依赖

pip install -r requirements.txt

调试方式

1. 配置JSON文件，设置正确的Coq路径和库路径
2. 使用提供的工具进行测试

{
    "tool": "type_check",
    "args": {
        "term": "<term to check>",
        "expected_type": "<type>",
        "context": ["relevant", "modules"] 
    }
}

许可证

该项目遵循 MIT 开源许可条款，请参阅 MIT 了解完整条款。