# 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
- [x] **Theorem Proving** — Resolution-based proving via Tau-Prolog
- [x] **Model Finding** — Finite model enumeration (domain ≤25 with SAT)
- [x] **Counterexample Detection** — Find models refuting conclusions
- [x] **Syntax Validation** — Pre-validate formulas with detailed errors
- [x] **CNF Clausification** — Transform FOL to Conjunctive Normal Form
- [x] **Tseitin Transformation** — Linear-size CNF conversion for SAT (avoids exponential blowup)
- [x] **DIMACS Export** — Export CNF for external SAT solvers
- [x] **Symmetry Breaking** — Lex-leader for model search (reduces search space exponentially)
- [x] **SAT-Backed Model Finding** — Scale to domain 25+ with automatic SAT threshold
- [ ] **Isomorphism Filtering** — Skip equivalent models (deferred until "findAllModels" use case)
- [x] **Proof Traces** — Step-by-step derivation output (via `include_trace`)

### Engine Federation
- [x] **Multi-Engine Architecture** — Automatic engine selection
- [x] **Prolog Engine** (Tau-Prolog) — Horn clauses, Datalog, equality
- [x] **SAT Engine** (MiniSat) — General FOL, non-Horn formulas
- [x] **SMT Engine** (Z3) — High-performance SMT solver with arithmetic & quantifiers
- [x] **ASP Engine** (Clingo) — Answer Set Programming (Constraints & Models)
- [x] **Engine Parameter** — Explicit engine selection via `engine` param
- [x] **Iterative Deepening** — Progressive inference limit strategy for complex proofs
- [x] **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
- [x] **Arithmetic Support** — Built-in: `lt`, `gt`, `plus`, `minus`, `times`, `divides`
- [x] **Equality Reasoning** — Reflexivity, symmetry, transitivity, congruence
- [x] **Rewriting System** — Knuth-Bendix style term rewriting for efficient equality handling (Prolog)
- [x] **Extended Axiom Library** — Ring, field, lattice, equivalence relation axioms
- [x] **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
- [x] **Session-Based Reasoning** — Incremental knowledge base construction with resource cleanup
- [x] **Axiom Resources** — Browsable libraries (category, Peano, ZFC, ring, lattice, etc.)
- [x] **Reasoning Prompts** — Templates for proof patterns
- [x] **Verbosity Control** — `minimal`/`standard`/`detailed` responses
- [x] **Structured Errors** — Machine-readable error codes and suggestions
- [x] **Streaming Progress** — Real-time progress notifications (via MCP notifications)
- [x] **High-Power Mode** — Extended limits with warning (via `highPower` option)

### Advanced Engines
- [x] **SMT (Z3 WASM)** — Theory reasoning (arithmetic, arrays), Equality, Quantifiers.
- [x] **ASP (Clingo)** — Non-monotonic reasoning, defaults, preferences.
- [ ] **Neural-Guided** — LLM-suggested proof paths with validation
- [ ] **Higher-Order Logic** — Quantify over predicates (research)

### Testing & Benchmarks
- [x] **Unit Tests** — 265+ tests passing, 80%+ coverage
- [x] **Pelletier Problems** — P1-P10 benchmark suite (extensible to P1-P75)
- [x] **Symmetry Benchmarks** — Bell number validation tests
- [x] **SAT Model Tests** — Group theory and algebraic structure verification
- [x] **Resilience Tests** — Resource leak detection and complexity limit verification
- [ ] **TPTP Library Subset** — Standard ATP benchmarks

---

## Quick Start

### Installation

```bash
git clone <repository>
cd mcplogic
pnpm install
pnpm run build
```

### Running the Server

```bash
pnpm start
```

### Verification

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

```bash
pnpm run verify
```

### Claude Desktop / MCP Client Configuration

Add to your MCP configuration:

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

### CLI Tools

The package includes a CLI for offline usage and verification:

```bash
# Check engine status
mcplogic check

# Prove a theorem from a file
mcplogic prove problem.p

# Find a model
mcplogic model theory.p

# Interactive REPL
mcplogic repl
```

---

## 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 |
| **translate-text** | Translate natural language to FOL (requires LLM) |

### 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:

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

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

| Engine | Best For | Capabilities |
|--------|----------|--------------|
| `prolog` | Horn clauses, Datalog | Equality, arithmetic, efficient unification |
| `sat` | Propositional, Finite Domain | Boolean logic, CNF solving |
| `z3` | General FOL, SMT | Arithmetic, Quantifiers, Equality |
| `clingo` | Answer Set Programming | Constraints (Experimental) |
| `auto` | Default — selects based on formula | Analyzes clause structure & features |

### Engine Capabilities

| Engine | Strength | Arithmetic | Quantifiers | Equality | Model Size |
|--------|----------|------------|-------------|----------|------------|
| **Z3** | High (SMT) | ✅ | ✅ | ✅ | Large |
| **Clingo** | High (ASP) | ✅ | Limited | ✅ | Large |
| **Prolog** | Medium (Resolution) | ✅ | Limited (Horn) | ✅ | Small/Medium |
| **SAT** | Low (Propositional) | ❌ | ❌ | ❌ | Small |

---

## 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

```
# All men are mortal, Socrates is a man
all x (man(x) -> mortal(x))
man(socrates)

# Transitivity of greater-than
all x all y all z ((greater(x, y) & greater(y, z)) -> greater(x, z))
```

---

## MCP Resources

| Resource URI | Description |
|--------------|-------------|
| `logic://axioms/category` | Category theory axioms |
| `logic://axioms/monoid` | Monoid structure |
| `logic://axioms/group` | Group axioms |
| `logic://axioms/ring` | Ring structure |
| `logic://axioms/lattice` | Lattice structure |
| `logic://axioms/equivalence` | Equivalence relations |
| `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) |

---

## 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 |

---

## 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

```bash
pnpm run build     # Compile TypeScript
pnpm test          # Run test suite
pnpm run dev       # Development mode with auto-reload
```

---

## License

MIT

---

## Future Directions

Potential enhancements will be driven by real-world usage:

- **Isomorphism Filtering** — Skip equivalent models in exhaustive model enumeration
- [x] **Proof Traces** — Step-by-step derivation output for educational/debugging use cases
- **Demodulation** — Equational term rewriting optimization for equality-heavy workloads
- [x] **Streaming Progress** — Real-time progress notifications for long-running operations
- **Extended Benchmarks** — TPTP library subset and group theory problem suites
- [x] **Advanced Engines** — SMT (Z3), ASP (Clingo)
- [x] **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 `pnpm 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`.