MCP-RoCQ

MIT License
2

Integrations

  • The README lists 'XML Protocol Integration' as a feature, describing it as providing 'reliable structured communication with Coq', indicating that the MCP server uses XML for protocol communication.

MCP-RoCQ(Coq推理服务器)

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

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

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

特征

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

安装

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

Related MCP Servers

  • -
    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
    • Linux
    • Apple
  • 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
  • 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
    14
    2
    TypeScript
    MIT License
  • -
    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

ID: 13cwhwe8l5