MCP-Logic

What is MCP-Logic?

MCP-Logic is an MCP server for automated first-order logic reasoning using Prover9 and Mace4. It offers theorem proving, model finding, counterexample generation, syntax validation, categorical reasoning, propositional contingency checking, and abductive reasoning — all in a self‑contained installation.

How to use MCP-Logic?

Install by cloning the repository and running the setup script (linux-setup-script.sh or windows-setup-mcp-logic.bat). For Claude Desktop, add the auto‑generated config entry to your MCP configuration. To run the server directly, use run_mcp_logic.sh (Linux/macOS) or run_mcp_logic.bat (Windows). Tools are invoked via the MCP protocol using tool names such as prove, find_model, check_contingency, and abductive_explain.

Key features of MCP-Logic

• Theorem proving with Prover9
• Finite model finding with Mace4
• Counterexample detection from premise/conclusion pairs
• Formula syntax validation with detailed error messages
• Built‑in category theory proof support
• Propositional contingency checking via HCC prover
• Abductive reasoning ranked by Variational Free Energy (VFE)
• Self‑contained: all dependencies install automatically

Use cases of MCP-Logic

• Proving logical theorems (e.g., Socrates example) as part of an AI assistant workflow.
• Finding finite models that satisfy a set of premises.
• Generating counterexamples to show that a conclusion does not follow.
• Verifying commutativity of categorical diagrams.
• Checking propositional formula contingency (tautology, contradiction, contingency) without brute force.
• Ranking explanatory hypotheses for observed data using abductive reasoning.

FAQ from MCP-Logic

What is the Hypersequent Contingency Calculus (HCC)?

HCC is a deductive checker for evaluating propositional formula contingencies instantly without brute‑force modeling. It is used by the check_contingency tool.

What is the Variational Free Energy (VFE) engine?

VFE engine implements abductive reasoning that ranks hypotheses using a non‑dogmatic Cournot‑Gaifman prior to elegantly satisfy Ockham’s Razor.

Does MCP-Logic require manually installing Prover9/Mace4?

No. The setup script automatically downloads and builds LADR binaries (prover9 and mace4) into the ladr/bin/ directory.

How do I fix "Prover9 not found"?

Run the setup script (linux-setup-script.sh or windows-setup-mcp-logic.bat) and verify that ladr/bin/prover9 exists. The server expects the --prover-path argument pointing to that directory.

What transport does MCP-Logic use?

The README does not specify the transport layer beyond launching the server as a subprocess (via uv or the run scripts), which is typical of MCP servers using stdio.