ask_logic_advisorLABSCO SUMMARY
Nine tools that turn a logic question into a machine-checked answer, not a confident guess.
The model writes the formulas, Prover9 and Mace4 decide them — so a claim that does not follow comes back as a counterexample rather than a plausible paragraph. check_well_formed exists because most failures are syntax, not logic, and catching them before the solver saves the round trip.
What it is
A server that puts Prover9 and Mace4 behind MCP tools, so premises and a conclusion go in and a proof, a model, or a counterexample comes back.
What you get
- prove — run a statement through Prover9; pure propositional queries are routed to the built-in HCC engine instead
- find_model and find_counterexample — Mace4 finds a finite model, or a case where the premises hold and the conclusion fails
- check_well_formed — catch a malformed formula before the solver runs, with the position of the error
- check_contingency — decide whether a propositional formula is a tautology, a contradiction, or contingent
- abductive_explain — rank candidate explanations for an observation by Variational Free Energy
- verify_commutativity and get_category_axioms — first-order premises for category, functor, group and monoid arguments
- ask_logic_advisor — put the question in plain English; the onboard model formalizes it, runs the solver, and explains the result
Requirements
A clone plus the setup script, which builds the Prover9/Mace4 binaries and writes the client config; the launch command points at them with --prover-path. The plain-English advisor is optional and downloads a 3.3 GB model on first use — start with --no-advisor to skip it. The server is MIT; the advisor model carries a non-commercial license.
Setup effort
Build from source — git clone https://github.com/angrysky56/mcp-logic
USE CASES
01
Checking whether a conclusion actually follows from your premises
Hand over the premises and the conclusion; a proof comes back, or a concrete model where the premises hold and the conclusion does not.
02
Asking a logic question without writing first-order syntax
Put it in plain English — the onboard model formalizes it, runs the solver, and returns the formalization it used alongside the answer.
03
Deciding if a propositional formula is a tautology
The HCC prover answers analytically instead of enumerating models, and returns the proof trace.
04
Proving a categorical diagram commutes
Give the two paths and the endpoints; you get first-order premises and a conclusion ready for the prover, with the axioms for the structure you are working in.
05
Fixing a formula the solver keeps rejecting
Validate the syntax first and get the position of the problem, plus warnings about implicit quantification and unused binders.
9 tools
Listed in project docs. Your client may show a different list.
provecheck_well_formedfind_modelfind_counterexampleverify_commutativityget_category_axiomscheck_contingencyabductive_explainBEFORE YOU INSTALL
What to know first
Tools you get
9 tools named in the project's documentation.
INSTALLATION
Connect your client
You clone this one yourself.
Server setup
TERMINAL
git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
./linux-setup-script.shMCP Clients
Claude Desktop
CLAUDE DESKTOP · JSON
{
"mcpServers": {
"mcp-logic": {
"command": "uv",
"args": [
"--directory",
"<YOUR_PATH_TO_MCP_LOGIC>",
"run",
"mcp_logic",
"--prover-path",
"<YOUR_PATH_TO_MCP_LOGIC>/ladr/bin"
]
}
}
}Codex
CODEX · TERMINAL
codex mcp add mcp-logic -- \
<YOUR_PATH_TO_MCP_LOGIC>/.venv/bin/mcp_logic \
--prover-path <YOUR_PATH_TO_MCP_LOGIC>/ladr/bin
