Logic Convert

# /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:**
```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