AtpMcp
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
| STAREXEC_PASS | No | Password for StarExec authentication. | |
| STAREXEC_USER | No | Username for StarExec authentication. | |
| ATP_MCP_CONFIG | No | Path to the configuration file (atp_mcp.exs). Used when the first config file location (atp_mcp --config PATH) is not provided. | |
| ISABELLE_PASSWORD | No | Password for connecting to a remote Isabelle server. |
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| list_backendsA | List the AtpClient backends this MCP server exposes (sotptp, isabelle, local_exec, starexec) and their human-readable labels. |
| describe_szsA | Return a text description of the SZS Ontology (https://tptp.org/UserDocs/SZSOntology/), the vocabulary every other tool uses to report verdicts. Enumerates each Success status (Theorem, Unsatisfiable, Satisfiable, CounterSatisfiable, …) and NoSuccess status (GaveUp, Timeout, ResourceOut, Forced, …) with a short gloss so an agent can decide what a verdict means without leaving the MCP session. |
| verify_backendA | Probe a backend's configuration and reachability. Returns "OK" if the backend is wired up correctly, otherwise an error describing what is missing or unreachable. |
| query_backendB | Run a TPTP-format problem through any AtpClient backend and return the
normalised SZS Ontology verdict (Theorem, Unsatisfiable, Satisfiable,
CounterSatisfiable, GaveUp, Timeout, ResourceOut, …). The unified
|
| list_proversA | List every theorem prover system available on SystemOnTPTP. |
| run_proverA | Submit a TPTP-format problem to a specific prover on SystemOnTPTP.
Returns the SZS Ontology verdict (Theorem, Unsatisfiable, Satisfiable,
CounterSatisfiable, GaveUp, Timeout, ResourceOut, …) or raw output.
Call |
| compare_proversA | Submit a TPTP problem to multiple SystemOnTPTP provers simultaneously
and report SZS Ontology verdicts side-by-side. Useful for
cross-checking or finding the fastest prover for a problem class.
Call |
| prove_isabelleA | Submit a hand-written Isabelle/HOL theory to the Isabelle server
configured for this MCP server. The theory text is written into the
configured shared directory and processed via |
| lint_problemA | Run syntax and type diagnostics on a TPTP problem. By default combines
the in-process structural checker with TPTP4X on SystemOnTPTP; pass
|
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored across 9 tools
Most tools have clearly distinct roles, but `query_backend` and `run_prover` both submit a TPTP problem and return SZS verdicts, differing mainly by abstraction level and target. The descriptions help clarify when to use `prove_isabelle` versus `query_backend` with the Isabelle backend, but there is still some potential for confusion between the unified query path and the direct prover path.
All tools use a consistent snake_case verb_noun pattern (`list_backends`, `verify_backend`, `query_backend`, `run_prover`, `compare_provers`, etc.). Proper nouns and acronyms like `szs` and `isabelle` are used naturally without breaking the convention.
Nine tools is well-scoped for an ATP integration server covering discovery, verification, execution, comparison, linting, and Isabelle-specific proving. Each tool appears to earn its place without obvious redundancy.
The surface covers the core ATP lifecycle well: listing backends/provers, understanding SZS verdicts, verifying configuration, running and comparing provers, linting problems, and proving Isabelle theories. Minor gaps remain around managing or inspecting the long-lived Isabelle session and retrieving raw output consistently across all execution paths.