MCP-Logic

Name: MCP-Logic
Author: angrysky56

@angrysky56

关于 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

#ai #server #tool #logic #llm #claude-3-5-sonnet #mcp-server

基本信息

分类

其他

许可证

MIT

运行时

python

传输方式

stdio

发布者

angrysky56

配置

使用下面的配置,将此服务器添加到你的 MCP 客户端。

{
  "mcpServers": {
    "mcp-logic": {
      "command": "python",
      "args": [
        "tests/test_enhancements.py"
      ]
    }
  }
}

工具

Prove 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

概览

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.