MCP-Logic
@angrysky56
About MCP-Logic
Fully functional AI Logic Calculator utilizing Prover9/Mace4 via Python based Model Context Protocol (MCP-Server)- tool for Windows, Linux, Claude App etc
Config
Add this server to your MCP-compatible client using the configuration below.
{
"mcpServers": {
"mcp-logic": {
"command": "python",
"args": [
"tests/test_enhancements.py"
]
}
}
}Tools
8Prove statements using Prover9
Validate formula syntax with detailed errors
Find finite models satisfying premises
Find counterexamples showing statements don't follow
Generate FOL for categorical diagram commutativity
Get axioms for category/functor/group/monoid
Check truth-functional contingency via HCC prover
Find the VFE-minimizing explanation for an observation
Overview
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.
Frequently asked questions
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.
Basic information
More Other MCP servers
XcodeBuildMCP
cameroncookeA Model Context Protocol (MCP) server and CLI that provides tools for agent use when working on iOS and macOS projects.
DeepMark
DeepMark helps teachers deliver rapid, consistent marking with meaningful feedback for every student — in a fraction of the time. What once took a week, now takes one free period.
🚀 Model Context Protocol (MCP) Curriculum for Beginners
microsoftThis open-source curriculum introduces the fundamentals of Model Context Protocol (MCP) through real-world, cross-language examples in .NET, Java, TypeScript, JavaScript, Rust and Python. Designed for developers, it focuses on practical techniques for building modular, scalable,
Production-ready MCP integrations for AI applications
Klavis-AIKlavis AI: MCP integration platforms that let AI agents use tools reliably at any scale
Blender
ahujasidOpen-source MCP to use Blender with any LLM
Comments