広告掲載
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.

コメント

「その他」の他のコンテンツ

Soar Flight Booking MCP

Soar Flight Booking MCP is a remote MCP server available at https://mcp.soar.flights.

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.

P

PickFu MCP

PickFu MCP is a Model Context Protocol (MCP) server that connects AI assistants, developers, marketers, product managers, and AI agents to PickFu's consumer research platform. It enables users to create surveys, conduct

EverArt

modelcontextprotocol

Model Context Protocol Servers

88.1K

Volley.sh

Volley

A good sequence diagram can solve almost any communication problem in engineering. Volley lets your agent write them as plain text, with the real request and response payloads on every arrow. It checks its own syntax wi

広告掲載