MCP-RoCQ(Coq 추론 서버)

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

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

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

특징

• 자동화된 종속 유형 검사 : 복잡한 종속 유형에 대한 용어 확인

• 귀납적 유형 정의 : 사용자 정의 귀납적 데이터 유형을 정의하고 자동으로 검증합니다.

• 속성 증명 : 사용자 정의 전략 및 자동화를 사용하여 논리적 속성 증명

• XML 프로토콜 통합 : Coq를 통한 안정적인 구조화된 통신

• 풍부한 오류 처리 : 유형 오류 및 실패한 교정에 대한 자세한 피드백

Related MCP server: Chiasmus

설치

1. Coq 플랫폼 8.19(2024.10) 설치

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

https://github.com/coq/platform

2. 이 저장소를 복제하세요:

지엑스피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"
      ]
    },

이게 효과가 있을 수도 있어요. 저는 자외선으로 해봤는데, 대부분은 환각일 수도 있거든요.

3. 종속성 설치:

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