Skip to main content
Glama
Sign In
enesjakozh
MCP-RoCQ

MCP-RoCQ

by angrysky56
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

MCP-RoCQ (Coq推論サーバー)

現在ツールが表示されていますが、何らかの理由で Claude はそれを適切に使用できません。無効な構文が一般的に問題であると思われますが、他に何か原因がある可能性もあります。

coq cli などを使って、もっと良い設定方法があるかもしれません。どなたか、この問題を解決したい方、あるいは何をしているのか分かっている方がいらっしゃいましたら、ぜひ教えてください。

MCP-RoCQは、Coq証明支援ツールとの統合により高度な論理推論機能を提供するモデルコンテキストプロトコル（MCP）サーバーです。カスタムタクティクスと自動化の両方を活用し、依存型チェック、帰納的型定義、プロパティ証明の自動化を可能にします。

特徴

  • 自動依存型チェック:複雑な依存型に対して項を検証する

  • 帰納的型定義:カスタム帰納的データ型を定義し、自動的に検証します

  • プロパティ証明: カスタム戦術と自動化を使用して論理プロパティを証明します

  • XMLプロトコル統合: Coqによる信頼性の高い構造化通信

  • 豊富なエラー処理: 型エラーや失敗した証明に関する詳細なフィードバック

Related MCP server: Chiasmus

インストール

  1. Coq Platform 8.19 (2024.10) をインストールする

Coqは形式的な証明管理システムです。数学的な定義、実行可能なアルゴリズム、定理を記述するための形式言語と、機械検証された証明を半対話的に開発するための環境を提供します。

https://github.com/coq/プラットフォーム

  1. このリポジトリをクローンします:

git clone https://github.com/angrysky56/mcp-rocq.git

リポジトリに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"
      ]
    },

これはうまくいくかもしれない。UV で実行できたが、そのほとんどは幻覚である可能性がある。

  1. 依存関係をインストールします:

pip install -r requirements.txt

使用法

サーバーは主に 3 つの機能を提供します。

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 ファイルを参照してください。

This server cannot be deployed

Claude Code, inside the Godot 4 editorFlockbay puts an AI agent in the real Godot 4 editor: it writes GDScript, runs your game and fixes what breaks. Free, or bring your own Claude Code or Codex.flockbay.comAd

Maintenance

ActivityInactive
ResponsivenessSyncing

Resources

Related MCP Connectors

Related MCP Servers

  • MCP-Logic

    angrysky56
    A
    license
    Not graded
    quality
    D
    maintenance
    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.
    47
    MIT

  • Chiasmus

    yogthos
    A
    license
    Not graded
    quality
    A
    maintenance
    MCP server that gives LLMs access to formal verification via Z3 and SWI-Prolog, plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results with mathematical certainty, and analyzes call graphs for reachability, dead code, and impact analysis.
    142 npm
    218
    Apache 2.0

  • rocq-piler

    scidonia
    A
    license
    Not graded
    quality
    D
    maintenance
    MCP server that bridges LLMs with the Rocq (Coq) proof assistant via LSP, enabling interactive theorem proving with AI.
    9
    Apache 2.0

  • Swarm Orchestrator

    Of-Arte
    A
    license
    Not graded
    quality
    C
    maintenance
    An MCP server that extends AI coding assistants with deterministic, algorithmic capabilities such as code analysis, fault localization, and formal verification, enabling an autonomous engineering team within the IDE.
    MIT

Appeared in Searches