MCP-RoCQ

MCP-RoCQ(Coq 추론 서버)

현재는 도구가 표시되고 있지만, 어떤 이유에서인지 클로드가 도구를 제대로 사용할 수 없습니다. 일반적으로 잘못된 구문이 문제인 듯하지만, 다른 이유가 있을 수도 있습니다.

coq cli 같은 걸 사용하면 더 나은 설정 방법이 있을 수도 있겠네요. 어떻게 해야 할지 아시는 분, 직접 시도해 보시고 고쳐 주실 수 있으면 좋겠습니다.

MCP-RoCQ는 Coq 증명 지원 도구와의 통합을 통해 고급 논리 추론 기능을 제공하는 모델 컨텍스트 프로토콜 서버입니다. 사용자 지정 전략 및 자동화를 통해 자동화된 종속 유형 검사, 귀납적 유형 정의 및 속성 증명을 지원합니다.

특징

자동화된 종속 유형 검사 : 복잡한 종속 유형에 대한 용어 확인
귀납적 유형 정의 : 사용자 정의 귀납적 데이터 유형을 정의하고 자동으로 검증합니다.
속성 증명 : 사용자 정의 전략 및 자동화를 사용하여 논리적 속성 증명
XML 프로토콜 통합 : Coq를 통한 안정적인 구조화된 통신
풍부한 오류 처리 : 유형 오류 및 실패한 교정에 대한 자세한 피드백

설치

Coq 플랫폼 8.19(2024.10) 설치

Coq는 정식 증명 관리 시스템입니다. 수학적 정의, 실행 가능한 알고리즘 및 정리를 작성할 수 있는 정식 언어와 기계 검증 증명의 준대화형 개발을 위한 환경을 제공합니다.

https://github.com/coq/platform

이 저장소를 복제하세요:

지엑스피1

저장소로 cd

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

Claude 앱이나 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 라이선스에 따라 라이선스가 부여되었습니다. 자세한 내용은 라이선스 파일을 참조하세요.

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 앱이나 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