MCP-Logic

MCP-Logic is an MCP server that provides automated first-order logic reasoning, model finding, and theorem proving capabilities to AI assistants like Claude Desktop and Codex. It connects MCP-compatible clients directly to automated theorem provers including Prover9 and Mace4, alongside an analytical Hypersequent Contingency Calculus engine and a Variational Free Energy abductive reasoning module. Developers, logicians, and computer scientists use this server to eliminate logical hallucination in language models by offloading formal proofs to deterministic solvers. In addition to manual logic formalization, the system supports an optional onboard local reasoning model (TwIL-LM3) to translate natural language problems into first-order logic formulas, execute underlying theorem provers, and explain proof results. The server facilitates verifying mathematical diagrams in category theory, evaluating propositional contingency, finding counterexamples, and deducing explanations through mathematically rigorous workflows.

Category: AI & LLM Tooling

Tags: automated-reasoning, logic, mace4, prover9, theorem-proving

Visit MCP-Logic

How to install and configure MCP-Logic

1. Clone the repository: bash git clone https://github.com/angrysky56/mcp-logic cd mcp-logic 2. Run the automated setup script for your operating system: - Linux/macOS: ./linux-setup-script.sh - Windows: windows-setup-mcp-logic.bat 3. (Optional) Run ./setup-advisor.sh (or setup-advisor.bat on Windows) to configure the local TwIL-LM3 reasoning advisor. 4. Add the server configuration to your Claude Desktop config file (claude-app-config.json): 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" ] } } } Replace /absolute/path/to/mcp-logic with the absolute path to your cloned repository.

What you can do with MCP-Logic

• Prove first-order logic conclusions from given premises using automated Prover9 resolution refutation. - Discover finite models and generate counterexamples via Mace4 to demonstrate why invalid arguments fail. - Check propositional logic formulas for truth-functional contingency or tautologies using the fast HCC prover. - Solve complex natural language logic puzzles end-to-end using the onboard TwIL-LM3 logic advisor tool. - Rank competing hypotheses for abductive reasoning problems using the Variational Free Energy minimization engine. - Verify commutativity of category theory diagrams by generating first-order logic axioms and path proofs.

Key facts

• Open Source
• https://github.com/angrysky56/mcp-logic
• AI & LLM Tooling, Developer Tools & Code Intelligence
• automated-reasoning, logic, mace4, prover9, theorem-proving

Part of MCP Servers

How do I install MCP-Logic?

Clone the GitHub repository and execute the provided setup script: linux-setup-script.sh on Linux or macOS, or windows-setup-mcp-logic.bat on Windows. The script builds the Prover9 and Mace4 binaries, creates a virtual environment using uv, installs Python dependencies, and generates your initial Claude Desktop configuration snippet.

What can MCP-Logic do?

MCP-Logic allows AI assistants to prove first-order logic statements using Prover9, search for finite counterexamples via Mace4, and inspect propositional contingency via Hypersequent Contingency Calculus. It also provides tools for verifying categorical diagrams, performing abductive hypothesis ranking, and interpreting natural language logic problems using an onboard language model.

Which MCP clients work with MCP-Logic?

MCP-Logic works with any client supporting standard MCP stdio servers, including Claude Desktop and Codex. Detailed configuration examples for both clients are provided in the repository documentation.

Is MCP-Logic open source?

Yes, MCP-Logic is open source on GitHub. Note that the optional onboard TwIL-LM3 advisor model is released under the webAI Non-Commercial License v1.0 and is intended for non-commercial use.