Skip to main content
Glama
Sign In
enesjakozh

MCP-Logic

by angrysky56
GitHub
MIT License
20
  • Linux
  • Apple
OverviewInspectNewSchemaRelated ServersReviewsScore
Need Help?View Source CodeReport Issue

Integrations

  • The MCP-Logic server is built with Python and integrates with Prover9/Mace4 to provide automated reasoning capabilities for AI systems through a clean MCP interface.

MCP-Logic

An MCP server providing automated reasoning capabilities using Prover9/Mace4 for AI systems. This server enables logical theorem proving and logical model verification through a clean MCP interface.

Design Philosophy

MCP-Logic bridges the gap between AI systems and formal logic by providing a robust interface to Prover9/Mace4. What makes it special:

  • AI-First Design: Built specifically for AI systems to perform automated reasoning
  • Knowledge Validation: Enables formal verification of knowledge representations and logical implications
  • Clean Integration: Seamless integration with the Model Context Protocol (MCP) ecosystem
  • Deep Reasoning: Support for complex logical proofs with nested quantifiers and multiple premises
  • Real-World Applications: Particularly useful for validating AI knowledge models and reasoning chains

Features

  • Seamless integration with Prover9 for automated theorem proving
  • Support for complex logical formulas and proofs
  • Built-in syntax validation
  • Clean MCP server interface
  • Extensive error handling and logging
  • Support for knowledge representation and reasoning about AI systems

Quick Example

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

Installation

Prerequisites

  • Python 3.10+
  • UV package manager
  • Git for cloning the repository
  • CMake and build tools (for building LADR/Prover9)

Setup

Clone this repository

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

Run the setup script: Windows run:

windows-setup-mcp-logic.bat

Linux/macOS:

chmod +x linux-setup-script.sh ./linux-setup-script.sh

The setup script:

  • Checks for dependencies (git, cmake, build tools)
  • Downloads LADR (Prover9/Mace4) from the external repository: laitep/LADR
  • Builds the LADR library to create Prover9 binaries in the ladr/bin directory
  • Creates a Python virtual environment
  • Sets up configuration files for running with or without Docker

IMPORTANT: The LADR directory is not included in the repository itself and will be installed through the setup script or manually.

Using Docker- no idea if this is working right, mainly designed for direct use with Claude Desktop

If you prefer to run with Docker this script:

  • Finds an available port
  • Activates the virtual environment
  • Runs the server with the correct paths to the installed Prover9
# Linux/macOS ./run-mcp-logic.sh
# Windows run-mcp-logic.bat

These scripts will build and run a Docker container with the necessary environment.

Claude Desktop Integration

To use MCP-Logic with Claude Desktop, use this configuration:

{ "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" ] } } }

Replace "/path/to/mcp-logic" with your actual repository path.

Available Tools

prove

Run logical proofs using Prover9:

{ "tool": "prove", "arguments": { "premises": [ "all x (man(x) -> mortal(x))", "man(socrates)" ], "conclusion": "mortal(socrates)" } }

check-well-formed

Validate logical statement syntax:

{ "tool": "check-well-formed", "arguments": { "statements": [ "all x (man(x) -> mortal(x))", "man(socrates)" ] } }

Documentation

See the Documents folder for detailed analysis and examples:

Project Structure

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

Note: After running setup-script.sh, a "ladr" directory will be created containing the Prover9 binaries, but this directory is not included in the repository itself.

Development

Run tests:

uv pip install pytest uv run pytest

License

MIT

This server cannot be installed

-
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 is a server that provides AI systems with automated reasoning capabilities, enabling logical theorem proving and model verification using Prover9/Mace4 through a clean MCP interface.

  1. Design Philosophy
    1. Features
      1. Quick Example
        1. Installation
          1. Prerequisites
          2. Setup
          3. Using Docker- no idea if this is working right, mainly designed for direct use with Claude Desktop
          4. Claude Desktop Integration
        2. Available Tools
          1. prove
          2. check-well-formed
        3. Documentation
          1. Project Structure
            1. Development
              1. License

                Related Resources

                Related MCP Servers

                • Deepseek Thinker MCP Server

                  ruixingshi
                  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

                • think-mcp-server

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

                • Unleash Feature Flag MCP Server

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

                • Think MCP Tool

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

                Appeared in Searches

                New MCP Servers

                ID: ok2nojolqg