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 文件。