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