MCP-Logic

An MCP server for automated first-order logic reasoning using Prover9, Mace4, and an onboard reasoning LLM.

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)
• 🤖 Logic Advisor (NEW) - Onboard TwIL-LM3 reasoning LLM that solves logic problems end-to-end: just ask a question in plain English
• 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

Enable the Logic Advisor (Optional)

The onboard logic advisor uses a local 3B-parameter LLM (TwIL-LM3 Q8) to solve logic problems end-to-end. Run the setup script to install it:

Linux/macOS:

./setup-advisor.sh

Windows:

setup-advisor.bat

The script automatically:

• Detects your GPU — CUDA on NVIDIA (Linux/Windows), Metal on Apple Silicon (macOS), or falls back to CPU
• Compiles llama-cpp-python with the right acceleration backend
• Downloads the model (~3.3 GB, one-time) to ~/.cache/mcp-logic/models/

No venv activation needed — the setup scripts use uv which manages the virtual environment automatically. All uv run and uv pip install --directory commands target the project's .venv without you having to activate it first.

Manual Installation (Advanced)

If you prefer to install manually instead of using the setup script:

Linux (NVIDIA GPU):

CMAKE_ARGS="-DGGML_CUDA=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

macOS (Apple Silicon):

CMAKE_ARGS="-DGGML_METAL=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

Windows (NVIDIA GPU, PowerShell):

$env:CMAKE_ARGS="-DGGML_CUDA=on"
uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

CPU-only (any platform):

uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

The model auto-downloads on first use, or pre-download manually:

uv run --directory . python -c "
from huggingface_hub import hf_hub_download
hf_hub_download('webAI-Official/TwIL-LM3', 'TwIL-LM3-Q8_0.gguf',
                revision='5d90f3a3251e142fc5cc6b42a62b175fdb0d4ccd',
                local_dir='$HOME/.cache/mcp-logic/models',
                local_dir_use_symlinks=False)
"

Platform Compatibility

... View full README on GitHub