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

Related MCP server: didlogic_mcp

Quick Start

Installation

Linux/macOS:

Windows:

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

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

Available Tools

Example Usage

Prove a Theorem

Result: ✓ THEOREM PROVED

Find a Counterexample

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

Verify Categorical Diagram

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

Running Locally

Instead of Claude Desktop, run the server directly:

Linux/macOS:

Windows:

Project Structure

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:

Test components directly:

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