Loading ToolBench
MCP Server for First-Order Logic Resolution Prover Skill - Pure Python Standard Library implementation of Robinson's First-Order Resolution Refutation. Unifies atomic literals via Most General Unifier (MGU) and iteratively derives the empty clause (contradiction).
Single tool with minimal definition quality. Tool name 'unify_terms' lacks action verb prefix (should be 'compute_mgu' or 'unify_terms_mgu'). Description is 127 chars but lacks WHEN/WHY context for LLM selection. Input schema present but parameters lack type information (terms1/terms2 are arrays but element types undefined). No output schema documented. No error handling guidance. No parameter constraints or validation hints. Tool appears functional but severely under-specified for agent use.
Most General Unification algorithm - unifies two lists of terms and returns the MGU (Most General Unifier) substitution if unifiable
Tool name lacks action verb. 'unify_terms' is a noun phrase; should start with verb like 'compute_mgu' or 'unify_terms_with_mgu' to signal intent to LLM.
Input schema lacks element type definitions. 'terms1' and 'terms2' are declared as arrays but element type (string? object?) is undefined. LLM cannot validate input structure.
No output schema documented. Response structure {'unifiable': bool, 'mgu': dict} is inferred from code, not declared. LLM cannot plan downstream use of mgu field.
Description lacks WHEN/WHY context. States WHAT (MGU algorithm) but not WHEN to call it or what problem it solves. LLM cannot determine if this is the right tool for a logic task.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | F | 34 | 2026-07-28+ | v2 |
No error handling guidance. If unification fails (returns None), LLM receives {'unifiable': false, 'mgu': null} with no hint on what to try next or why it failed.