Loading ToolBench
MCP server for logical reasoning using Prover9 and Mace4 theorem provers
The server provides 10 logical reasoning tools with well-structured schemas and clear descriptions. All tools have proper JSON Schema definitions with types and parameter descriptions. However, several tools lack depth in their descriptions (under 100 chars in some cases), and error handling strategies are not explicitly documented in the tool definitions. Tool names follow good verb_noun conventions (prove, find_counterexample, check_*). Output schemas are not explicitly documented in the visible code, which is a notable gap. The server targets a specialized domain (logic/theorem proving) where descriptions could be more accessible to non-specialist LLM agents.
Generate abductive explanations (hypotheses that would make observations logically follow from background knowledge)
Ask the logic advisor (TwIL-LM3 language model) for guidance on logical reasoning problems
Check if a formula is contingent (true in some models, false in others) using HCC-based verification
Check if premises entail a conclusion using Z3 SMT solver
Check if a set of logical formulas is satisfiable using Z3 SMT solver
Classify a logical formula into decidable/undecidable fragments and determine decision procedure applicability
Search for a finite model that satisfies the premises but violates the conclusion, using Mace4 model finder
Output schemas not documented in tool definitions. While input schemas are complete, the expected return types and fields are not explicitly declared in the visible tool registration. This forces LLMs to infer output structure from descriptions alone.
Tool descriptions lack context on when to use each tool and what to do with results. E.g., 'classify_fragment' (60 chars) does not explain why an LLM would call it or how the classification output should influence subsequent reasoning. Descriptions should be 50-200 chars and answer WHAT, WHEN, and next steps.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-21 | C | 60 | <=2025-11-25 | v2 |
| 2026-03-09 | D | 55 | - | v1 |
Retrieve category theory axioms for use in logical proofs
Attempt to prove that a conclusion logically follows from given premises using Prover9 theorem prover
Validate that given formulas are syntactically correct logical expressions
No explicit error handling or recovery guidance in tool descriptions. E.g., 'prove' does not document timeout behavior, what happens if Prover9 is unavailable, or how to interpret a resource limit vs. genuine unprovability. The code shows _classify_search_failure logic, but this is not surfaced in the tool description.
'ask_logic_advisor' description is vague ('guidance on logical reasoning problems'). Does not warn that the advisor is optional and may be unavailable, or what happens when it is disabled. The pyproject.toml notes the advisor is optional and requires extra setup, but the tool description does not mention this.
Domain-specific terminology in descriptions assumes LLM familiarity with logic (e.g., 'satisfiable', 'entailment', 'contingency', 'abductive explanation'). For non-specialist agents, these could be more accessible. E.g., 'check_satisfiable' should explain it tests if formulas can ALL be true together.