MCP-RoCQ（Coq推理服务器）
目前显示工具，但 Claude 由于某种原因无法正确使用它 - 无效语法通常似乎是问题所在，但也可能存在其他问题。
也许有更好的方法可以用 coq cli 或其他工具来解决这个问题。如果有人想尝试修复这个问题并且知道该怎么做就太好了。
MCP-RoCQ 是一个模型上下文协议服务器，通过与 Coq 证明助手集成，提供高级逻辑推理功能。它支持自动依赖类型检查、归纳类型定义和属性证明，并支持自定义策略和自动化功能。
特征
自动依赖类型检查：根据复杂的依赖类型验证术语
归纳类型定义：定义并自动验证自定义归纳数据类型
属性证明：使用自定义策略和自动化来证明逻辑属性
XML 协议集成：与 Coq 进行可靠的结构化通信
丰富的错误处理：类型错误和失败证明的详细反馈
Related MCP server: onyx-mcp-server
安装
安装 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 文件。