Logic (Prover9/Mace4)

by angrysky56

20 stars
401 downloads
Not rated
GitHub

About

Integrates Prover9/Mace4 for automated reasoning, theorem proving, and logical analysis.

Details

Author
angrysky56
Repository
angrysky56/mcp-logic
GitHub stars
20
Downloads
401
License
MIT License
Categories
Developer Tools, AI, Other, Knowledge Base, Productivity, Design, Search, Frontend, Project Management, Infrastructure

Jump to

- 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

Setting up with Highlight

This MCP is not yet compatible with Highlight’s one-click setup. However, you can still use it with Highlight by following these steps:

  1. Download and install Highlight from highlightai.com/download
  2. Navigate to the plugins tab and select "Add Custom Plugin"
  3. Configure the plugin with the settings below
    Plugin Name Logic (Prover9/Mace4)
    Command (node, npx, python, etc.) uv
    Arguments
    • Argument 1 --directory
    • Argument 2 /absolute/path/to/mcp-logic
    • Argument 3 run
    • Argument 4 mcp_logic
    • Argument 5 --prover-path
    • Argument 6 /absolute/path/to/mcp-logic/ladr/bin

    Please refer to the README for specific instructions on how to obtain API keys or other required environment variables.

  4. Enable "Start Automatically" if you want the plugin to start when Highlight launches

From the repository

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

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

ask_logic_advisor

Solve logic problems in plain English (end-to-end) using the onboard logic advisor.

prove

Prove statements using Prover9.

check_well_formed

Validate formula syntax with detailed error messages.

find_model

Find finite models satisfying given premises.

find_counterexample

Find counterexamples showing why statements don't follow.

verify_commutativity

Generate first-order logic for categorical diagram commutativity.

get_category_axioms

Get axioms for category, functor, group, or monoid.

check_contingency

Check truth-functional contingency via HCC prover.

abductive_explain

Find the VFE-minimizing explanation for an observation.

| Tool | Purpose |
| ------------------------ | ------------------------------------------------------ |
| ask_logic_advisor 🤖 | Solve logic problems in plain English (end-to-end) |
| 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 |
| check_contingency | Check truth-functional contingency via HCC prover |
| abductive_explain | Find the VFE-minimizing explanation for an observation |

Claude Desktop / Cursor

Paste into your MCP client config file to install this server.

{
    "mcpServers": {
        "logic (prover9/mace4)": {
            "cwd": "optional",
            "env": {},
            "args": [
                "--directory",
                "/absolute/path/to/mcp-logic",
                "run",
                "mcp_logic",
                "--prover-path",
                "/absolute/path/to/mcp-logic/ladr/bin"
            ],
            "shell": false,
            "command": "uv"
        }
    }
}

Linux

{
    "cwd": "optional",
    "env": [],
    "args": [
        "--directory",
        "/absolute/path/to/mcp-logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
    ],
    "shell": false,
    "command": "uv"
}

Macos

{
    "cwd": "optional",
    "env": [],
    "args": [
        "--directory",
        "/absolute/path/to/mcp-logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
    ],
    "shell": false,
    "command": "uv"
}

Windows

{
    "cwd": "optional",
    "env": [],
    "args": [
        "--directory",
        "/absolute/path/to/mcp-logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
    ],
    "shell": false,
    "command": "uv"
}

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

- 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)- OnboardTwIL-LM3reasoning LLM that solves logic problems end-to-end: just ask a question in plain English
- Self-Contained- All dependencies install automatically

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

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

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

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:

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

No venv activation needed— the setup scripts useuvwhich manages the virtual environment automatically. Alluv runanduv pip install --directorycommands target the project's.venvwithout you having to activate it first.

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

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

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

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

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

Add to your Claude Desktop MCP config (auto-generated atclaude-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-logicwith 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 normalproveandfind_modelcalls do not consume GPU memory.

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 withcodex mcp get mcp-logic. Restart Codex after adding or changing the server so its tools are loaded into the next session.

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.

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

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

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

Use the find_counterexample tool with: premises: ["P(a)"] conclusion: "P(b)"

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

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 thatf∘g = h.

Instead of Claude Desktop, run the server directly:

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

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

- ✅ask_logic_advisortool: 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

- ✅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:provetool automatically routes pure propositional queries to the HCC engine, and first-order queries to Prover9.
- ✅Configurable Model Finder:find_modelandfind_counterexamplenow support custom timeouts and structured predicate/function extraction.
- ✅Decidable Fragment Search:BSR and safely bounded monadic theories receive a complete1..model_boundsearch. Ano_model_foundresponse is absolute only with a context-licensedPROVEDorREFUTEDstatus; aBOUNDED_NO_MODELresponse 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_formedwarns about implicit universal quantification and unused binders without rejecting legal Prover9 formulas.

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

The test fixtures automatically discover the bundledladr/bin/prover9andladr/bin/mace4; noLADR_PATHis needed for a normal checkout.

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.

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

- Run the setup script:./linux-setup-script.shorwindows-setup-mcp-logic.bat
- Check thatladr/bin/prover9andladr/bin/mace4exist

- Run the advisor setup:./setup-advisor.shorsetup-advisor.bat
- Check GPU detection:nvidia-smi(Linux/Windows) orsystem_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-advisorto 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: InstallVisual Studio Build Toolswith "Desktop development with C++" workload
- CUDA: Ensure CUDA Toolkit is installed andnvccis in PATH

- Restart server after code changes
- Check logs for syntax errors

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

Note:The TwIL-LM3 model used by the logic advisor is licensed under thewebAI 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.

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

This is a web browser that enables your coding agent, such as Claude Code, to visit websites on your behalf and assist you in identifying bugs or creating UI test cases.

Search and evaluate MCP servers from your AI agent: quality grades, live verification status, install commands and client compatibility for 5,000+ servers.

The Brain that turns Generalist Agents into ML Experts.

MCP server for the Oyemi semantic lexicon. Provides deterministic word-to-code mapping and valence/sentiment analysis for AI agents like Claude, ChatGPT, and Gemini.

Cited compliance, legal & security intelligence for AI agents — 300+ law, regulation and standards corpora (GDPR, NIS2, AI Act, DORA) with article-level citations, plus live CVE/KEV/EPSS vulnerability context. OAuth remote server, free tier

Lightning-Fast, High-Accuracy Deep Research Agent 👉 8–10x faster 👉 Greater depth & accuracy 👉 Unlimited parallel runs

Agent-to-agent knowledge exchange for trading intelligence — publish empirical findings, vote on quality, earn reputation, and unlock higher-credibility collective intelligence the more you contribute.

Multimodal RAG for source-backed AI answers

Give your AI assistant the ability to identify cognitive blind spots. The official Model Context Protocol (MCP) server for cognitivebiaslabs.com.

A cognitive framework selector to help choose the right mental models and thinking frameworks for any situation.

No reviews yet — be the first

Sign in to leave a review

Use Google, GitHub, or an email account so ratings stay tied to real people.

Email sign in

No reviews posted yet.

Install

Add to Claude Desktop or Cursor

{
    "mcpServers": {
        "logic (prover9/mace4)": {
            "cwd": "optional",
            "env": {},
            "args": [
                "--directory",
                "/absolute/path/to/mcp-logic",
                "run",
                "mcp_logic",
                "--prover-path",
                "/absolute/path/to/mcp-logic/ladr/bin"
            ],
            "shell": false,
            "command": "uv"
        }
    }
}

More like this

Similar MCP servers you might find useful

Browse category

Sequential Thinking

Sequential Thinking is an MCP server that provides a tool for dynamic and reflective problem-solving through a structured, step-by-step thinking process. It is…

88.2k
Other

Filesystem

Filesystem is a Node.js server that implements the Model Context Protocol (MCP) for filesystem operations. It enables AI assistants to read, write, and manage…

88.1k
Other