MCP-Logic

An MCP server for automated first-order logic reasoning using Prover9 and Mace4.

Features

• Theorem Proving - Prove logical statements with Prover9
• Model Finding - Find finite models with Mace4
• Counterexample Finding - Show why statements don't follow
• Syntax Validation - Pre-validate formulas with helpful error messages
• Categorical Reasoning - Built-in support for category theory proofs
• Propositional Contingency - Purely analytical HCC prover for fast propositional checks
• Abductive Reasoning - Rank hypotheses using Variational Free Energy (VFE)
• Self-Contained - All dependencies install automatically

Quick Start

Installation

Linux/macOS:

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
./linux-setup-script.sh

Windows:

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

The setup script automatically:

• Downloads and builds LADR (Prover9 + Mace4)
• Creates Python virtual environment
• Installs all dependencies
• Generates Claude Desktop config

Claude Desktop Integration

Add to your Claude Desktop MCP config (auto-generated at claude-app-config.json):

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

Important: Replace /absolute/path/to/mcp-logic with your actual repository path.

Available Tools

Example Usage

Prove a Theorem

Use the mcp-logic prove tool with:
premises: ["all x (man(x) -> mortal(x))", "man(socrates)"]
conclusion: "mortal(socrates)"

Result: ✓ THEOREM PROVED

Analyze Propositional Contingency

Use the mcp-logic check_contingency tool with:
formula: "(p -> q) | (q -> p)"

Result: Identifies that the formula is a non-contingent tautology, returning the proof trace.

Find a Counterexample

Use the mcp-logic find-counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"

Result: Model found where P(a) is true but P(b) is false, proving the conclusion doesn't follow.

Verify Categorical Diagram

Use the mcp-logic verify-commutativity tool with:
path_a: ["f", "g"]
path_b: ["h"]
object_start: "A"
object_end: "C"

Result: FOL premises and conclusion to prove that f∘g = h.

Running Locally

Instead of Claude Desktop, run the server directly:

Linux/macOS:

./run_mcp_logic.sh

Windows:

run_mcp_logic.bat

Project Structure

mcp-logic/
├── src/mcp_logic/
│   ├── server.py              # Main MCP server (8 tools)
│   ├── mace4_wrapper.py       # Mace4 model finder
│   ├── syntax_validator.py    # Formula syntax validation
│   ├── categorical_helpers.py # Category theory utilities
│   ├── hcc_pro

... [View full README on GitHub](https://github.com/angrysky56/mcp-logic#readme)