Claude Desktop
Desktop · Freemium · Proprietary
Anthropic's official Claude AI desktop application. Supports MCP servers to extend functionality.
WindowsMacOS
Developer Tools · Education & Learning
MCP Logic
angrysky56/mcp-logic
An MCP server for automated first-order logic reasoning using Prover9, Mace4, and an onboard reasoning LLM.
Install
Client configuration
{
"mcpServers": {
"mcp-logic": {
"command": "uv",
"args": [
"--directory",
"/absolute/path/to/mcp-logic",
"run",
"mcp_logic",
"--prover-path",
"/absolute/path/to/mcp-logic/ladr/bin"
]
}
}
}Environment variables
CMAKE_ARGS- GitHub stars
- 20
- Author
- @angrysky56
- Category
- Developer Tools, Education & Learning
- License
- MIT
- Updated
- Oct 6, 2026
Features
Theorem Proving - Prove logical statements with Prover9
Model Finding - Find finite models with Mace4
Counterexample Finding - Show why statements don't follow
Syntax Validation - Pre-validate formulas with helpful error messages
Categorical Reasoning - Built-in support for category theory proofs
Propositional Contingency - Purely analytical HCC prover for fast propositional checks
Abductive Reasoning - Rank hypotheses using Variational Free Energy (VFE)
Logic Advisor (NEW) - Onboard TwIL-LM3 reasoning LLM that solves logic problems end-to-end: just ask a question in plain English
Self-Contained - All dependencies install automatically
Tools (9)
ask_logic_advisor
Solve logic problems in plain English (end-to-end)
prove
Prove statements using Prover9
check_well_formed
Validate formula syntax with detailed errors
find_model
Find finite models satisfying premises
find_counterexample
Find counterexamples showing statements don't follow
verify_commutativity
Generate FOL for categorical diagram commutativity
get_category_axioms
Get axioms for category/functor/group/monoid
check_contingency
Check truth-functional contingency via HCC prover
abductive_explain
Find the VFE-minimizing explanation for an observation
Details on this page are taken from the project's README. Open README
Supported clients
Clients mentioned in this server's README:
Related MCP servers
Playwright
microsoft/playwright
Playwright is a framework for web automation and testing. It drives Chromium, Firefox, and WebKit with a single API — in your tests, in your scripts, and as a tool for AI agents.
repomix
yamadashy/repomix
Repomix is a tool that packs a codebase into an AI-friendly format, supporting local and remote repository processing and providing code compression, security checks and multiple output formats.
UI-TARS-desktop
bytedance/UI-TARS-desktop
TARS is ByteDance's multimodal AI agent stack, shipping two projects: Agent TARS (a CLI and Web UI agent built on MCP) and UI-TARS-desktop (a desktop GUI agent).
blender
ahujasid/blender-mcp
formerly blender-mcp — the PyPI package is now mcp-for-blender. Existing setups keep working; no config change is required. Read more.
Playwright Browser Automation
microsoft/playwright-mcp
A Model Context Protocol (MCP) server that provides browser automation capabilities using Playwright. This server enables LLMs to interact with web pages through structured accessibility snapshots, bypassing the need for screenshots or visually-tuned models.
2344
comet-ml/opik
Opik is the open-source LLM observability and evaluation platform for AI agent tracing, LLM evaluation, prompt management, and production monitoring. Built by Comet. Apache-2.0 licensed, free to self-host the full platform, with 20,000+ GitHub stars.