/logic-convert

Convert natural language documents into symbolic logic programs.

Description

This skill translates natural language text, rules, regulations, or knowledge bases into formal logic programs that can be used for automated reasoning. It follows the Logic-LLM methodology with enhancements for persistent storage and code reuse.

Supported Formats

Format	Solver	Best For
prolog	prolog-mcp	Deductive reasoning, Horn clauses
clingo	clingo-mcp	Constraints, optimization, ASP
z3	z3smt-mcp	Arithmetic, SMT, satisfiability
fol	folprover-mcp	First-order logic with quantifiers
pyke	pyke-mcp	Forward/backward chaining, Python

Usage

/logic-convert [options] <source>

Options

• --format <prolog|clingo|z3|fol|pyke> - Target format (default: auto-detect)
• --output <path> - Output file path for generated logic program
• --append - Append to existing knowledge base instead of creating new
• --register - Auto-register predicates in the registry
• --domain <name> - Domain name for organizing predicates (e.g., "legal", "medical")
• --validate - Validate generated code with solver before saving
• --dmn-compatible - Generate DMN-compatible Prolog (only with --format prolog)
• --test - Generate and run test cases using MCP server

Examples

/logic-convert --format prolog ./contracts/terms.txt
/logic-convert --format clingo --domain legal ./regulations/
/logic-convert --format z3 ./scheduling-constraints.txt
/logic-convert --format fol --register ./logical-premises.md
/logic-convert --format pyke ./inference-rules.txt
/logic-convert --append --register ./new-rules.md

# DMN-compatible Prolog with validation
/logic-convert --format prolog --dmn-compatible --test ./decision-table.txt
/logic-convert --format prolog --dmn-compatible --validate --output ./dmn_rules.pl ./rules.md

Format Selection Guide

Choose format based on problem type:

Problem Type	Recommended Format
Deductive reasoning (if-then chains)	prolog or pyke
Constraints with optimization	clingo
Arithmetic constraints	z3
Full first-order logic (∀, ∃)	fol
Analytical reasoning (LSAT)	z3
Legal/policy with exceptions	clingo or prolog
Python integration needed	pyke

Behavior

1. Document Analysis: Read and parse the input document(s)
2. Problem Classification: Determine best solver if format not specified
3. Predicate Extraction: Identify entities, relationships, and rules
4. Registry Check: Look up existing predicates to ensure consistency
5. Code Generation: Generate code following Logic-LLM methodology
6. Self-Refinement: Fix errors using solver feedback (up to 3 attempts)
7. Registration: Register new predicates, facts, and rules in the registry
8. Validation: Syntax-check the generated code using the appropriate solver

Output

The skill generates:

• Logic program file(s) in the specified format
• Registry entries for new predicates and rules
• Conversion report with mapping from natural language to logic

Integration

This skill uses:

• prolog-mcp for Prolog validation
• clingo-mcp for Clingo/ASP validation
• z3smt-mcp for Z3/SMT validation
• folprover-mcp for FOL validation
• pyke-mcp for Pyke validation
• logic-registry MCP server for predicate registration
• Stored prompt templates from prompts/ directory

DMN Compatibility Mode

When using --dmn-compatible with Prolog, the generator follows Decision Model and Notation (DMN) constraints:

DMN Constraints

1. Horn Clauses Only: No negation-as-failure (+, not)
2. Deterministic Rules: Single solution per input (uses cuts)
3. Simple Data Types: Atoms, numbers, strings only
4. Decision Table Structure: Rules map to decision table rows
5. Limited Recursion: Maximum depth of 3 levels
6. FEEL Compatibility: Compatible with FEEL expression language

DMN Validation Checks

The --dmn-compatible flag enforces:

• ✓ All rules are Horn clauses
• ✓ No NAF predicates
• ✓ Deterministic output (cut placement)
• ✓ Simple data types
• ✓ Recursion depth ≤ 3

Testing with prolog-mcp

When --test is specified, the skill:

1. Generates test cases for all rules
2. Loads program into prolog-mcp
3. Verifies determinism (single solution per input)
4. Checks for NAF usage
5. Validates recursion depth
6. Reports any DMN compliance violations

Example: DMN-Compatible Credit Approval

Input Document:

Approve credit if:
- Credit score >= 700 and income >= 50000
- Credit score >= 650 and income >= 75000 and employment >= 3 years
Otherwise reject.

Generated Prolog:

% Decision Table: Credit Approval
approve_credit(Score, Income, _) :- Score >= 700, Income >= 50000.
approve_credit(Score, Income, Years) :- Score >= 650, Income >= 75000, Years >= 3.

credit_decision(Score, Income, Years, approved) :- approve_credit(Score, Income, Years), !.
credit_decision(_, _, _, rejected).

Test Output:

✓ DMN Compliance: PASS
✓ Determinism: PASS (1 solution per input)
✓ No NAF: PASS
✓ Recursion: PASS (no recursion)
✓ Data Types: PASS (numbers, atoms only)

Test Cases:
  credit_decision(750, 60000, 2, approved) - PASS
  credit_decision(680, 80000, 4, approved) - PASS
  credit_decision(550, 40000, 1, rejected) - PASS

Notes

• For documents exceeding context limits, the skill processes in chunks and maintains consistency through the registry
• Generated code follows naming conventions from the registry to avoid duplicates
• Use --append when adding to an existing knowledge base to maintain referential integrity
• Auto-detection analyzes problem for quantifiers, arithmetic, constraints to choose best format
• DMN compatibility is only available for Prolog format
• Testing with --test requires the appropriate MCP server to be enabled and running