MCP-RoCQ (Servidor de razonamiento Coq)

Name: MCP-RoCQ
Author: angrysky56

Actualmente se muestran herramientas, pero Claude no puede usarlas correctamente por alguna razón: la sintaxis no válida generalmente parece ser el problema, pero podría haber algo más.

Quizás haya una mejor manera de configurar esto con la CLI de Coq o algo similar. Si alguien sabe lo que hace y quiere intentar solucionarlo, sería genial.

MCP-RoCQ es un servidor de Protocolo de Contexto de Modelo que proporciona capacidades avanzadas de razonamiento lógico mediante la integración con el asistente de pruebas Coq. Permite la verificación automatizada de tipos dependientes, la definición inductiva de tipos y la verificación de propiedades con tácticas personalizadas y automatización.

Características

Comprobación automatizada de tipos dependientes : verifique términos contra tipos dependientes complejos
Definición de tipo inductivo : defina y verifique automáticamente tipos de datos inductivos personalizados
Comprobación de propiedades : pruebe propiedades lógicas utilizando tácticas personalizadas y automatización
Integración del protocolo XML : comunicación estructurada confiable con Coq
Manejo de errores enriquecido : comentarios detallados sobre errores de tipo y pruebas fallidas

Related MCP server: onyx-mcp-server

Instalación

Instalar la plataforma Coq 8.19 (2024.10)

Coq es un sistema de gestión de pruebas formales. Proporciona un lenguaje formal para escribir definiciones matemáticas, algoritmos ejecutables y teoremas, junto con un entorno para el desarrollo semiinteractivo de pruebas verificadas por máquina.

https://github.com/coq/platform

Clonar este repositorio:

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

cd al repositorio

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

JSON para la aplicación Claude o configuración de mcphost: configure sus rutas de acuerdo con cómo instaló coq y el repositorio.

"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" ] },

Esto podría funcionar. Lo hice funcionar con luz ultravioleta y la mayor parte de esto podría ser alucinante.

Instalar dependencias:

pip install -r requirements.txt

Uso

El servidor proporciona tres capacidades principales:

1. Comprobación de tipos

{ "tool": "type_check", "args": { "term": "<term to check>", "expected_type": "<type>", "context": ["relevant", "modules"] } }

2. Tipos inductivos

{ "tool": "define_inductive", "args": { "name": "Tree", "constructors": [ "Leaf : Tree", "Node : Tree -> Tree -> Tree" ], "verify": true } }

3. Prueba de propiedad

{ "tool": "prove_property", "args": { "property": "<statement>", "tactics": ["<tactic sequence>"], "use_automation": true } }

Licencia

Este proyecto está licenciado bajo la licencia MIT: consulte el archivo de LICENCIA para obtener más detalles.

This server cannot be installed

-

security - not tested

A

license - permissive license

-

quality - not tested

How are these scores calculated?

Resources

GitHub Repository

Need Help?

Report Issue

Reddit Discussion

Related Servers

MCP-RoCQ