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

| Tool | Purpose | | ------------------------ | ---------------------------------------------------- | | prove | Prove statements using Prover9 | | check-well-formed | Validate formula syntax with detailed errors | | find-model | Find finite models satisfying premises | | find-counterexample | Find counterexamples showing statements don't follow | | verify-commutativity | Generate FOL for categorical diagram commutativity | | get-category-axioms | Get axioms for category/functor/group/monoid |

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

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 (6 tools)
│   ├── mace4_wrapper.py       # Mace4 model finder
│   ├── syntax_validator.py    # Formula syntax validation
│   └── categorical_helpers.py # Category theory utilities
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Test suite
├── linux-setup-script.sh      # Linux/macOS setup
├── windows-setup-mcp-logic.bat # Windows setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

What's New in v0.2.0

Enhanced Features:

✅ Mace4 model finding and counterexample detection
✅ Detailed syntax validation with position-specific errors
✅ Categorical reasoning support (category theory axioms, commutativity verification)
✅ Structured JSON output from all tools
✅ Self-contained installation (no manual path configuration)

Development

Run tests:

source .venv/bin/activate
pytest tests/ -v

Test components directly:

python tests/test_enhancements.py

Documentation

ENHANCEMENTS.md - Quick reference for v0.2.0 features
Documents/ - Detailed analysis and examples
walkthrough.md - Implementation details (in artifacts)

Troubleshooting

"Prover9 not found" error:

Run the setup script: ./linux-setup-script.sh or windows-setup-mcp-logic.bat
Check that ladr/bin/prover9 and ladr/bin/mace4 exist

Server not updating:

Restart Claude Desktop after code changes
Check logs for syntax errors

Syntax validation warnings:

Use lowercase for predicates/functions (e.g., man(x) not Man(x))
Add spaces around operators for clarity
Balance all parentheses

License

MIT

Credits

Prover9/Mace4: William McCune's LADR library
LADR Repository: laitep/ladr

MCP Servers