Description

First-order logic reasoning server built with Tau-Prolog that provides theorem proving, model finding, and syntax validation capabilities for logical formulas. Supports Prover9-style syntax with quantifiers, connectives, predicates, and functions, offering tools to prove statements using resolution, find finite models satisfying premises, discover counterexamples, and validate formula syntax with helpful error messages. Includes specialized support for category theory with axiom generation for categories, functors, monoids, and groups, plus diagram commutativity verification.

Installation

git clone https://github.com/autonull/mcplogic

Claude Desktop Configuration

Add this configuration to your Claude Desktop config file to enable this MCP server:

Config file location: ~/Library/Application Support/Claude/claude_desktop_config.json

Config file location: %APPDATA%\Claude\claude_desktop_config.json

Config file location: ~/.config/Claude/claude_desktop_config.json

claude_desktop_config.json

{
  "mcpServers": {
    "logic": {
      "command": "node",
      "args": [
        "path/to/server.js"
      ]
    }
  }
}