MCP-Logic

Proporciona razonamiento automatizado para sistemas de IA utilizando los demostradores de teoremas Prover9 y Mace4.

Documentación

MCP-Logic

Un servidor MCP para razonamiento automatizado de lógica de primer orden utilizando Prover9, Mace4 y un LLM de razonamiento integrado.

Características

Demostración de Teoremas - Demuestra afirmaciones lógicas con Prover9
Búsqueda de Modelos - Encuentra modelos finitos con Mace4
Búsqueda de ContraeJemplos - Muestra por qué las afirmaciones no se deducen
Validación de Sintaxis - Pre-valida fórmulas con mensajes de error útiles
Razonamiento Categórico - Soporte integrado para demostraciones de teoría de categorías
Contingencia Proposicional - Demostrador HCC puramente analítico para comprobaciones proposicionales rápidas
Razonamiento Abductivo - Clasifica hipótesis utilizando Energía Libre Variacional (VFE)
🤖 Asesor de Lógica (NUEVO) - LLM de razonamiento TwIL-LM3 integrado que resuelve problemas de lógica de principio a fin: solo pregunta en inglés sencillo
Autocontenido - Todas las dependencias se instalan automáticamente

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

Habilitar el Asesor de Lógica (Opcional)

El asesor de lógica integrado utiliza un LLM local de 3B parámetros (TwIL-LM3 Q8) para resolver problemas de lógica de principio a fin. Ejecuta el script de configuración para instalarlo:

Linux/macOS:

./setup-advisor.sh

Windows:

setup-advisor.bat

El script automáticamente:

Detecta tu GPU — CUDA en NVIDIA (Linux/Windows), Metal en Apple Silicon (macOS), o recurre a CPU
Compila llama-cpp-python con el backend de aceleración correcto
Descarga el modelo (~3.3 GB, una sola vez) a ~/.cache/mcp-logic/models/

No se necesita activar el venv — los scripts de configuración usan uv que gestiona el entorno virtual automáticamente. Todos los comandos uv run y uv pip install --directory apuntan al .venv del proyecto sin que tengas que activarlo primero.

Instalación Manual (Avanzada)

Si prefieres instalar manualmente en lugar de usar el script de configuración:

Linux (GPU NVIDIA):

CMAKE_ARGS="-DGGML_CUDA=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

macOS (Apple Silicon):

CMAKE_ARGS="-DGGML_METAL=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

Windows (GPU NVIDIA, PowerShell):

$env:CMAKE_ARGS="-DGGML_CUDA=on"
uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

Solo CPU (cualquier plataforma):

uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

El modelo se descarga automáticamente en el primer uso, o descárgalo manualmente:

uv run --directory . python -c "
from huggingface_hub import hf_hub_download
hf_hub_download('webAI-Official/TwIL-LM3', 'TwIL-LM3-Q8_0.gguf',
                revision='5d90f3a3251e142fc5cc6b42a62b175fdb0d4ccd',
                local_dir='$HOME/.cache/mcp-logic/models',
                local_dir_use_symlinks=False)
"

Compatibilidad de Plataformas

Plataforma	Aceleración GPU	Notas
Linux (x86_64)	✅ CUDA (NVIDIA)	Requiere CUDA Toolkit + `nvidia-smi`
macOS (Apple Silicon)	✅ Metal	Se recomienda Python ARM64 nativo
macOS (Intel)	⚠️ Metal (limitado)	Funciona pero más lento que Apple Silicon
Windows (x86_64)	✅ CUDA (NVIDIA)	Requiere CUDA Toolkit + Visual Studio Build Tools
Cualquier plataforma	✅ CPU	Siempre funciona, más lento (~10-20s por consulta para modelo 3B)

Integración con Claude Desktop

Añade 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",
        "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.

Añade "--no-advisor" para pruebas deterministas solo con solucionador o cuando las dependencias opcionales del asesor no estén instaladas. El modelo se carga de forma diferida, por lo que las llamadas normales a prove y find_model no consumen memoria de GPU.

Integración con Codex

Registra el servidor stdio globalmente con rutas absolutas:

codex mcp add mcp-logic -- \
  /absolute/path/to/mcp-logic/.venv/bin/mcp_logic \
  --prover-path /absolute/path/to/mcp-logic/ladr/bin

Confirma el comando guardado con codex mcp get mcp-logic. Reinicia Codex después de añadir o cambiar el servidor para que sus herramientas se carguen en la siguiente sesión.

Herramientas Disponibles

Herramienta	Propósito
ask_logic_advisor 🤖	Resuelve problemas de lógica en inglés sencillo (de principio a fin)
prove	Demuestra afirmaciones usando Prover9
check_well_formed	Valida la sintaxis de fórmulas con errores detallados
find_model	Encuentra modelos finitos que satisfacen las premisas
find_counterexample	Encuentra contraejemplos que muestran que las afirmaciones no se deducen
verify_commutativity	Genera FOL para la conmutatividad de diagramas categóricos
get_category_axioms	Obtiene axiomas para categoría/funtor/grupo/monoide
check_contingency	Comprueba la contingencia veritativo-funcional mediante el demostrador HCC
abductive_explain	Encuentra la explicación que minimiza VFE para una observación

Ejemplo de Uso

Preguntar al Asesor de Lógica (Más Fácil)

Solo haz una pregunta en lenguaje natural — el asesor la formaliza, ejecuta el solucionador y explica el resultado:

Use ask_logic_advisor with:
question: "Is it true that if all humans are mortal and Socrates is human,
           then Socrates is mortal?"

Resultado: El asesor traduce a FOL, demuestra el teorema con Prover9 y devuelve:

"Sí, Sócrates es mortal. La demostración se deduce de la premisa universal de que todos los humanos son mortales, combinada con el hecho de que Sócrates es humano."

La respuesta también incluye la formalización utilizada y la salida cruda del solucionador para transparencia.

Demostrar un Teorema (Directo)

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

Resultado: ✓ TEOREMA DEMOSTRADO

Analizar Contingencia Proposicional

Use the 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 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 deduce.

Verificar Diagrama Categórico

Use the 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 (9 tools)
│   ├── logic_advisor.py       # Onboard TwIL-LM3 agentic solver
│   ├── 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
│   └── fol_ast.py             # First-order AST, parser, and transformations
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Unit, solver integration, and MCP stdio tests
├── linux-setup-script.sh      # Linux/macOS core setup
├── windows-setup-mcp-logic.bat # Windows core setup
├── setup-advisor.sh           # Linux/macOS advisor setup
├── setup-advisor.bat          # Windows advisor setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

Detalles del Asesor de Lógica

La herramienta ask_logic_advisor utiliza un pipeline agéntico de 3 fases:

  Natural Language Question
         │
         ▼
  ┌─────────────────────┐
  │ 1. FORMALIZE        │  TwIL-LM3 translates to FOL
  │    (LLM call)       │  → {"tool":"prove", "premises":[...], ...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 2. EXECUTE          │  Runs actual Prover9/Mace4/HCC
  │    (Solver call)    │  → {"result":"proved", "proof":...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 3. INTERPRET        │  TwIL-LM3 explains the result
  │    (LLM call)       │  → Plain English answer
  └─────────────────────┘

Modelo: TwIL-LM3 (3B parámetros, ajustado para razonamiento formal)
Cuantización: Q8_0 GGUF (~3.3 GB en disco, ~3.5 GB VRAM)
Carga diferida: El modelo se carga en la primera consulta, no al iniciar el servidor
Licencia: Licencia No Comercial webAI v1.0 (solo uso no comercial)

Requisitos de Recursos

Escenario	VRAM	Velocidad de Inferencia
GPU NVIDIA (CUDA)	~3.5 GB	~1-3s por llamada LLM
Apple Silicon (Metal)	~3.5 GB	~2-5s por llamada LLM
Solo CPU	0 (usa RAM)	~10-20s por llamada LLM

Novedades en v0.4.0

Asesor de Lógica Integrado:

✅ Herramienta ask_logic_advisor: Resuelve problemas de lógica en inglés sencillo — el LLM TwIL-LM3 integrado formaliza, ejecuta el solucionador e interpreta los resultados automáticamente
✅ Configuración de GPU multiplataforma: Detecta automáticamente CUDA (NVIDIA) o Metal (Apple Silicon) y compila en consecuencia
✅ Carga diferida del modelo: No se usa VRAM hasta que se llama al asesor por primera vez
✅ Descarga automática: El modelo se descarga de HuggingFace en el primer uso

Novedades en v0.3.0

Mejoras en la Arquitectura Cognitiva:

✅ Cálculo de Contingencia por Hipersecuentes (HCC): Añadido 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): Implementado razonamiento abductivo que clasifica hipótesis usando un prior Cournot-Gaifman no dogmático para satisfacer elegantemente la Navaja de Ockham.
✅ Enrutamiento Inteligente del Demostrador: La herramienta prove enruta automáticamente consultas proposicionales puras al motor HCC y 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.
✅ Búsqueda de Fragmentos Decidibles: Las teorías monádicas BSR y acotadas de forma segura reciben una búsqueda completa de 1..model_bound. Una respuesta no_model_found es absoluta solo con un estado PROVED o REFUTED con licencia de contexto; una respuesta BOUNDED_NO_MODEL conserva la salvaguarda de límite finito.
✅ Enrutamiento del Asesor Consciente de la Teoría: La selección del solucionador sigue la estructura de la fórmula analizada, incluyendo aritmética mixta y predicados no interpretados, en lugar de coincidencia de palabras clave en inglés.
✅ Lint de Alcance de Variables: check_well_formed advierte sobre cuantificación universal implícita y ligadores no utilizados sin rechazar fórmulas Prover9 legales.

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 de 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

Los accesorios de prueba descubren automáticamente el ladr/bin/prover9 y ladr/bin/mace4 incluidos; no se necesita LADR_PATH para una copia normal.

Ejecuta la suite completa:

.venv/bin/python -m pytest tests/ -q

Ejecuta solo la prueba MCP stdio de extremo a extremo, que inicia el servidor y ejercita tanto Prover9 como Mace4 a través de llamadas a herramientas MCP:

.venv/bin/python -m pytest tests/test_mcp_stdio_integration.py -q

Los sandboxes de procesos restringidos pueden permitir que los binarios LADR se inicien mientras les impiden avanzar, produciendo tiempos de espera engañosos de 30/60 segundos. Ejecuta las pruebas respaldadas por solucionador fuera de ese sandbox; no compenses aumentando el tiempo de espera del solucionador.

Documentación

mcp_logic_agent.md - Guía del agente (referencia de herramientas + flujos de trabajo)
ENHANCEMENTS.md - Referencia rápida para características de v0.2.0
Documents/ - Análisis detallado y ejemplos

Solución de Problemas

Error "Prover9 no encontrado":

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 existen

El asesor de lógica no funciona:

Ejecuta la configuración del asesor: ./setup-advisor.sh o setup-advisor.bat
Comprueba la detección de GPU: nvidia-smi (Linux/Windows) o system_profiler SPDisplaysDataType (macOS)
Fuerza el modo CPU: ./setup-advisor.sh --cpu
Comprueba que el modelo existe: ls ~/.cache/mcp-logic/models/TwIL-LM3-Q8_0.gguf
Desactívalo si no es necesario: añade --no-advisor a los argumentos del servidor

Fallo de compilación de "llama-cpp-python":

Linux: Instala herramientas de compilación: sudo apt-get install build-essential cmake
macOS: Instala herramientas de Xcode: xcode-select --install
Windows: Instala Visual Studio Build Tools con la carga de trabajo "Desarrollo de escritorio con C++"
CUDA: Asegúrate de que CUDA Toolkit esté instalado y nvcc esté en PATH

El servidor no se actualiza:

Reinicia el servidor después de cambios de código
Revisa los registros para detectar errores de sintaxis

Advertencias de validación de sintaxis:

Usa minúsculas para predicados/funciones (por ejemplo, man(x) no Man(x))
Añade espacios alrededor de los operadores para mayor claridad
Equilibra todos los paréntesis

Licencia

MIT (servidor mcp-logic)

Nota: El modelo TwIL-LM3 utilizado por el asesor de lógica está licenciado bajo la Licencia No Comercial webAI v1.0. Esto restringe la función del asesor a uso no comercial. El servidor principal mcp-logic (prove, find_model, etc.) permanece bajo licencia MIT y puede usarse comercialmente sin el asesor.

Créditos

Prover9/Mace4: Biblioteca LADR de William McCune
Repositorio LADR: laitep/ladr
TwIL-LM3: webAI — modelo de razonamiento de 3B ajustado para lógica formal
Cálculo de Contingencia por Hipersecuentes (HCC): Basado en "A Hypersequent Calculus for Classical Contingencies" de Eugenio Orlandelli, Giannandrea Pulcini y Achille C. Varzi (2024).