MCP Logic

You can run a self-contained MCP server that performs first-order logic reasoning using multiple engines. This server lets you construct incremental knowledge bases, prove theorems, find models, and stream progress to clients, all within a single, TypeScript-based runtime with no external binaries required.

How to use

You connect to the MCP server through an MCP client, send requests to load premises incrementally, and ask questions such as proofs or models. The server supports session-based reasoning, so you can build up a knowledge base piece by piece, request proofs or models for your current KB, and receive structured errors or progress updates. You can control verbosity to tailor responses for debugging, development, or production usage.

How to install

Follow these concrete steps to set up the MCP server locally and prepare it for use.

git clone <repository>
cd mcplogic
npm install
npm run build

Configuration and usage notes

Configure the server in your MCP client by pointing to the local runtime as shown in the example below. This config loads the compiled MCP logic from the build output and executes it via Node.

{
  "mcpServers": {
    "mcp_logic": {
      "command": "node",
      "args": ["/path/to/mcplogic/dist/index.js"]
    }
  }
}

Running the server and verifying health

Start the server after building to begin responding to client requests. The standard workflow includes installation, building, and launching the server, followed by a health check to ensure engines are available and ready.

npm start

Troubleshooting and tips

If you encounter issues related to engine availability or memory usage, try the default small-scale configuration first and confirm the build completed successfully. Use the health check command to verify the server and engine readiness, and adjust any resource limits if needed.

Development notes

For development workflows, you can run tests or a development server with auto-reload as you iterate on the TypeScript source.

npm test
npm run dev

Available tools

prove

Prove statements using resolution with engine selection

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/monoid/group

translate-text

Translate natural language to FOL (requires LLM)

create-session

Create a new reasoning session with TTL

assert-premise

Add a formula to a session's knowledge base

query-session

Query the accumulated KB with a goal

retract-premise

Remove a specific premise from the KB

list-premises

List all premises in a session

clear-session

Clear all premises (keeps session alive)

delete-session

Delete a session entirely