logic-llm

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

:warning: 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.