home / mcp / mcp-logic mcp server

MCP-Logic MCP Server

Self-contained MCP server for automated first-order logic reasoning with Prover9 and Mace4.

Installation

Add the following to your MCP client configuration file.

Configuration

{
  "mcpServers": {
    "angrysky56-mcp-logic": {
      "command": "./run_mcp_logic.sh",
      "args": []
    }
  }
}

You can run and use the MCP-Logic server to perform automated first-order logic reasoning with Prover9 and Mace4. This server integrates theorem proving, model finding, counterexample detection, syntax validation, and abductive reasoning, all in a self-contained package that installs dependencies automatically and exposes tools you can use from your MCP client or Claude Desktop integration.

How to use

You run the MCP-Logic server locally and connect your MCP client or Claude Desktop to its endpoints. The server provides tools for proving theorems, finding finite models, locating counterexamples, validating syntax, and performing abductive reasoning. Use it to automatically route purely propositional queries to the contingency checker and handle first-order queries with Prover9. You interact with the server by starting it on your machine and issuing requests through your MCP client using the supported tool endpoints.

How to install

Prerequisites: ensure you have a Unix-like environment (Linux or macOS) or Windows with a compatible shell. You will need Git to clone the repository and a shell to run the setup script. After setup, the server will include the required Prover9 and Mace4 binaries.

Step 1: Clone the project repository.

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

Step 2: Run the platform-specific setup script to install dependencies and build the prover binaries.

./linux-setup-script.sh
```
or for Windows:
```cmd
windows-setup-mcp-logic.bat

Step 3: Start the MCP-Logic server locally.

./run_mcp_logic.sh
```
or, on Windows:
```cmd
run_mcp_logic.bat

Configuration and runtime endpoints

You can connect via different MCP endpoints. The simplest local run starts the server so your MCP client can issue tool requests such as prove, check-well-formed, find_model, find_counterexample, verify_commutativity, get_category_axioms, check_contingency, and abductive_explain.

Additional configuration for Claude Desktop integration

If you use Claude Desktop, you can add an MCP server configuration that points to the local MCP-Logic runtime. The following example demonstrates how Claude Desktop can invoke the server from your local machine.

{
  "mcpServers": {
    "mcp-logic": {
      "command": "uv",
      "args": [
        "--directory",
        "/absolute/path/to/mcp-logic/src/mcp_logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
      ]
    }
  }
}

Running locally on different platforms

Choose the appropriate start script for your platform and run it to launch the local MCP-Logic server.

Troubleshooting tips

If you encounter issues, try these steps: ensure the setup script completed successfully, verify that the Prover9 and Mace4 binaries are present in the installed ladr/bin directory, and restart the server after code changes. For syntax validation, follow the guidelines to write readable formulas with proper predicate casing, spacing around operators, and balanced parentheses.

Project structure and runtime entries

The project bundles the server, model finder, syntax validator, category utilities, contingency prover, abductive engine, and the formulas parser. The provided run scripts start the server locally on Linux/macOS or Windows.

What's new in versions

v0.3.0 highlights cognitive architecture enhancements, including a Hypersequent Contingency Calculus checker, a Variational Free Energy abductive engine, and smart prover routing that directs propositional queries to the contingency checker and first-order queries to Prover9.

Available tools

prove

Prove logical theorems using Prover9 by supplying premises and a conclusion.

check-well-formed

Validate formula syntax with detailed error messages to help you correct mistakes.

find_model

Find finite models that satisfy given premises to demonstrate satisfiability.

find_counterexample

Identify a model where premises hold but the conclusion fails to establish non-entailed statements.

verify_commutativity

Generate first-order logic representations to verify categorical diagram commutativity.

get_category_axioms

Retrieve axioms for category theory concepts such as categories, functors, groups, and monoids.

check_contingency

Assess propositional contingencies using a dedicated HCC prover for fast truth-functional checks.

abductive_explain

Compute the VFE-minimizing explanation for an observation to support abductive reasoning.