Skip to main content
Glama

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

TableJSON Schema
NameRequiredDescriptionDefault
premisesYesList of logical premises
domain_sizeNoSpecific domain size to search (skips incremental search)
max_domain_sizeNoMaximum domain size to try (default: 10). Larger values may timeout.
verbosityNoResponse verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info)

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/automenta/mcplogic'

If you have feedback or need assistance with the MCP directory API, please join our Discord server