mcp-logic

MCP-Logic is an automated reasoning server that wraps Prover9 and Mace4 for first-order logic, category theory reasoning, and abductive explanations via Variational Free Energy. The server exposes a set of tools that let you prove theorems, search for finite models, check formula syntax, verify categorical diagrams, and generate explanations for observations. Typical workflows include proving a theorem from premises, checking whether a formula is contingent, or finding a counterexample where a conclusion does not follow from premises. The tooling is designed to route first-order queries to Prover9 and propositional tasks to the Hypersequent Contingency Calculus (HCC) where appropriate, ensuring efficient and sound reasoning.

To run locally, start the Python MCP server (as shown in the installation steps). Once running, you can invoke tools such as prove, find_model, find_counterexample, check-well-formed, verify_commutativity, get_category_axioms, check_contingency, and abductive_explain via your preferred client or CLI wrapper that communicates with the server. The server returns structured JSON outputs to simplify downstream processing and integration with editors or automation pipelines.

Prerequisites:

• Git
• Python 3.8+ (virtual environments recommended)
• Build tools for Prover9/Mace4 (LADR) which the setup script will fetch/build

Step-by-step:

1. Clone the repository git clone https://github.com/angrysky56/mcp-logic cd mcp-logic

2. Run the platform-specific setup script to install dependencies and binaries

   • Linux/macOS: ./linux-setup-script.sh
   • Windows: windows-setup-mcp-logic.bat

   The setup script will:

   • Download and build LADR (Prover9 and Mace4)
   • Create a Python virtual environment
   • Install Python dependencies
   • Generate Claude Desktop config (auto-generated)

3. Activate the Python environment (if using one)

   • On Linux/macOS: source .venv/bin/activate
   • On Windows: .venv\Scripts\activate

4. Start the MCP server locally Linux/macOS: ./run_mcp_logic.sh Windows: run_mcp_logic.bat

5. Verify the server is running by querying the API/socket endpoint defined by your setup (see project docs for exact endpoints).

Note: The server relies on the LADR binaries located at ladr/bin (prover9 and mace4). If you relocate the repository, update the environment variable LADR_BIN_PATH accordingly.

Tips and common issues:

• Ensure the LADR binaries exist at the expected path (ladr/bin/prover9 and mace4). If you see 'Prover9 not found', re-run the setup script or verify paths.
• The server is self-contained; it installs dependencies automatically, but network access is required during the initial setup.
• For Claude Desktop integration, you may need to specify absolute paths to your repository and LADR binaries in the generated config file.
• If you customize the server path, keep the run scripts updated to reflect the new paths and environment.
• Use the available tools to validate formulas early: check_well_formed for syntax, find_model for finite models, and verify_commutativity for categorical diagrams.
• When using abductive_explain, you’ll get VFE-minimizing explanations, which can help rank hypotheses under a simple prior model.