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:

Formula Analysis — Clausifies input to determine structure
Horn Check — If all clauses are Horn, uses Prolog
SAT Fallback — Non-Horn formulas route to MiniSat
Explicit Override — engine parameter forces specific engine

CNF Clausification

The clausifier transforms arbitrary FOL to CNF:

Eliminate biconditionals and implications
Push negations inward (NNF)
Standardize variable names
Skolemize existentials
Drop universal quantifiers
Distribute OR over AND
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

Inference Depth — Complex proofs may exceed limits
Model Size — Finder limited to domains ≤10 elements
SAT Variables — Arithmetic not supported in SAT engine
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

Fork the repository
Create a feature branch
Run tests: npm test
Submit a pull request

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:

Formula Analysis — Clausifies input to determine structure
Horn Check — If all clauses are Horn, uses Prolog
SAT Fallback — Non-Horn formulas route to MiniSat
Explicit Override — engine parameter forces specific engine

CNF Clausification

The clausifier transforms arbitrary FOL to CNF:

Eliminate biconditionals and implications
Push negations inward (NNF)
Standardize variable names
Skolemize existentials
Drop universal quantifiers
Distribute OR over AND
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

Inference Depth — Complex proofs may exceed limits
Model Size — Finder limited to domains ≤10 elements
SAT Variables — Arithmetic not supported in SAT engine
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

Fork the repository
Create a feature branch
Run tests: npm test
Submit a pull request