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