Logic (Prover9/Mace4) MCP server

The MCP-Logic server provides automated reasoning capabilities through Prover9/Mace4 for AI systems. It enables logical theorem proving and model verification through a clean Model Context Protocol interface, allowing AI systems to perform formal validation of knowledge representations and logical implications.

Installation

Prerequisites

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

Setup Process

Clone the repository:

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

Run the appropriate setup script for your operating system:

For Windows:

windows-setup-mcp-logic.bat

For Linux/macOS:

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

These setup scripts will:

• Check for dependencies
• Download LADR (Prover9/Mace4) from the external repository
• Build the LADR library to create Prover9 binaries
• Create a Python virtual environment
• Set up configuration files

Docker Setup

To run MCP-Logic with Docker:

# Linux/macOS
./run-mcp-logic.sh

# Windows
run-mcp-logic.bat

Claude Desktop Integration

To use MCP-Logic with Claude Desktop, add 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"
      ]
    }
  }
}

Be sure to replace /path/to/mcp-logic with your actual repository path.

Using MCP-Logic

Available Tools

Proving Logical Statements

The prove tool allows you to run logical proofs using Prover9:

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

Validating Syntax

The check-well-formed tool validates logical statement syntax:

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

Example Usage

Here's an example of using the proving capabilities:

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

Running Locally

To run MCP-Logic locally without Docker:

./run-mcp-logic-local.sh

How to add this MCP server to Cursor

There are two ways to add an MCP server to Cursor. The most common way is to add the server globally in the ~/.cursor/mcp.json file so that it is available in all of your projects.

If you only need the server in a single project, you can add it to the project instead by creating or adding it to the .cursor/mcp.json file.

Adding an MCP server to Cursor globally

To add a global MCP server go to Cursor Settings > MCP and click "Add new global MCP server".

When you click that button the ~/.cursor/mcp.json file will be opened and you can add your server like this:

{
    "mcpServers": {
        "cursor-rules-mcp": {
            "command": "npx",
            "args": [
                "-y",
                "cursor-rules-mcp"
            ]
        }
    }
}

Adding an MCP server to a project

To add an MCP server to a project you can create a new .cursor/mcp.json file or add it to the existing one. This will look exactly the same as the global MCP server example above.

How to use the MCP server

Once the server is installed, you might need to head back to Settings > MCP and click the refresh button.

The Cursor agent will then be able to see the available tools the added MCP server has available and will call them when it needs to.

You can also explictly ask the agent to use the tool by mentioning the tool name and describing what the function does.