find-model
Find finite models that satisfy logical premises to demonstrate satisfiability in first-order logic.
Instructions
Find a finite model satisfying the given premises.
When to use: You want to show premises are satisfiable (have at least one model). When NOT to use: You want to prove a conclusion follows (use prove instead).
Example: premises: ["exists x P(x)", "all x (P(x) -> Q(x))"] → Returns: { success: true, model: { domain: [0], predicates: {...} } }
Performance notes:
Searches domains size 2 through max_domain_size (default: 10)
Larger domains take exponentially longer
Use domain_size to search a specific size only
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| premises | Yes | List of logical premises | |
| domain_size | No | Specific domain size to search (skips incremental search) | |
| max_domain_size | No | Maximum domain size to try (default: 10). Larger values may timeout. | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |