Lógica MCP
Un servidor MCP que proporciona capacidades de razonamiento automatizado mediante Prover9/Mace4 para sistemas de IA. Este servidor permite la demostración de teoremas lógicos y la verificación de modelos lógicos mediante una interfaz MCP sencilla.
Filosofía del diseño
MCP-Logic conecta los sistemas de IA con la lógica formal al proporcionar una interfaz robusta con Prover9/Mace4. ¿Qué lo hace especial?
- Diseño AI-First : creado específicamente para que los sistemas de IA realicen un razonamiento automatizado.
- Validación de conocimiento : permite la verificación formal de las representaciones de conocimiento y las implicaciones lógicas.
- Integración limpia : Integración perfecta con el ecosistema del Protocolo de contexto de modelo (MCP)
- Razonamiento profundo : Soporte para pruebas lógicas complejas con cuantificadores anidados y múltiples premisas
- Aplicaciones en el mundo real : particularmente útiles para validar modelos de conocimiento de IA y cadenas de razonamiento.
Características
- Integración perfecta con Prover9 para la demostración automatizada de teoremas
- Soporte para fórmulas y pruebas lógicas complejas
- Validación de sintaxis incorporada
- Interfaz de servidor MCP limpia
- Amplio manejo y registro de errores
- Apoyo a la representación del conocimiento y razonamiento sobre sistemas de IA
Ejemplo rápido
# Prove that understanding + context leads to application
result = await prove(
premises=[
"all x all y (understands(x,y) -> can_explain(x,y))",
"all x all y (can_explain(x,y) -> knows(x,y))",
"all x all y (knows(x,y) -> believes(x,y))",
"all x all y (believes(x,y) -> can_reason_about(x,y))",
"all x all y (can_reason_about(x,y) & knows_context(x,y) -> can_apply(x,y))",
"understands(system,domain)",
"knows_context(system,domain)"
],
conclusion="can_apply(system,domain)"
)
# Returns successful proof!
Instalación
Prerrequisitos
- Python 3.10+
- Gestor de paquetes UV
- Git para clonar el repositorio
- Herramientas de CMake y compilación (para compilar LADR/Prover9)
Configuración
Clonar este repositorio
git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
Ejecute el script de instalación: Windows ejecuta:
windows-setup-mcp-logic.bat
Linux/macOS:
chmod +x linux-setup-script.sh
./linux-setup-script.sh
El script de configuración:
- Comprobaciones de dependencias (git, cmake, herramientas de compilación)
- Descarga LADR (Prover9/Mace4) del repositorio externo: laitep/LADR
- Construye la biblioteca LADR para crear binarios de Prover9 en el directorio ladr/bin
- Crea un entorno virtual de Python
- Configura archivos de configuración para ejecutarse con o sin Docker
IMPORTANTE: El directorio LADR no está incluido en el repositorio en sí y se instalará a través del script de instalación o manualmente.
Uso de Docker: no tengo idea si funciona correctamente, está diseñado principalmente para uso directo con Claude Desktop.
Si prefieres ejecutar este script con Docker:
- Encuentra un puerto disponible
- Activa el entorno virtual
- Ejecuta el servidor con las rutas correctas al Prover9 instalado
# Linux/macOS
./run-mcp-logic.sh
# Windows
run-mcp-logic.bat
Estos scripts construirán y ejecutarán un contenedor Docker con el entorno necesario.
Integración de escritorio de Claude
Para utilizar MCP-Logic con Claude Desktop, utilice esta configuración:
{
"mcpServers": {
"mcp-logic": {
"command": "uv",
"args": [
"--directory",
"/path/to/mcp-logic/src/mcp_logic",
"run",
"mcp_logic",
"--prover-path",
"/path/to/mcp-logic/ladr/bin"
]
}
}
}
Reemplace "/path/to/mcp-logic" con su ruta de repositorio actual.
Herramientas disponibles
probar
Ejecute pruebas lógicas usando Prover9:
{
"tool": "prove",
"arguments": {
"premises": [
"all x (man(x) -> mortal(x))",
"man(socrates)"
],
"conclusion": "mortal(socrates)"
}
}
Validar la sintaxis de la declaración lógica:
{
"tool": "check-well-formed",
"arguments": {
"statements": [
"all x (man(x) -> mortal(x))",
"man(socrates)"
]
}
}
Documentación
Consulte la carpeta Documentos para obtener un análisis detallado y ejemplos:
Estructura del proyecto
mcp-logic/
├── src/
│ └── mcp_logic/
│ └── server.py # Main MCP server implementation
├── tests/
│ ├── test_proofs.py # Core functionality tests
│ └── test_debug.py # Debug utilities
├── Documents/ # Analysis and documentation
├── pyproject.toml # Python package config
├── setup-script.sh # Setup script (installs LADR & dependencies)
├── run-mcp-logic.sh # Docker-based run script (Linux/macOS)
├── run-mcp-logic.bat # Docker-based run script (Windows)
├── run-mcp-logic-local.sh # Local run script (no Docker)
└── README.md # This file
Nota: Después de ejecutar setup-script.sh, se creará un directorio "ladr" que contiene los binarios de Prover9, pero este directorio no está incluido en el repositorio en sí.
Desarrollo
Ejecutar pruebas:
uv pip install pytest
uv run pytest
Licencia
Instituto Tecnológico de Massachusetts (MIT)