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)
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations provided, the description carries the full burden. It effectively discloses key behavioral traits: the search strategy (domains size 2 through max_domain_size), performance implications ('larger domains take exponentially longer'), and the effect of the domain_size parameter ('skips incremental search'). It doesn't cover error handling or output format details, but provides substantial operational context.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured with clear sections (purpose, usage guidelines, example, performance notes), each sentence adds value, and it's front-loaded with the core purpose. There's no redundant or wasted text, making it efficient for an agent to parse.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a tool with no annotations and no output schema, the description does well by covering purpose, usage, example, and performance. It explains the search behavior and constraints, which is crucial for a satisfiability tool. The main gap is the lack of output format details (only hinted in the example), but given the context, it's reasonably complete.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100%, so the baseline is 3. The description adds some value through the example showing premises usage and performance notes about domain sizes, but doesn't significantly enhance parameter understanding beyond what the schema already documents. The example illustrates premises format but doesn't explain other parameters deeply.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description starts with a clear, specific statement: 'Find a finite model satisfying the given premises.' This explicitly states the verb ('find') and resource ('finite model'), and distinguishes it from sibling tools like 'prove' or 'find-counterexample' by focusing on satisfiability rather than proof or counterexamples.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines5/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description includes explicit 'When to use' and 'When NOT to use' sections, directly naming the alternative tool ('prove') and clarifying the distinction between satisfiability and proof. This provides clear guidance on tool selection in context.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Install Server

Other Tools

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/autonull/mcplogic'

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