Skip to main content
Glama
automenta

MCP Logic

by automenta
OverviewSchemaRelated ServersScoreDiscussions
TypeScript
Remote

MCP Logic

A self-contained MCP server for first-order logic reasoning, implemented in TypeScript with no external binary dependencies.

Original: https://github.com/angrysky56/mcp-logic/

Features

Core Reasoning

  • Theorem Proving — Prove logical statements using resolution

  • Model Finding — Find finite models satisfying premises

  • Counterexample Detection — Find models showing conclusions don't follow

  • Syntax Validation — Pre-validate formulas with detailed error messages

Engine Federation

  • Multi-Engine Architecture — Automatic engine selection based on formula structure

  • Prolog Engine (Tau-Prolog) — Efficient for Horn clauses, Datalog, equality reasoning

  • SAT Engine (MiniSat) — Handles general FOL and non-Horn formulas

  • Engine Parameter — Explicit engine selection: 'prolog', 'sat', or 'auto'

Advanced Logic

  • Arithmetic Support — Built-in predicates: lt, gt, plus, minus, times, divides

  • Equality Reasoning — Reflexivity, symmetry, transitivity, congruence axioms

  • CNF Clausification — Transform FOL to Conjunctive Normal Form

  • DIMACS Export — Export CNF for external SAT solvers

MCP Protocol

  • Session-Based Reasoning — Incremental knowledge base construction

  • Axiom Resources — Browsable axiom libraries (category theory, Peano, ZFC, etc.)

  • Reasoning Prompts — Templates for proof by contradiction, formalization, etc.

  • Verbosity Control — Token-efficient responses for LLM chains

Infrastructure

  • Self-Contained — Pure npm dependencies, no external binaries

  • Structured Errors — Machine-readable error information with suggestions

  • 254 Tests — Comprehensive test coverage

Quick Start

Installation

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

Running the Server

npm start

Or for development with auto-reload:

npm run dev

Claude Desktop / MCP Client Configuration

Add to your MCP configuration:

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

Available Tools

Core Reasoning Tools

Tool

Description

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

Session Management Tools

Tool

Description

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

Engine Selection

The prove tool supports automatic or explicit engine selection:

{ "name": "prove", "arguments": { "premises": ["foo | bar", "-foo"], "conclusion": "bar", "engine": "auto" } }

Engine

Best For

Capabilities

prolog

Horn clauses, Datalog

Equality, arithmetic, efficient unification

sat

Non-Horn formulas, SAT problems

Full FOL, CNF solving

auto

Default — selects based on formula

Analyzes clause structure

The response includes engineUsed to show which engine was selected:

{ "success": true, "result": "proved", "engineUsed": "sat/minisat" }

Arithmetic and Equality

Arithmetic Support

Enable with enable_arithmetic: true:

{ "name": "prove", "arguments": { "premises": ["lt(1, 2)", "lt(2, 3)", "all x all y all z ((lt(x,y) & lt(y,z)) -> lt(x,z))"], "conclusion": "lt(1, 3)", "enable_arithmetic": true } }

Built-in predicates: lt, gt, le, ge, plus, minus, times, divides, mod

Equality Reasoning

Enable with enable_equality: true:

{ "name": "prove", "arguments": { "premises": ["a = b", "P(a)"], "conclusion": "P(b)", "enable_equality": true } }

Automatically injects reflexivity, symmetry, transitivity, and congruence axioms.

MCP Resources

Browse axiom libraries via the MCP resources protocol:

Resource URI

Description

logic://axioms/category

Category theory axioms

logic://axioms/monoid

Monoid structure

logic://axioms/group

Group axioms

logic://axioms/peano

Peano arithmetic

logic://axioms/set-zfc

ZFC set theory basics

logic://axioms/propositional

Propositional tautologies

logic://templates/syllogism

Aristotelian syllogism patterns

logic://engines

Available reasoning engines (JSON)

MCP Prompts

Reasoning templates for common tasks:

Prompt

Description

prove-by-contradiction

Set up proof by contradiction

verify-equivalence

Check formula equivalence

formalize

Natural language to FOL translation guide

diagnose-unsat

Diagnose unsatisfiable premises

explain-proof

Explain proven theorem

Verbosity Control

All tools support a verbosity parameter:

Level

Description

Use Case

minimal

Just success/result

Token-efficient LLM chains

standard

+ message, bindings, engineUsed

Default balance

detailed

+ Prolog program, statistics

Debugging

{ "name": "prove", "arguments": { "premises": ["man(socrates)", "all x (man(x) -> mortal(x))"], "conclusion": "mortal(socrates)", "verbosity": "minimal" } }

Minimal response: { "success": true, "result": "proved" }

Formula Syntax

This server uses first-order logic (FOL) syntax compatible with Prover9:

Quantifiers

  • all x (...) — Universal quantification (∀x)

  • exists x (...) — Existential quantification (∃x)

Connectives

  • -> — Implication (→)

  • <-> — Biconditional (↔)

  • & — Conjunction (∧)

  • | — Disjunction (∨)

  • - — Negation (¬)

Predicates and Terms

  • Predicates: man(x), loves(x, y), greater(x, y)

  • Constants: socrates, a, b

  • Variables: x, y, z (lowercase, typically single letters)

  • Functions: f(x), successor(n)

  • Equality: x = y

Examples

# All men are mortal, Socrates is a man all x (man(x) -> mortal(x)) man(socrates) # There exists someone who loves everyone exists x all y loves(x, y) # Transitivity of greater-than all x all y all z ((greater(x, y) & greater(y, z)) -> greater(x, z))

Tool Usage Examples

1. Prove a Theorem (with Engine Selection)

{ "name": "prove", "arguments": { "premises": [ "all x (man(x) -> mortal(x))", "man(socrates)" ], "conclusion": "mortal(socrates)", "engine": "prolog" } }

2. Prove with SAT Engine (Non-Horn)

{ "name": "prove", "arguments": { "premises": ["alpha | beta", "alpha -> gamma", "beta -> gamma"], "conclusion": "gamma", "engine": "sat" } }

3. Find a Counterexample

{ "name": "find-counterexample", "arguments": { "premises": ["P(a)"], "conclusion": "P(b)" } }

4. Session-Based Reasoning

// 1. Create a session { "name": "create-session", "arguments": { "ttl_minutes": 30 } } // 2. Assert premises { "name": "assert-premise", "arguments": { "session_id": "abc-123...", "formula": "all x (man(x) -> mortal(x))" }} // 3. Query the KB { "name": "query-session", "arguments": { "session_id": "abc-123...", "goal": "mortal(socrates)" }} // 4. Cleanup { "name": "delete-session", "arguments": { "session_id": "abc-123..." } }

Project Structure

mcplogic/ ├── package.json ├── tsconfig.json ├── src/ │ ├── index.ts # CLI entry point │ ├── server.ts # MCP server (13 tools) │ ├── parser.ts # FOL tokenizer & parser │ ├── translator.ts # FOL ↔ Prolog conversion │ ├── logicEngine.ts # Tau-Prolog wrapper │ ├── clausifier.ts # CNF clausification & DIMACS export │ ├── syntaxValidator.ts # Syntax validation │ ├── categoricalHelpers.ts # Category theory │ ├── modelFinder.ts # Finite model enumeration │ ├── sessionManager.ts # Session lifecycle │ ├── equalityAxioms.ts # Equality reasoning │ ├── engines/ │ │ ├── interface.ts # ReasoningEngine interface │ │ ├── manager.ts # Engine federation │ │ ├── prolog.ts # Prolog engine adapter │ │ └── sat.ts # SAT engine adapter │ ├── resources/ │ │ └── axioms.ts # MCP resources │ ├── prompts/ │ │ └── index.ts # MCP prompts │ └── types/ │ ├── index.ts # Shared types │ ├── errors.ts # Structured errors │ └── clause.ts # CNF clause types └── tests/ # 254 tests

Technical Details

Engine Federation

The EngineManager automatically selects the best engine:

  1. Formula Analysis — Clausifies input to determine structure

  2. Horn Check — If all clauses are Horn, uses Prolog

  3. SAT Fallback — Non-Horn formulas route to MiniSat

  4. Explicit Override — engine parameter forces specific engine

CNF Clausification

The clausifier transforms arbitrary FOL to CNF:

  1. Eliminate biconditionals and implications

  2. Push negations inward (NNF)

  3. Standardize variable names

  4. Skolemize existentials

  5. Drop universal quantifiers

  6. Distribute OR over AND

  7. Extract clauses

DIMACS Export

For external SAT solver interop:

import { clausify, clausesToDIMACS } from './clausifier'; const result = clausify('(P -> Q) & P'); const dimacs = clausesToDIMACS(result.clauses); // dimacs.dimacs = "p cnf 2 2\n-1 2 0\n1 0" // dimacs.varMap = Map { 'P' => 1, 'Q' => 2 }

Structured Errors

All errors include machine-readable information:

interface LogicError { code: LogicErrorCode; // 'PARSE_ERROR' | 'INFERENCE_LIMIT' | ... message: string; span?: { start, end, line, col }; suggestion?: string; context?: string; }

API Reference

prove

interface ProveArgs { premises: string[]; conclusion: string; inference_limit?: number; // Max steps (default: 1000) engine?: 'prolog' | 'sat' | 'auto'; // Engine selection enable_arithmetic?: boolean; // Enable arithmetic predicates enable_equality?: boolean; // Inject equality axioms verbosity?: 'minimal' | 'standard' | 'detailed'; } interface ProveResult { success: boolean; result: 'proved' | 'failed' | 'timeout' | 'error'; message?: string; engineUsed?: string; // Which engine was used bindings?: Record<string, string>[]; proof?: string[]; prologProgram?: string; // (detailed only) statistics?: { timeMs: number; inferences?: number }; }

check-well-formed

interface CheckArgs { statements: string[]; verbosity?: 'minimal' | 'standard' | 'detailed'; } interface ValidationResult { valid: boolean; formulaResults: Array<{ formula: string; valid: boolean; errors: string[]; warnings: string[]; }>; }

find-model / find-counterexample

interface FindModelArgs { premises: string[]; domain_size?: number; max_domain_size?: number; // Default: 10 verbosity?: 'minimal' | 'standard' | 'detailed'; } interface ModelResult { success: boolean; result: 'model_found' | 'no_model' | 'timeout' | 'error'; model?: { domainSize: number; predicates: Record<string, string[]>; constants: Record<string, number>; }; }

Session Tools

// create-session { session_id: string; expires_at: string; ttl_minutes: number } // assert-premise { success: boolean; premise_count: number } // query-session { success: boolean; result: string; engineUsed?: string } // list-premises { premises: string[]; premise_count: number }

Limitations

  1. Inference Depth — Complex proofs may exceed limits

  2. Model Size — Finder limited to domains ≤10 elements

  3. SAT Variables — Arithmetic not supported in SAT engine

  4. Higher-Order — Only first-order logic supported

Troubleshooting

"No proof found" for valid theorem

  • Increase inference_limit for complex proofs

  • Try engine: 'sat' for non-Horn formulas

  • Enable enable_equality if using equality

Model finder returns "no_model"

  • Increase max_domain_size

  • Check for contradictory premises

Session errors

  • Check session hasn't expired (default: 30 min)

  • Use list-premises to inspect state

Development

npm test # Run 254 tests npm run build # Compile TypeScript npx tsc --noEmit # Type check only

License

MIT

Contributing

  1. Fork the repository

  2. Create a feature branch

  3. Run tests: npm test

  4. Submit a pull request

This server cannot be installed

-
security - not tested
F
license - not found
-
quality - not tested

How are these scores calculated?

Resources

New MCP Servers

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/automenta/mcplogic'

If you have feedback or need assistance with the MCP directory API, please join our Discord server