广告合作
MCP.so
登录

MCP Logic

@angrysky56

代码仓库

基本信息

分类

其他

许可证

MIT

传输方式

stdio

作者

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

MCP Logic 配置

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

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

MCP Logic 工具

8

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.

常见问题

1

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.

2

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.

3

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.

4

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.

5

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.

评论

其他 分类下的更多 MCP 服务器

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.

Sequential Thinking

modelcontextprotocol

Model Context Protocol Servers

88.2K

Klarix Intelligence Engine

Klarix

B2B competitive intelligence, live sales battlecards, 5-axis ICP prospect fit scoring, and tech stack teardowns over MCP and REST with cited public-web evidence.

MaxKB

1Panel-dev

🔥 MaxKB is an open-source platform for building enterprise-grade agents. 强大易用的开源企业级智能体平台。

22.0K

🚀 Model Context Protocol (MCP) Curriculum for Beginners

microsoft

This 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,

16.7K
广告合作