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/

Feature Status

✅ = Implemented | 🔲 = Planned | 🔬 = Research/Vision

Core Reasoning

• Theorem Proving — Resolution-based proving via Tau-Prolog

• Model Finding — Finite model enumeration (domain ≤25 with SAT)

• Counterexample Detection — Find models refuting conclusions

• Syntax Validation — Pre-validate formulas with detailed errors

• CNF Clausification — Transform FOL to Conjunctive Normal Form

• Tseitin Transformation — Linear-size CNF conversion for SAT (avoids exponential blowup)

• DIMACS Export — Export CNF for external SAT solvers

• Symmetry Breaking — Lex-leader for model search (reduces search space exponentially)

• SAT-Backed Model Finding — Scale to domain 25+ with automatic SAT threshold

• Isomorphism Filtering — Skip equivalent models (deferred until "findAllModels" use case)

• Proof Traces — Step-by-step derivation output (via include_trace)

Engine Federation

• Multi-Engine Architecture — Automatic engine selection

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

• SAT Engine (MiniSat) — General FOL, non-Horn formulas

• SMT Engine (Z3) — High-performance SMT solver with arithmetic & quantifiers

• ASP Engine (Clingo) — Answer Set Programming (Constraints & Models)

• Engine Parameter — Explicit engine selection via engine param

• Iterative Deepening — Progressive inference limit strategy for complex proofs

• Resource Management — Automatic cleanup of WASM resources (Z3 contexts)

• Prover9 WASM — Optional high-power ATP (deferred until SAT+iterative proves insufficient)

• Demodulation — Equational term rewriting (deferred until equality workloads show perf issues)

Logic Features

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

• Equality Reasoning — Reflexivity, symmetry, transitivity, congruence

• Rewriting System — Knuth-Bendix style term rewriting for efficient equality handling (Prolog)

• Extended Axiom Library — Ring, field, lattice, equivalence relation axioms

• Function Interpretation — Full function support in model finding

• Typed/Sorted FOL — Domain-constraining type annotations (research)

• Modal Logic — Necessity, possibility operators (research)

• Probabilistic Logic — Weighted facts, Bayesian inference (research)

MCP Protocol

• Session-Based Reasoning — Incremental knowledge base construction with resource cleanup

• Axiom Resources — Browsable libraries (category, Peano, ZFC, ring, lattice, etc.)

• Reasoning Prompts — Templates for proof patterns

• Verbosity Control — minimal/standard/detailed responses

• Structured Errors — Machine-readable error codes and suggestions

• Streaming Progress — Real-time progress notifications (via MCP notifications)

• High-Power Mode — Extended limits with warning (via highPower option)

Advanced Engines

• SMT (Z3 WASM) — Theory reasoning (arithmetic, arrays), Equality, Quantifiers.

• ASP (Clingo) — Non-monotonic reasoning, defaults, preferences.

• Neural-Guided — LLM-suggested proof paths with validation

• Higher-Order Logic — Quantify over predicates (research)

Testing & Benchmarks

• Unit Tests — 265+ tests passing, 80%+ coverage

• Pelletier Problems — P1-P10 benchmark suite (extensible to P1-P75)

• Symmetry Benchmarks — Bell number validation tests

• SAT Model Tests — Group theory and algebraic structure verification

• Resilience Tests — Resource leak detection and complexity limit verification

• TPTP Library Subset — Standard ATP benchmarks

Quick Start

Installation

Running the Server

Verification

Run the comprehensive health check to verify build, tests, and engine availability:

Claude Desktop / MCP Client Configuration

Add to your MCP configuration:

CLI Tools

The package includes a CLI for offline usage and verification:

Available Tools

Core Reasoning Tools

Session Management Tools

Engine Selection

The prove tool supports automatic or explicit engine selection:

The include_trace option (boolean) enables step-by-step derivation output in the response, useful for debugging or understanding the proof path.

Engine Capabilities

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 (¬)

Examples

MCP Resources

Verbosity Control

All tools support a verbosity parameter:

Limitations (Current)

1. Model Size — Finder limited to domains ≤25 elements (using SAT)

2. Inference Depth — Complex proofs may exceed default limit (increase via inference_limit or use iterative strategy)

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

Future improvements may address these limitations as real-world usage dictates.

Development

License

MIT

Future Directions

Potential enhancements will be driven by real-world usage:

• Isomorphism Filtering — Skip equivalent models in exhaustive model enumeration

• Proof Traces — Step-by-step derivation output for educational/debugging use cases

• Demodulation — Equational term rewriting optimization for equality-heavy workloads

• Streaming Progress — Real-time progress notifications for long-running operations

• Extended Benchmarks — TPTP library subset and group theory problem suites

• Advanced Engines — SMT (Z3), ASP (Clingo)

• Evolution Engine — Genetic algorithm for evolving efficient proof strategies

• Neural-Guided — LLM-suggested proof paths with validation

Troubleshooting

WASM Engines (Z3 / Clingo)

If you encounter errors related to z3-solver or clingo-wasm:

1. Ensure your environment supports WebAssembly.

2. In browser environments, ensure the .wasm files are served correctly. The check command can verify basic functionality in Node.js.

3. If you see OOM or memory errors, try running with the default engine (Prolog) or increasing the timeout/inference limits.

build:browser Failures

Ensure you have run npm install to get the latest type definitions. The browser build relies on specific overrides for WASM modules that are handled in src/engines/*/index.ts.