Loading ToolBench
MCP server for First-Order Logic theorem proving using Vampire, E, and Prover9
FOL Prover MCP provides 10 well-structured tools with complete input schemas and descriptions. Tool naming follows verb-first conventions (prove, add_premise, set_conclusion, etc.) and is generally clear. All tools have non-empty descriptions (average ~120 chars, within the 34-392 baseline). However, several tools lack output schema documentation, the code shows input schemas explicitly but does not document what fields/structure the tool returns. Session-based tools (prove_session, add_premise, set_conclusion, get_session, create_session, clear_session) form a coherent composition pattern for incremental proof building. Error handling is present but minimal; code references INTERNAL_ERROR and INVALID_PARAMS types but does not show actionable recovery guidance in descriptions. No tool annotations (readOnlyHint, destructiveHint, idempotentHint) are visible in the schema registration, despite clear READ_ONLY vs WRITE semantics being known. Parameter descriptions are present and explain the FOL notation well (Unicode operators documented), but do not include ranges, constraints, or format details for timeout or prover selection. Output schemas are completely undocumented, we cannot see what prove() returns (success flag? proof steps? error details?) from the code provided.
Add a premise (axiom) to the current session for incremental proof building.
Clear all premises and conclusion from a session.
Convert a FOL problem to TPTP format (standard format for theorem provers).
Create a new named session for proof building.
Get the current state of a session including all premises and conclusion.
List available theorem provers and their status.
Parse and validate a FOL formula. Returns information about variables, constants, predicates, and whether the formula is syntactically valid.
Output schemas are completely undocumented. The code defines input schemas but never documents what prove(), prove_session(), parse_formula(), convert_to_tptp(), list_provers(), or get_session() return. LLMs cannot plan downstream tool calls or extract the right fields without knowing the response structure.
No tool annotations (readOnlyHint, destructiveHint, idempotentHint) are present in the schema definitions, despite clear semantic differences (e.g., add_premise, set_conclusion, clear_session are WRITE operations; prove, get_session are READ_ONLY). This prevents LLMs and clients from understanding safety/idempotency properties without reading descriptions.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | D | 54 | <=2025-11-25 | v2 |
Execute a FOL proof. Attempts to prove the conclusion from the given premises using the specified theorem prover (vampire, eprover, or prover9).
Execute a proof using the current session's premises and conclusion.
Set the conclusion (goal) to prove in the current session.
Session parameter handling is implicit and underdocumented. Most tools accept an optional 'session' parameter that 'defaults to current session', but the code does not explain how the current session is tracked or changed, when a user would pass an explicit session name vs rely on the default, or how multi-session workflows are intended. An LLM cannot reason about session scope without this clarity.
Error handling guidance is missing. Descriptions do not explain what errors can occur or what the LLM should do next. For example, prove() could fail if premises are malformed FOL, if the prover is not installed, or if the proof times out, none of these recovery paths are documented in the tool description.
Parameter constraints are underspecified. The 'timeout' parameter defaults to 30 seconds but has no documented minimum or maximum, which means an LLM could pass a timeout of 0, 999999, or negative values. Similarly, 'prover' enum includes 'simple' (built-in) vs external provers, but descriptions do not explain when 'simple' is appropriate vs full Vampire/E, or what limitations it has.
list_provers() description is generic ('List available theorem provers and their status') and does not explain what 'status' means, is it installed/not installed? online/offline? Available for use/requires configuration? This prevents an LLM from understanding when to call it or what to do with the response.