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

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",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
      ]
    }
  }
}

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

Add `"--no-advisor"` for deterministic solver-only testing or when the

optional advisor dependencies are not installed. The model is lazy-loaded, so

normal `prove` and `find_model` calls do not consume GPU memory.

Codex Integration

Register the stdio server globally with absolute paths:

codex mcp add mcp-logic -- \
  /absolute/path/to/mcp-logic/.venv/bin/mcp_logic \
  --prover-path /absolute/path/to/mcp-logic/ladr/bin

Confirm the saved command with `codex mcp get mcp-logic`. Restart Codex after

adding or changing the server so its tools are loaded into the next session.

Available Tools

Example Usage

Ask the Logic Advisor (Easiest)

Just ask a question in natural language — the advisor formalizes it, runs the solver, and explains the result:

Use ask_logic_advisor with:
question: "Is it true that if all humans are mortal and Socrates is human,
           then Socrates is mortal?"

Result: The advisor translates to FOL, proves the theorem with Prover9, and returns:

> _"Yes, Socrates is mortal. The proof follows from the universal premise that all humans are mortal, combined with the fact that Socrates is human."_

The response also includes the formalization it used and the raw solver output for transparency.

Prove a Theorem (Direct)

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

Result: ✓ THEOREM PROVED

Analyze Propositional Contingency

Use the 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 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 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 (9 tools)
│   ├── logic_advisor.py       # Onboard TwIL-LM3 agentic solver
│   ├── mace4_wrapper.py       # Mace4 model finder
│   ├── syntax_validator.py    # Formula syntax validation
│   ├── categorical_helpers.py # Category theory utilities
│   ├── hcc_prover.py          # Hypersequent Contingency Calculus prover
│   ├── vfe_engine.py          # Variational Free Energy abductive engine
│   ├── formula_ast.py         # Propositional logic AST and parser
│   └── fol_ast.py             # First-order AST, parser, and transformations
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Unit, solver integration, and MCP stdio tests
├── linux-setup-script.sh      # Linux/macOS core setup
├── windows-setup-mcp-logic.bat # Windows core setup
├── setup-advisor.sh           # Linux/macOS advisor setup
├── setup-advisor.bat          # Windows advisor setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

Logic Advisor Details

The `ask_logic_advisor` tool uses a 3-phase agentic pipeline:

Natural Language Question
         │
         ▼
  ┌─────────────────────┐
  │ 1. FORMALIZE        │  TwIL-LM3 translates to FOL
  │    (LLM call)       │  → {"tool":"prove", "premises":[...], ...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 2. EXECUTE          │  Runs actual Prover9/Mace4/HCC
  │    (Solver call)    │  → {"result":"proved", "proof":...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 3. INTERPRET        │  TwIL-LM3 explains the result
  │    (LLM call)       │  → Plain English answer
  └─────────────────────┘

• Model: TwIL-LM3 (3B params, fine-tuned for formal reasoning)
• Quantization: Q8_0 GGUF (~3.3 GB on disk, ~3.5 GB VRAM)
• Lazy loading: Model loads on first query, not at server startup
• License: webAI Non-Commercial License v1.0 (non-commercial use only)

Resource Requirements

What's New in v0.4.0

Onboard Logic Advisor:

• ✅ ask_logic_advisor tool: Solve logic problems in plain English — the onboard TwIL-LM3 LLM formalizes, runs the solver, and interprets results automatically
• ✅ Cross-platform GPU setup: Auto-detects CUDA (NVIDIA) or Metal (Apple Silicon) and compiles accordingly
• ✅ Lazy model loading: No VRAM used until the advisor is first called
• ✅ Auto-download: Model downloads from HuggingFace on first use

What's New in v0.3.0

Cognitive Architecture Enhancements:

• ✅ Hypersequent Contingency Calculus (HCC): Added a rigorous deductive checker for evaluating propositional formula contingencies instantly without brute-force modeling.
• ✅ Variational Free Energy (VFE) Engine: Implemented abductive reasoning that ranks hypotheses using a non-dogmatic Cournot-Gaifman prior to elegantly satisfy Ockham's Razor.
• ✅ Smart Prover Routing: `prove` tool automatically routes pure propositional queries to the HCC engine, and first-order queries to Prover9.
• ✅ Configurable Model Finder: `find_model` and `find_counterexample` now support custom timeouts and structured predicate/function extraction.
• ✅ Decidable Fragment Search: BSR and safely bounded monadic theories

receive a complete `1..model_bound` search. A `no_model_found` response is

absolute only with a context-licensed `PROVED` or `REFUTED` status; a

`BOUNDED_NO_MODEL` response retains the finite-bound hedge.

• ✅ Theory-aware Advisor Routing: Solver selection follows parsed formula

structure, including mixed arithmetic and uninterpreted predicates, rather

than English keyword matching.

• ✅ Variable-scope Lint: `check_well_formed` warns about implicit universal

quantification and unused binders without rejecting legal Prover9 formulas.

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

The test fixtures automatically discover the bundled `ladr/bin/prover9` and

`ladr/bin/mace4`; no `LADR_PATH` is needed for a normal checkout.

Run the complete suite:

.venv/bin/python -m pytest tests/ -q

Run only the end-to-end MCP stdio test, which starts the server and exercises

both Prover9 and Mace4 through MCP tool calls:

.venv/bin/python -m pytest tests/test_mcp_stdio_integration.py -q

Restricted process sandboxes can allow the LADR binaries to start while

preventing them from making progress, producing misleading 30/60-second

timeouts. Run solver-backed tests outside that sandbox; do not compensate by

increasing the solver timeout.

Documentation

• `mcp_logic_agent.md` - Agent guide (tool reference + workflows)
• `ENHANCEMENTS.md` - Quick reference for v0.2.0 features
• `Documents/` - Detailed analysis and examples

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

Logic advisor not working:

• Run the advisor setup: `./setup-advisor.sh` or `setup-advisor.bat`
• Check GPU detection: `nvidia-smi` (Linux/Windows) or `system_profiler SPDisplaysDataType` (macOS)
• Force CPU mode: `./setup-advisor.sh --cpu`
• Check model exists: `ls ~/.cache/mcp-logic/models/TwIL-LM3-Q8_0.gguf`
• Disable if not needed: add `--no-advisor` to server args

"llama-cpp-python" build fails:

• Linux: Install build tools: `sudo apt-get install build-essential cmake`
• macOS: Install Xcode tools: `xcode-select --install`
• Windows: Install Visual Studio Build Tools with "Desktop development with C++" workload
• CUDA: Ensure CUDA Toolkit is installed and `nvcc` is in PATH

Server not updating:

• Restart server 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 (mcp-logic server)

> Note: The TwIL-LM3 model used by the logic advisor is licensed under the webAI Non-Commercial License v1.0. This restricts the advisor feature to non-commercial use. The core mcp-logic server (prove, find_model, etc.) remains MIT-licensed and usable commercially without the advisor.

Credits

• Prover9/Mace4: William McCune's LADR library
• LADR Repository: laitep/ladr
• TwIL-LM3: webAI — 3B reasoning model fine-tuned for formal logic
• Hypersequent Contingency Calculus (HCC): Based on "A Hypersequent Calculus for Classical Contingencies" by Eugenio Orlandelli, Giannandrea Pulcini, and Achille C. Varzi (2024).