Skip to main content
Glama

MCP-Logic

MIT License
20
  • Linux
  • Apple

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

imagen

# 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!

imagen

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

imagen

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:

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)

-
security - not tested
A
license - permissive license
-
quality - not tested

hybrid server

The server is able to function both locally and remotely, depending on the configuration or use case.

MCP-Logic es un servidor que proporciona a los sistemas de IA capacidades de razonamiento automatizado, lo que permite la demostración de teoremas lógicos y la verificación de modelos utilizando Prover9/Mace4 a través de una interfaz MCP limpia.

  1. Filosofía del diseño
    1. Características
      1. Ejemplo rápido
        1. Instalación
          1. Prerrequisitos
          2. Configuración
          3. Uso de Docker: no tengo idea si funciona correctamente, está diseñado principalmente para uso directo con Claude Desktop.
          4. Integración de escritorio de Claude
        2. Herramientas disponibles
          1. probar
          2. cheque bien formado
        3. Documentación
          1. Estructura del proyecto
            1. Desarrollo
              1. Licencia

                Related MCP Servers

                • A
                  security
                  F
                  license
                  A
                  quality
                  Provides reasoning content to MCP-enabled AI clients by interfacing with Deepseek's API or a local Ollama server, enabling focused reasoning and thought process visualization.
                  Last updated -
                  1
                  54
                  24
                  JavaScript
                • -
                  security
                  A
                  license
                  -
                  quality
                  A minimal MCP Server that provides Claude AI models with the 'think' tool capability, enabling better performance on complex reasoning tasks by allowing the model to pause during response generation for additional thinking steps.
                  Last updated -
                  525
                  1
                  TypeScript
                  MIT License
                  • Apple
                • -
                  security
                  F
                  license
                  -
                  quality
                  An MCP server that allows AI assistants to programmatically manage Unleash feature flags through natural language, enabling operations like creating, updating, and retrieving feature flags across projects.
                  Last updated -
                  5
                  2
                  TypeScript
                • -
                  security
                  -
                  license
                  -
                  quality
                  An MCP server that provides a "think" tool enabling structured reasoning for AI agents, allowing them to pause and record explicit thoughts during complex tasks or multi-step tool use.
                  Last updated -
                  1
                  Python
                  MIT License

                View all related MCP servers

                MCP directory API

                We provide all the information about MCP servers via our MCP API.

                curl -X GET 'https://glama.ai/api/mcp/v1/servers/angrysky56/mcp-logic'

                If you have feedback or need assistance with the MCP directory API, please join our Discord server