MCP-Logic

Un servidor MCP para el razonamiento lógico de primer orden automatizado utilizando Prover9 y Mace4.

Características

• Demostración de teoremas - Demuestra enunciados lógicos con Prover9

• Búsqueda de modelos - Encuentra modelos finitos con Mace4

• Búsqueda de contraejemplos - Muestra por qué los enunciados no se cumplen

• Validación de sintaxis - Prevalida fórmulas con mensajes de error útiles

• Razonamiento categórico - Soporte integrado para demostraciones de teoría de categorías

• Contingencia proposicional - Probador HCC puramente analítico para comprobaciones proposicionales rápidas

• Razonamiento abductivo - Clasifica hipótesis utilizando Energía Libre Variacional (VFE)

• Autocontenido - Todas las dependencias se instalan automáticamente

Related MCP server: warrant-mcp

Inicio rápido

Instalación

Linux/macOS:

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
./linux-setup-script.sh

Windows:

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
windows-setup-mcp-logic.bat

El script de configuración automáticamente:

• Descarga y compila LADR (Prover9 + Mace4)

• Crea un entorno virtual de Python

• Instala todas las dependencias

• Genera la configuración de Claude Desktop

Integración con Claude Desktop

Añádelo a tu configuración MCP de Claude Desktop (generada automáticamente en claude-app-config.json):

{
  "mcpServers": {
    "mcp-logic": {
      "command": "uv",
      "args": [
        "--directory",
        "/absolute/path/to/mcp-logic/src/mcp_logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
      ]
    }
  }
}

Importante: Reemplaza /absolute/path/to/mcp-logic con la ruta real de tu repositorio.

Herramientas disponibles

Ejemplo de uso

Demostrar un teorema

Use the mcp-logic prove tool with:
premises: ["all x (man(x) -> mortal(x))", "man(socrates)"]
conclusion: "mortal(socrates)"

Resultado: ✓ TEOREMA DEMOSTRADO

Analizar la contingencia proposicional

Use the mcp-logic check_contingency tool with:
formula: "(p -> q) | (q -> p)"

Resultado: Identifica que la fórmula es una tautología no contingente, devolviendo el rastro de la demostración.

Encontrar un contraejemplo

Use the mcp-logic find-counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"

Resultado: Modelo encontrado donde P(a) es verdadero pero P(b) es falso, demostrando que la conclusión no se cumple.

Verificar un diagrama categórico

Use the mcp-logic verify-commutativity tool with:
path_a: ["f", "g"]
path_b: ["h"]
object_start: "A"
object_end: "C"

Resultado: Premisas y conclusión FOL para demostrar que f∘g = h.

Ejecución local

En lugar de Claude Desktop, ejecuta el servidor directamente:

Linux/macOS:

./run_mcp_logic.sh

Windows:

run_mcp_logic.bat

Estructura del proyecto

mcp-logic/
├── src/mcp_logic/
│   ├── server.py              # Main MCP server (8 tools)
│   ├── mace4_wrapper.py       # Mace4 model finder
│   ├── syntax_validator.py    # Formula syntax validation
│   ├── categorical_helpers.py # Category theory utilities
│   ├── hcc_prover.py          # Hypersequent Contingency Calculus prover
│   ├── vfe_engine.py          # Variational Free Energy abductive engine
│   └── formula_ast.py         # Propositional logic AST and parser
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Test suite
├── linux-setup-script.sh      # Linux/macOS setup
├── windows-setup-mcp-logic.bat # Windows setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

Novedades en v0.3.0

Mejoras en la arquitectura cognitiva:

• ✅ Cálculo de contingencia de hipersecuentes (HCC): Se añadió un comprobador deductivo riguroso para evaluar contingencias de fórmulas proposicionales al instante sin modelado por fuerza bruta.

• ✅ Motor de Energía Libre Variacional (VFE): Se implementó un razonamiento abductivo que clasifica hipótesis utilizando una prioridad no dogmática de Cournot-Gaifman para satisfacer elegantemente la Navaja de Ockham.

• ✅ Enrutamiento inteligente de probadores: La herramienta prove enruta automáticamente las consultas proposicionales puras al motor HCC, y las consultas de primer orden a Prover9.

• ✅ Buscador de modelos configurable: find_model y find_counterexample ahora admiten tiempos de espera personalizados y extracción estructurada de predicados/funciones.

Novedades en v0.2.0

Características mejoradas:

• ✅ Búsqueda de modelos y detección de contraejemplos con Mace4

• ✅ Validación de sintaxis detallada con errores específicos de posición

• ✅ Soporte para razonamiento categórico (axiomas de teoría de categorías, verificación de conmutatividad)

• ✅ Salida JSON estructurada de todas las herramientas

• ✅ Instalación autocontenida (sin configuración manual de rutas)

Desarrollo

Ejecutar pruebas:

source .venv/bin/activate
pytest tests/ -v

Probar componentes directamente:

python tests/test_enhancements.py

Documentación

• ENHANCEMENTS.md - Referencia rápida para las características de v0.2.0

• Documents/ - Análisis detallado y ejemplos

• walkthrough.md - Detalles de implementación (en artefactos)

Solución de problemas

Error "Prover9 not found":

• Ejecuta el script de configuración: ./linux-setup-script.sh o windows-setup-mcp-logic.bat

• Comprueba que ladr/bin/prover9 y ladr/bin/mace4 existan

El servidor no se actualiza:

• Reinicia el servidor después de realizar cambios en el código

• Revisa los registros en busca de errores de sintaxis

Advertencias de validación de sintaxis:

• Usa minúsculas para predicados/funciones (ej. man(x) no Man(x))

• Añade espacios alrededor de los operadores para mayor claridad

• Equilibra todos los paréntesis

Licencia

MIT

Créditos

• Prover9/Mace4: Biblioteca LADR de William McCune

• Repositorio LADR: laitep/ladr

• Cálculo de contingencia de hipersecuentes (HCC): Basado en el marco lógico de "A Hypersequent Calculus for Classical Contingencies" de Eugenio Orlandelli, Giannandrea Pulcini y Achille C. Varzi (2024).