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.

Related MCP server: didlogic_mcp

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)"
  }
}

cheque bien formado

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:

• Del conocimiento a la aplicación : un análisis lógico formal de la comprensión y la aplicación práctica en sistemas de IA

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)