Skip to main content
Glama
jcschuster

AtpMcp

lint_problem

Validate TPTP problems by running syntax and type diagnostics. Combines a local structural checker with TPTP4X by default, or restricts checks to the local backend.

Instructions

Run syntax and type diagnostics on a TPTP problem. By default combines the in-process structural checker with TPTP4X on SystemOnTPTP; pass backends: ["local"] for the cheap pass only.

Input Schema

NameRequiredDescriptionDefault
problemYesTPTP problem text
backendsNoWhich lint backends to run (default: both)

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observedv0.8.1

TDQS

A3.6/5.0
Behavior3/5

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

With no annotations, the description carries the full behavioral burden. It usefully discloses that the default combines an in-process structural checker with TPTP4X on SystemOnTPTP and that local is the cheap pass, but it omits return format, external-service implications, timeout/error behavior, and resource costs.

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?

Two sentences, front-loaded with the core action and followed by the default/backend tradeoff. Every sentence adds useful information with no repetition or wasted phrasing.

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

Completeness3/5

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

For a low-complexity, two-parameter diagnostic tool with full schema coverage, it covers purpose and backend selection adequately. But with no output schema, the description should ideally state what diagnostics are returned and whether results are structured, so the agent knows what to expect.

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

Parameters4/5

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

Schema coverage is already 100%, so the baseline is 3. The description earns an extra point by explaining the practical meaning behind the backends parameter: default means combining local structural checking with TPTP4X, while local-only is the cheap pass.

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

Purpose4/5

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

The description states a specific verb and resource: "Run syntax and type diagnostics on a TPTP problem." This clearly distinguishes it from prover-running siblings, though it does not explicitly contrast it with tools like verify_backend or query_backend.

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

Usage Guidelines3/5

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

It explains the default backend behavior and when to pass backends: ["local"] for the cheap pass, which is useful parameter-level guidance. However, it does not say when to use this tool versus other diagnostic or verification siblings, nor does it state explicit exclusions.

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