Logic Query

# /logic-query

Query symbolic knowledge bases using natural language or formal logic syntax.

## Description

This skill enables querying knowledge bases that have been created through `/logic-convert` or manually. It translates natural language questions into formal queries and returns human-readable answers using the appropriate solver.

## Supported Solvers

| Solver | MCP Server | Query Types |
|--------|------------|-------------|
| Prolog | prolog-mcp | Yes/no, find values, find all |
| Clingo | clingo-mcp | Answer sets, optimization |
| Z3 | z3smt-mcp | Satisfiability, models, proofs |
| FOL | folprover-mcp | Theorem proving |
| Pyke | pyke-mcp | Goal proving, variable bindings |

## Usage

```
/logic-query [options] <question>
```

### Options

- `--format <prolog|clingo|z3|fol|pyke>` - Query format (auto-detected if KB loaded)
- `--kb <path>` - Path to knowledge base file(s) to load
- `--session <name>` - Use named session (persists loaded facts/rules)
- `--explain` - Show reasoning trace/proof
- `--all` - Return all solutions/answer sets/models
- `--timeout <ms>` - Query timeout in milliseconds

### Examples

```
/logic-query "Is John allowed to access the confidential files?"
/logic-query --kb ./legal/rules.pl --explain "Can contractors view salary data?"
/logic-query --format clingo --all "What are the valid schedules?"
/logic-query --format z3 "Is it possible to assign all tasks within budget?"
/logic-query --format fol --explain "Does mortality follow from the premises?"
/logic-query --format pyke --session hr "Who reports to the CEO?"
```

## Query Types by Solver

### Prolog Queries
```
# Yes/No
?- can_access(john, file_a).

# Find values
?- can_access(john, What).

# Find all
?- findall(X, can_access(X, confidential), People).
```

### Clingo Queries
```
# Check satisfiability (answer sets exist?)
# Find all answer sets
# Optimization (minimize/maximize)
```

### Z3 Queries
```
# Satisfiability check
s.check()

# Get model
s.model()

# Prove theorem
prove(theorem)
```

### FOL Queries
```
# Prove from premises
prove(premises, conclusion)

# Check validity
```

### Pyke Queries
```
# Test fact
query("Mortal(socrates, True)")

# Find bindings
prove_goal("Descendant(tom, $who, True)")
```

## Behavior

1. **Session Management**: Load or create query session
2. **Knowledge Base Loading**: Load specified KB files if not in session
3. **Query Translation**: Convert natural language to formal query
4. **Registry Lookup**: Use registry to resolve predicate names
5. **Solver Selection**: Choose appropriate solver based on format
6. **Execution**: Run query through MCP server
7. **Result Interpretation**: Translate formal results to natural language

## Output

The skill returns:
- Answer to the query (yes/no, values, or explanations)
- Reasoning trace if `--explain` is used
- Multiple solutions if `--all` is specified
- Confidence indicator when translation is ambiguous

## Session Persistence

Sessions are stored in `data/sessions/` and can be resumed across conversations:
- Use `--session myproject` to name a session
- Sessions preserve loaded facts, rules, and query history
- Sessions support incremental knowledge base updates
- Each solver has its own session namespace

## Integration

This skill uses:
- `prolog-mcp`: runPrologQuery, loadProgram
- `clingo-mcp`: solve, getProgram
- `z3smt-mcp`: check_sat, solve, prove
- `folprover-mcp`: prove, add_premise
- `pyke-mcp`: query, prove_goal
- `logic-registry` for predicate resolution

## Notes

- Natural language queries are mapped to formal queries using the registry's predicate descriptions
- Complex queries may be decomposed into sub-queries for better accuracy
- The skill handles negation appropriately for each solver type
- Timeout helps prevent long-running queries from blocking