FOL Prover MCP Server
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
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 | {
"listChanged": false
} |
| experimental | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| proveA | Execute a FOL proof. Attempts to prove the conclusion from the given premises using the specified theorem prover (vampire, eprover, or prover9). |
| prove_sessionB | Execute a proof using the current session's premises and conclusion. |
| add_premiseA | Add a premise (axiom) to the current session for incremental proof building. |
| set_conclusionC | Set the conclusion (goal) to prove in the current session. |
| clear_sessionA | Clear all premises and conclusion from a session. |
| get_sessionA | Get the current state of a session including all premises and conclusion. |
| parse_formulaA | Parse and validate a FOL formula. Returns information about variables, constants, predicates, and whether the formula is syntactically valid. |
| convert_to_tptpC | Convert a FOL problem to TPTP format (standard format for theorem provers). |
| list_proversA | List available theorem provers and their status. |
| create_sessionB | Create a new named session for proof building. |
| list_sessionsA | List all active sessions. |
| switch_sessionB | Switch to a different session. |
| remove_premiseB | Remove a premise by index from the current session. |
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 13 tools
Each tool has a clear, distinct purpose. There is no overlap between adding/removing premises, setting conclusions, managing sessions, parsing formulas, or executing proofs. The two prove tools are differentiated by whether they use session state or direct inputs.
All tool names follow a consistent verb_noun pattern in snake_case, such as add_premise, clear_session, list_provers, and set_conclusion. The verbs are descriptive and uniform.
With 13 tools, the surface is well-scoped for a FOL prover server. It covers session management, formula parsing, multiple theorem provers, and TPTP conversion without excess.
The tool set covers the full proof workflow: create session, add premises, set conclusion, parse formulas, run proofs, and manage sessions. Minor gaps exist, such as no direct 'update premise' tool, but removing and re-adding works around this.