Logic-LLM Plugin for Claude Code

A Claude Code plugin that integrates symbolic reasoning capabilities using multiple solvers, based on the 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
Clingo	clingo-mcp	Constraints, optimization, ASP	NewJerseyStyle/clingo-mcp
Z3/SMT	z3smt-mcp	Arithmetic, satisfiability, verification	NewJerseyStyle/z3smt-mcp
FOL Prover	folprover-mcp	First-order logic (∀, ∃), theorem proving	NewJerseyStyle/folprover-mcp
Pyke	pyke-mcp	Forward/backward chaining, Python integration	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:

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

⚠️ This method is not well tested, manual install is more reliable

Install the Plugin Manually

# 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

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

Install MCP Servers

Node.js-based Servers (Prolog, Clingo)

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

# Clingo
npm install clingo-mcp

Python-based Servers (Z3, FOL, Pyke)

# 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 for detailed setup instructions.

Usage

Skills (Slash Commands)

/logic-convert

Convert documents to symbolic logic programs.

/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.

/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.

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

/logic-register

Manage the predicate registry.

/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 - Prolog/Clingo
• Scheduling Problem - 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 - Original methodology (EMNLP 2023)
• Prolog MCP
• Clingo MCP
• Z3/SMT MCP
• FOL Prover MCP
• Pyke MCP
• Claude Code Plugins Reference