What is Mcp Logic

MCP-Logic is a fully functional AI Logic Calculator that utilizes Prover9/Mace4 through a Python-based Model Context Protocol (MCP-Server). It provides automated reasoning capabilities for AI systems, enabling logical theorem proving and model verification.

Use cases

MCP-Logic is particularly useful for validating AI knowledge models, reasoning chains, and ensuring the correctness of logical implications in AI systems. It can be applied in various fields such as automated reasoning, knowledge representation, and formal verification.

How to use

To use MCP-Logic, integrate it with your AI system via the MCP interface. You can define premises and conclusions in logical formulas and invoke the proving function to validate logical implications. The server processes these inputs and returns proof results.

Key features

Key features include seamless integration with Prover9 for automated theorem proving, support for complex logical formulas, built-in syntax validation, a clean MCP server interface, extensive error handling, and logging capabilities.

Where to use

undefined

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:

• Knowledge to Application: A formal logical analysis of understanding and practical application in AI systems

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