logic-llm - Claude Code Plugin

Documentation

# Logic-LLM Plugin for Claude Code

A Claude Code plugin that integrates symbolic reasoning capabilities using multiple solvers, based on the [Logic-LLM](https://github.com/teacherpeterpan/Logic-LLM) methodology.

## Overview

This plugin enables Claude Code to:
- Convert natural language documents into formal logic programs
- Execute symbolic reasoning using 5 different solver backends
- Maintain persistent knowledge bases for multi-turn conversations
- Handle inputs that exceed context limits through registry-based memory

## Supported Solvers

| Solver | MCP Server | Best For | Repository |
|--------|------------|----------|------------|
| **Prolog** | prolog-mcp | Deductive reasoning, Horn clauses | [adamrybinski/prolog-mcp](https://github.com/adamrybinski/prolog-mcp) |
| **Clingo** | clingo-mcp | Constraints, optimization, ASP | [NewJerseyStyle/clingo-mcp](https://github.com/NewJerseyStyle/clingo-mcp) |
| **Z3/SMT** | z3smt-mcp | Arithmetic, satisfiability, verification | [NewJerseyStyle/z3smt-mcp](https://github.com/NewJerseyStyle/z3smt-mcp) |
| **FOL Prover** | folprover-mcp | First-order logic (∀, ∃), theorem proving | [NewJerseyStyle/folprover-mcp](https://github.com/NewJerseyStyle/folprover-mcp) |
| **Pyke** | pyke-mcp | Forward/backward chaining, Python integration | [NewJerseyStyle/pyke-mcp](https://github.com/NewJerseyStyle/pyke-mcp) |

### Solver Selection Guide

| Problem Type | Recommended Solver |
|--------------|-------------------|
| Deductive chains (ProntoQA, ProofWriter) | Prolog, Pyke |
| Constraints with optimization | Clingo |
| First-order logic with quantifiers (FOLIO) | FOL Prover |
| Constraint satisfaction (LogicalDeduction) | Clingo, Z3 |
| Analytical reasoning (AR-LSAT) | Z3 |
| Arithmetic constraints | Z3 |
| Legal/policy with exceptions | Clingo, Prolog |

### DMN (Decision Model and Notation) Support

The plugin supports generating **DMN-compatible Prolog** for business rule systems:

```bash
/logic-convert --format prolog --dmn-compatible --test ./decision-rules.txt
```

**DMN Constraints Enforced:**
- ✓ Horn clauses only (no negation-as-failure)
- ✓ Deterministic rules (single output per input)
- ✓ Simple data types (atoms, numbers, strings)
- ✓ Decision table structure
- ✓ Limited recursion (≤ 3 levels)
- ✓ FEEL expression compatibility

**Validation via prolog-mcp:**
- Determinism testing (1 solution per input)
- NAF detection and warnings
- Recursion depth analysis
- Automated test case generation

See [examples/dmn-credit-approval.md](examples/dmn-credit-approval.md) for a complete example.

### Differences from Original Logic-LLM

> **Important:** This plugin extends the original Logic-LLM approach:

| Feature | Original Logic-LLM | This Plugin |
|---------|-------------------|-------------|
| **Scope** | Q&A only | Q&A + code generation + document conversion |
| **Memory** | Per-query | Persistent registry across sessions |
| **Context** | Single query | Multi-turn with symbolic memory |
| **Input Size** | Within context | Unlimited via chunked processing |
| **Code Reuse** | None | Registry-based predicate reuse |
| **Solvers** | Per-dataset | All solvers available, auto-selection |
| **Output** | Answers | Answers + reusable logic programs |

The plugin stores generated predicates, facts, and rules in a **registry** that persists across sessions. This enables:
- Long documents processed in chunks while maintaining consistency
- Previously generated code reused, not regenerated
- Variable/predicate naming consistent across conversions
- Multi-turn reasoning referencing previous context stored in symbols


## Installation
Simple setup is to add in Claude Code CLI
```
/plugin marketplace add NewJerseyStyle/Claude-plugins-marketplace
/plugin install logic-llm
```

> :warning: This method is not well tested, manual install is more reliable

### Install the Plugin Manually

```bash
# Clone the plugin repository
git clone https://github.com/NewJerseyStyle/plugin-logic-llm.git

# Install to user scope (available across all projects)
claude plugin install ./plugin-logic-llm --scope user

# Or install to project scope (shared with team via git)
claude plugin install ./plugin-logic-llm --scope project
```

### Build the Registry Server

```bash
cd plugin-logic-llm/servers/registry-server
npm install
npm run build
```

### Install MCP Servers

#### Node.js-based Servers (Prolog, Clingo)

```bash
# Prolog
# npx -y github:adamrybinski/prolog-mcp

# Clingo
npm install clingo-mcp
```

#### Python-based Servers (Z3, FOL, Pyke)

```bash
# Z3/SMT
pip install z3smt-mcp

# FOL Prover
pip install folprover-mcp

# Pyke
pip install git+https://github.com/evertrol/pyke3 pyke-mcp
```

## Configuration

See [CONFIGURATION.md](CONFIGURATION.md) for detailed setup instructions.

## Usage

### Skills (Slash Commands)

#### `/logic-convert`
Convert documents to symbolic logic programs.

```bash
/logic-llm:logic-convert --format prolog ./contracts/terms.txt
/logic-llm:logic-convert --format clingo --domain legal ./regulations/
/logic-llm:logic-convert --format z3 ./scheduling-problem.txt
/logic-llm:logic-convert --format fol ./logical-premises.md
/logic-llm:logic-convert --format pyke ./inference-rules.txt
```

#### `/logic-query`
Query knowledge bases using natural language.

```bash
/logic-llm:logic-query "Can John access the confidential files?"
/logic-llm:logic-query --format z3 "Is there a valid assignment under budget?"
/logic-llm:logic-query --format fol --explain "Is Socrates mortal?"
```

#### `/logic-ingest`
Batch process directories of documents.

```bash
/logic-llm:logic-ingest --format prolog --domain legal ./all-contracts/
/logic-llm:logic-ingest --incremental --watch ./regulations/
```

#### `/logic-register`
Manage the predicate registry.

```bash
/logic-llm:logic-register search "access"
/logic-llm:logic-register list --domain legal
/logic-llm:logic-register add --domain legal "can_approve(Person, Amount)"
```

## Architecture

```
plugin-logic-llm/
├── .claude-plugin/
│   └── plugin.json           # Plugin manifest
├── .mcp.json                 # MCP server configuration (6 servers)
├── skills/                   # Skill definitions
│   ├── logic-convert/        # Document conversion
│   ├── logic-query/          # Knowledge base queries
│   ├── logic-ingest/         # Batch processing
│   └── logic-register/       # Registry management
├── agents/                   # Specialized agents (7 agents)
│   ├── prolog-reasoner.md
│   ├── clingo-reasoner.md
│   ├── z3-reasoner.md
│   ├── fol-reasoner.md
│   ├── pyke-reasoner.md
│   ├── document-converter.md
│   └── registry-manager.md
├── prompts/                  # Prompt templates (6 templates)
│   ├── prolog-conversion.md
│   ├── clingo-conversion.md
│   ├── z3-conversion.md
│   ├── fol-conversion.md
│   ├── pyke-conversion.md
│   └── query-translation.md
├── servers/
│   └── registry-server/      # Registry MCP server
├── data/
│   ├── registry/             # Persistent predicate registry
│   └── sessions/             # Solver sessions
└── examples/                 # Usage examples
```

## How It Works

### Document Conversion Flow

```
┌─────────────────┐
│ Natural Language│
│    Document     │
└────────┬────────┘
         │
         ▼
┌─────────────────┐
│  Registry Check │◄──────┐
│ (existing preds)│       │
└────────┬────────┘       │
         │                │
         ▼                │
┌─────────────────┐       │
│ Format Selection│       │
│ (auto or manual)│       │
└────────┬────────┘       │
         │                │
         ▼                │
┌─────────────────┐       │
│ Code Generation │       │
│  (Logic-LLM)    │       │
└────────┬────────┘       │
         │                │
         ▼                │
┌─────────────────┐       │
│   Validation    │       │
│   (via solver)  │       │
└────────┬────────┘       │
         │ error?         │
         ├───────────────►│
         │ Self-Refinement│
         │ (up to 3x)     │
         ▼                │
┌─────────────────┐       │
│  Registration   │───────┘
│ (new predicates)│
└────────┬────────┘
         │
         ▼
┌─────────────────┐
│  Logic Program  │
│    (output)     │
└─────────────────┘
```

### Handling Large Documents

For documents exceeding context limits:

1. Document split into logical chunks
2. Each chunk processed with registry context
3. New predicates registered after each chunk
4. Consistency maintained through the registry
5. Final deduplication removes redundant rules
6. Complete knowledge base validated

**The context limit is no longer a hard constraint** for document processing.

## Examples

See the `examples/` directory for detailed walkthroughs:
- [Legal Access Control](examples/legal-access-control.md) - Prolog/Clingo
- [Scheduling Problem](examples/scheduling-problem.md) - Clingo with optimization

## Troubleshooting

### MCP Server Not Connecting

1. Verify paths in `.mcp.json` are correct
2. For Node.js servers: ensure built (`npm run build`)
3. For Python servers: ensure installed (`pip install`)
4. Check logs: `claude --debug`

### Solver-Specific Issues

| Solver | Common Issue | Solution |
|--------|-------------|----------|
| Prolog | Undefined predicate | Add missing facts/rules |
| Clingo | Unsafe variable | Ensure variables in positive body |
| Z3 | Type mismatch | Check Int vs Real vs Bool |
| FOL | Timeout | Simplify formula, try different prover |
| Pyke | Missing `$` | Variables must have `$` prefix |

## Contributing

Contributions welcome! Please see the repository for guidelines.

## License

MIT License

## References

- [Logic-LLM Paper](https://github.com/teacherpeterpan/Logic-LLM) - Original methodology (EMNLP 2023)
- [Prolog MCP](https://github.com/adamrybinski/prolog-mcp)
- [Clingo MCP](https://github.com/NewJerseyStyle/clingo-mcp)
- [Z3/SMT MCP](https://github.com/NewJerseyStyle/z3smt-mcp)
- [FOL Prover MCP](https://github.com/NewJerseyStyle/folprover-mcp)
- [Pyke MCP](https://github.com/NewJerseyStyle/pyke-mcp)
- [Claude Code Plugins Reference](https://code.claude.com/docs/en/plugins-reference)