MCP Logic is a self-contained, multi-engine server for first-order logic reasoning that proves theorems, finds models, detects counterexamples, and manages knowledge bases through a session-based API.
Core Reasoning:
Theorem Proving: Prove logical statements using resolution-based proving with automatic or explicit engine selection (Prolog, SAT, Z3, Clingo)
Model Finding: Find finite models (up to domain size 25) that satisfy given premises
Counterexample Detection: Find models that refute conclusions to show they don't logically follow
Syntax Validation: Check formula syntax with detailed error messages
Category Theory: Verify categorical diagram commutativity and retrieve axioms for categories, functors, monoids, groups, rings, lattices, and more
Session Management:
Create/Delete Sessions: Build knowledge bases incrementally with configurable TTL (default 30 minutes)
Assert/Retract/List Premises: Add, remove, or view formulas in a session's knowledge base
Query Sessions: Prove goals from accumulated premises
Clear Sessions: Remove all premises while keeping the session active
Advanced Features:
Multi-Engine Architecture: Prolog (Horn clauses), SAT (propositional/finite domain), Z3 (SMT with arithmetic/quantifiers/equality), Clingo (ASP for non-monotonic reasoning)
Arithmetic & Equality: Built-in support for arithmetic predicates (lt, gt, plus, minus, times, divides) and equality reasoning with congruence
Proof Traces: Step-by-step derivation output for debugging and education
Axiom Libraries: Pre-built sets for Peano arithmetic, ZFC set theory, propositional tautologies, equivalence relations, and algebraic structures
Verbosity Control: Minimal, standard, or detailed output for token efficiency
Advanced Techniques: Tseitin transformation, CNF conversion, DIMACS export, symmetry breaking, iterative deepening
CLI Tools: Check engine status, prove theorems, find models, and interactive REPL
Logic Syntax:
First-Order Logic: Universal (all x) and existential (exists x) quantifiers, connectives (->, <->, &, |, -)
Prover9 Compatible: Standard Prover9 syntax with functions and predicates
Click on "Install Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@MCP Logic prove that if all men are mortal and Socrates is a man, then Socrates is mortal"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
A self-contained MCP server for first-order logic reasoning, implemented in TypeScript with no external binary dependencies.
Original: https://github.com/angrysky56/mcp-logic/
✅ = Implemented | 🔲 = Planned | 🔬 = Research/Vision
Theorem Proving — Resolution-based proving via Tau-Prolog
Model Finding — Finite model enumeration (domain ≤25 with SAT)
Counterexample Detection — Find models refuting conclusions
Syntax Validation — Pre-validate formulas with detailed errors
CNF Clausification — Transform FOL to Conjunctive Normal Form
Tseitin Transformation — Linear-size CNF conversion for SAT (avoids exponential blowup)
DIMACS Export — Export CNF for external SAT solvers
Symmetry Breaking — Lex-leader for model search (reduces search space exponentially)
SAT-Backed Model Finding — Scale to domain 25+ with automatic SAT threshold
Isomorphism Filtering — Skip equivalent models (deferred until "findAllModels" use case)
Proof Traces — Step-by-step derivation output (via include_trace)
Multi-Engine Architecture — Automatic engine selection
Prolog Engine (Tau-Prolog) — Horn clauses, Datalog, equality
SAT Engine (MiniSat) — General FOL, non-Horn formulas
SMT Engine (Z3) — High-performance SMT solver with arithmetic & quantifiers
ASP Engine (Clingo) — Answer Set Programming (Constraints & Models)
Engine Parameter — Explicit engine selection via engine param
Iterative Deepening — Progressive inference limit strategy for complex proofs
Resource Management — Automatic cleanup of WASM resources (Z3 contexts)
Prover9 WASM — Optional high-power ATP (deferred until SAT+iterative proves insufficient)
Demodulation — Equational term rewriting (deferred until equality workloads show perf issues)
Arithmetic Support — Built-in: lt, gt, plus, minus, times, divides
Equality Reasoning — Reflexivity, symmetry, transitivity, congruence
Rewriting System — Knuth-Bendix style term rewriting for efficient equality handling (Prolog)
Extended Axiom Library — Ring, field, lattice, equivalence relation axioms
Function Interpretation — Full function support in model finding
Typed/Sorted FOL — Domain-constraining type annotations (research)
Modal Logic — Necessity, possibility operators (research)
Probabilistic Logic — Weighted facts, Bayesian inference (research)
Session-Based Reasoning — Incremental knowledge base construction with resource cleanup
Axiom Resources — Browsable libraries (category, Peano, ZFC, ring, lattice, etc.)
Reasoning Prompts — Templates for proof patterns
Verbosity Control — minimal/standard/detailed responses
Structured Errors — Machine-readable error codes and suggestions
Streaming Progress — Real-time progress notifications (via MCP notifications)
High-Power Mode — Extended limits with warning (via highPower option)
SMT (Z3 WASM) — Theory reasoning (arithmetic, arrays), Equality, Quantifiers.
ASP (Clingo) — Non-monotonic reasoning, defaults, preferences.
Neural-Guided — LLM-suggested proof paths with validation
Higher-Order Logic — Quantify over predicates (research)
Unit Tests — 265+ tests passing, 80%+ coverage
Pelletier Problems — P1-P10 benchmark suite (extensible to P1-P75)
Symmetry Benchmarks — Bell number validation tests
SAT Model Tests — Group theory and algebraic structure verification
Resilience Tests — Resource leak detection and complexity limit verification
TPTP Library Subset — Standard ATP benchmarks
Related MCP server: Congo River Compositional Intelligence
git clone <repository>
cd mcplogic
pnpm install
pnpm run buildpnpm startRun the comprehensive health check to verify build, tests, and engine availability:
pnpm run verifyAdd to your MCP configuration:
{
"mcpServers": {
"mcp-logic": {
"command": "node",
"args": ["/path/to/mcplogic/dist/index.js"]
}
}
}The package includes a CLI for offline usage and verification:
# Check engine status
mcplogic check
# Prove a theorem from a file
mcplogic prove problem.p
# Find a model
mcplogic model theory.p
# Interactive REPL
mcplogic replTool | Description |
prove | Prove statements using resolution with engine selection |
check-well-formed | Validate formula syntax with detailed errors |
find-model | Find finite models satisfying premises |
find-counterexample | Find counterexamples showing statements don't follow |
verify-commutativity | Generate FOL for categorical diagram commutativity |
get-category-axioms | Get axioms for category/functor/monoid/group |
translate-text | Translate natural language to FOL (requires LLM) |
Tool | Description |
create-session | Create a new reasoning session with TTL |
assert-premise | Add a formula to a session's knowledge base |
query-session | Query the accumulated KB with a goal |
retract-premise | Remove a specific premise from the KB |
list-premises | List all premises in a session |
clear-session | Clear all premises (keeps session alive) |
delete-session | Delete a session entirely |
The prove tool supports automatic or explicit engine selection:
{
"name": "prove",
"arguments": {
"premises": ["foo | bar", "-foo"],
"conclusion": "bar",
"engine": "auto",
"include_trace": true
}
}The include_trace option (boolean) enables step-by-step derivation output in the response, useful for debugging or understanding the proof path.
Engine | Best For | Capabilities |
| Horn clauses, Datalog | Equality, arithmetic, efficient unification |
| Propositional, Finite Domain | Boolean logic, CNF solving |
| General FOL, SMT | Arithmetic, Quantifiers, Equality |
| Answer Set Programming | Constraints (Experimental) |
| Default — selects based on formula | Analyzes clause structure & features |
Engine | Strength | Arithmetic | Quantifiers | Equality | Model Size |
Z3 | High (SMT) | ✅ | ✅ | ✅ | Large |
Clingo | High (ASP) | ✅ | Limited | ✅ | Large |
Prolog | Medium (Resolution) | ✅ | Limited (Horn) | ✅ | Small/Medium |
SAT | Low (Propositional) | ❌ | ❌ | ❌ | Small |
This server uses first-order logic (FOL) syntax compatible with Prover9:
all x (...) — Universal quantification (∀x)
exists x (...) — Existential quantification (∃x)
-> — Implication (→)
<-> — Biconditional (↔)
& — Conjunction (∧)
| — Disjunction (∨)
- — Negation (¬)
# All men are mortal, Socrates is a man
all x (man(x) -> mortal(x))
man(socrates)
# Transitivity of greater-than
all x all y all z ((greater(x, y) & greater(y, z)) -> greater(x, z))Resource URI | Description |
| Category theory axioms |
| Monoid structure |
| Group axioms |
| Ring structure |
| Lattice structure |
| Equivalence relations |
| Peano arithmetic |
| ZFC set theory basics |
| Propositional tautologies |
| Aristotelian syllogism patterns |
| Available reasoning engines (JSON) |
All tools support a verbosity parameter:
Level | Description | Use Case |
| Just success/result | Token-efficient LLM chains |
| + message, bindings, engineUsed | Default balance |
| + Prolog program, statistics | Debugging |
Model Size — Finder limited to domains ≤25 elements (using SAT)
Inference Depth — Complex proofs may exceed default limit (increase via inference_limit or use iterative strategy)
Higher-Order — Only first-order logic supported
Future improvements may address these limitations as real-world usage dictates.
pnpm run build # Compile TypeScript
pnpm test # Run test suite
pnpm run dev # Development mode with auto-reloadMIT
Potential enhancements will be driven by real-world usage:
Isomorphism Filtering — Skip equivalent models in exhaustive model enumeration
Proof Traces — Step-by-step derivation output for educational/debugging use cases
Demodulation — Equational term rewriting optimization for equality-heavy workloads
Streaming Progress — Real-time progress notifications for long-running operations
Extended Benchmarks — TPTP library subset and group theory problem suites
Advanced Engines — SMT (Z3), ASP (Clingo)
Evolution Engine — Genetic algorithm for evolving efficient proof strategies
Neural-Guided — LLM-suggested proof paths with validation
If you encounter errors related to z3-solver or clingo-wasm:
Ensure your environment supports WebAssembly.
In browser environments, ensure the .wasm files are served correctly. The check command can verify basic functionality in Node.js.
If you see OOM or memory errors, try running with the default engine (Prolog) or increasing the timeout/inference limits.
Ensure you have run pnpm install to get the latest type definitions. The browser build relies on specific overrides for WASM modules that are handled in src/engines/*/index.ts.
Add a formula to a session's knowledge base.
When to use: Building up premises incrementally in a session.
Example: session_id: "abc-123..." formula: "all x (man(x) -> mortal(x))" → Adds the formula to the session KB
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | Yes | Session ID from create-session | |
| formula | Yes | FOL formula to add to the knowledge base | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It states the tool adds a formula to a KB, implying a write operation, but doesn't disclose behavioral traits like error handling (e.g., invalid formulas), side effects, or response format. The example shows expected inputs but lacks output details. This is adequate but has clear gaps for a mutation tool.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is front-loaded with the core purpose, followed by a clear 'When to use' section and a concise example. Every sentence earns its place by adding value, with no redundant or verbose text. The structure is efficient and easy to parse.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given no annotations and no output schema, the description is moderately complete for a mutation tool. It covers the purpose and usage context well but lacks details on behavioral aspects like error conditions or response format. For a tool that modifies session state, more transparency would be beneficial, making it adequate but not fully comprehensive.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all parameters thoroughly. The description adds minimal value beyond the schema: it mentions 'session_id' and 'formula' in the example but doesn't provide additional semantics or usage nuances. This meets the baseline for high schema coverage.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the specific action ('Add a formula') and target resource ('to a session's knowledge base'), distinguishing it from sibling tools like 'list-premises' (reads) and 'retract-premise' (removes). The verb 'Add' is precise and the scope is well-defined.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explicitly includes a 'When to use' section that states 'Building up premises incrementally in a session,' providing clear context for when this tool should be used. This directly addresses the intended scenario without being misleading.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Check if logical statements are well-formed with detailed syntax validation.
When to use: Before calling prove/find-model to catch syntax errors early. When NOT to use: You already know the formula syntax is correct.
Example: statements: ["all x (P(x) -> Q(x))"] → Returns: { valid: true, statements: [...] }
Common syntax issues:
Use lowercase for predicates/functions: man(x), not Man(x)
Quantifiers: "all x (...)" or "exists x (...)"
Operators: -> (implies), & (and), | (or), - (not), <-> (iff)
| Name | Required | Description | Default |
|---|---|---|---|
| statements | Yes | Logical statements to check | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries full burden and does well by explaining the tool's behavior: it validates syntax, returns a structured result with validity status and processed statements, and lists common syntax issues. It doesn't cover all behavioral aspects like error handling or performance, but provides substantial context beyond basic purpose.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured and front-loaded with the core purpose, followed by usage guidelines, example, and common issues. Every sentence earns its place by providing actionable information without redundancy, making it efficient and easy to parse.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given no annotations and no output schema, the description does a good job covering the tool's context: it explains the validation purpose, usage scenarios, example output, and syntax rules. It could be more complete by detailing the output structure or error cases, but it's largely sufficient for a validation tool with clear parameters.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents both parameters thoroughly. The description doesn't add significant meaning beyond the schema—it mentions 'statements' in the example but doesn't elaborate on syntax rules beyond the common issues list, and doesn't discuss 'verbosity' at all. Baseline 3 is appropriate when schema does the heavy lifting.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the specific purpose: 'Check if logical statements are well-formed with detailed syntax validation.' This explicitly identifies the verb ('check'), resource ('logical statements'), and scope ('syntax validation'), distinguishing it from siblings like prove or find-model which perform different operations on statements.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides explicit guidance with dedicated 'When to use' and 'When NOT to use' sections. It specifies to use this tool 'Before calling prove/find-model to catch syntax errors early' and avoid it when 'You already know the formula syntax is correct,' clearly differentiating it from alternative tools.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Clear all premises from a session (keeps session alive).
When to use: Start fresh within the same session.
Example: session_id: "abc-123..." → Clears all premises, session remains valid
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | Yes | Session ID from create-session | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It clearly describes the core behavior ('Clears all premises, session remains valid'), which is essential for understanding this destructive operation. However, it doesn't mention potential side effects like whether this affects other session data or error conditions, leaving some behavioral aspects unspecified.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is efficiently structured with clear sections: purpose statement, usage guidelines, and an example. Each sentence serves a distinct purpose with zero wasted content, and the information is front-loaded with the most important details first.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a destructive operation with no annotations and no output schema, the description provides good context about what the tool does and when to use it. However, it doesn't describe what happens to the cleared premises (are they recoverable?) or what the response contains, leaving some completeness gaps for a mutation tool.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
With 100% schema description coverage, the schema already fully documents both parameters. The description doesn't add any parameter-specific information beyond what's in the schema, though it does provide an example showing session_id usage. This meets the baseline expectation when schema coverage is complete.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the specific action ('Clear all premises') and resource ('from a session'), with explicit differentiation from sibling tools like delete-session by noting 'keeps session alive'. This provides a precise verb+resource combination that distinguishes it from alternatives.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description includes a dedicated 'When to use' section that explicitly states 'Start fresh within the same session', providing clear guidance on when this tool should be used versus alternatives like delete-session (which would terminate the session). This gives explicit context for tool selection.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Create a new reasoning session for incremental knowledge base construction.
When to use: You want to build up premises incrementally and query multiple times. When NOT to use: Single query with all premises known upfront (use prove directly).
Example: ttl_minutes: 30 → Returns: { session_id: "uuid...", expires_at: ... }
Notes:
Sessions auto-expire after TTL (default: 30 minutes)
Maximum 1000 concurrent sessions
Session ID must be passed to all session operations
| Name | Required | Description | Default |
|---|---|---|---|
| ttl_minutes | No | Session time-to-live in minutes (default: 30, max: 1440) | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It effectively describes key traits: sessions auto-expire after TTL (with a default), there's a maximum of 1000 concurrent sessions, and the session ID must be passed to all session operations. However, it lacks details on error handling or performance limits beyond concurrency.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with clear sections (purpose, usage guidelines, example, notes), each sentence adds value without redundancy, and it's front-loaded with the core purpose. It efficiently conveys necessary information in a compact format.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (creating sessions with expiration and concurrency limits), no annotations, and no output schema, the description does a good job covering key aspects like purpose, usage, behavioral traits, and an example. However, it could be more complete by detailing the output structure beyond the example or error scenarios.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents both parameters (ttl_minutes and verbosity) thoroughly. The description adds minimal parameter semantics beyond the schema, such as implying ttl_minutes affects expiration in the example, but it doesn't provide additional syntax or format details. This meets the baseline of 3 when schema coverage is high.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description explicitly states the tool's purpose as 'Create a new reasoning session for incremental knowledge base construction,' which is a specific verb ('Create') + resource ('reasoning session') with clear scope ('incremental knowledge base construction'). It distinguishes from sibling tools like 'prove' by emphasizing incremental building versus single-query operations.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description includes explicit 'When to use' and 'When NOT to use' sections, clearly stating to use this tool for incremental premise building and querying multiple times, and to avoid it for single queries with known premises (using 'prove' instead). This provides direct guidance on alternatives and context.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Delete a session entirely.
When to use: Done with a session, want to free resources.
Example: session_id: "abc-123..." → Session is deleted and ID becomes invalid
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | Yes | Session ID to delete | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It discloses that deletion makes the session ID invalid, which is a key behavioral trait. However, it lacks details on permissions, error conditions, or resource implications beyond freeing resources, leaving some behavioral aspects unclear.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is front-loaded with the core purpose, followed by usage guidelines and an example. Each sentence earns its place by adding value: the first states the action, the second provides context, and the third illustrates usage. No wasted words, and structure enhances clarity.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given no annotations and no output schema, the description is moderately complete. It covers purpose, usage, and an example, but lacks details on return values, error handling, or deeper behavioral traits. For a destructive tool with 2 parameters, this is adequate but has clear gaps.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema fully documents both parameters. The description adds minimal value beyond the schema: it mentions 'session_id' in the example but doesn't explain parameter semantics further. Baseline 3 is appropriate as the schema handles the heavy lifting.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the specific action ('Delete') and resource ('a session entirely'), distinguishing it from sibling tools like 'clear-session' (which likely clears content) and 'create-session' (which creates). The verb+resource combination is precise and unambiguous.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explicitly includes a 'When to use' section that states 'Done with a session, want to free resources,' providing clear context for when this tool should be invoked versus alternatives like 'clear-session' or 'create-session.' This directly addresses sibling differentiation.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Find a counterexample showing the conclusion doesn't follow from premises.
When to use: You suspect a conclusion doesn't logically follow and want proof. When NOT to use: You want to prove the conclusion (use prove instead).
Example: premises: ["P(a)"] conclusion: "P(b)" → Returns counterexample where P(a)=true but P(b)=false
How it works: Searches for a model satisfying premises ∧ ¬conclusion. If found, proves the conclusion doesn't logically follow.
| Name | Required | Description | Default |
|---|---|---|---|
| premises | Yes | List of logical premises | |
| conclusion | Yes | Conclusion to disprove | |
| domain_size | No | Specific domain size to search | |
| max_domain_size | No | Maximum domain size to try (default: 10) | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It explains the tool's mechanism ('Searches for a model satisfying premises ∧ ¬conclusion') and outcome behavior ('If found, proves the conclusion doesn't logically follow'), which is valuable context beyond basic functionality. However, it doesn't mention performance characteristics like computational limits or error handling.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with clear sections (purpose, usage guidelines, example, mechanism), uses bullet points effectively, and every sentence adds value. It's appropriately sized for a tool with multiple parameters and sibling alternatives.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's logical reasoning complexity and lack of output schema, the description provides good contextual coverage: purpose, usage guidelines, example, and operational mechanism. It could be more complete by explaining the format of returned counterexamples or error conditions, but it's largely adequate for the agent's needs.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all parameters thoroughly. The description adds minimal parameter-specific information beyond the schema (e.g., it implies 'premises' and 'conclusion' are logical formulas in the example). This meets the baseline for high schema coverage.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description explicitly states the tool's purpose: 'Find a counterexample showing the conclusion doesn't follow from premises.' It uses specific verbs ('find', 'showing') and clearly distinguishes it from the 'prove' sibling tool, making the purpose unambiguous and differentiated.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description includes explicit 'When to use' and 'When NOT to use' sections, providing clear guidance on when to select this tool versus the 'prove' alternative. This directly addresses sibling tool differentiation and usage context.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Find a finite model satisfying the given premises.
When to use: You want to show premises are satisfiable (have at least one model). When NOT to use: You want to prove a conclusion follows (use prove instead).
Example: premises: ["exists x P(x)", "all x (P(x) -> Q(x))"] → Returns: { success: true, model: { domain: [0], predicates: {...} } }
Performance notes:
Searches domains size 2 through max_domain_size (default: 10)
Larger domains take exponentially longer
Use domain_size to search a specific size only
| Name | Required | Description | Default |
|---|---|---|---|
| premises | Yes | List of logical premises | |
| domain_size | No | Specific domain size to search (skips incremental search) | |
| max_domain_size | No | Maximum domain size to try (default: 10). Larger values may timeout. | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden. It effectively discloses key behavioral traits: the search strategy (domains size 2 through max_domain_size), performance implications ('larger domains take exponentially longer'), and the effect of the domain_size parameter ('skips incremental search'). It doesn't cover error handling or output format details, but provides substantial operational context.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with clear sections (purpose, usage guidelines, example, performance notes), each sentence adds value, and it's front-loaded with the core purpose. There's no redundant or wasted text, making it efficient for an agent to parse.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a tool with no annotations and no output schema, the description does well by covering purpose, usage, example, and performance. It explains the search behavior and constraints, which is crucial for a satisfiability tool. The main gap is the lack of output format details (only hinted in the example), but given the context, it's reasonably complete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the baseline is 3. The description adds some value through the example showing premises usage and performance notes about domain sizes, but doesn't significantly enhance parameter understanding beyond what the schema already documents. The example illustrates premises format but doesn't explain other parameters deeply.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description starts with a clear, specific statement: 'Find a finite model satisfying the given premises.' This explicitly states the verb ('find') and resource ('finite model'), and distinguishes it from sibling tools like 'prove' or 'find-counterexample' by focusing on satisfiability rather than proof or counterexamples.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description includes explicit 'When to use' and 'When NOT to use' sections, directly naming the alternative tool ('prove') and clarifying the distinction between satisfiability and proof. This provides clear guidance on tool selection in context.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Get FOL axioms for category theory concepts.
Available concepts:
category: Composition, identity, associativity axioms
functor: Preserves composition and identity
natural-transformation: Naturality condition
monoid: Binary operation with identity and associativity
group: Monoid with inverses
Example: concept: "monoid" → Returns axioms for monoid structure
| Name | Required | Description | Default |
|---|---|---|---|
| concept | Yes | Which concept's axioms to retrieve | |
| functor_name | No | For functor axioms: name of the functor (default: F) | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden. It discloses that the tool retrieves axioms (implying a read-only operation) and includes an example of output format, but lacks details on behavioral traits like error handling, rate limits, or authentication needs. The example adds some context but is not comprehensive.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is appropriately sized and front-loaded, starting with the core purpose, followed by a structured list of concepts and a clear example. Every sentence earns its place by providing essential information without redundancy.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the complexity (3 parameters, no output schema, no annotations), the description is somewhat complete but has gaps. It covers the purpose and concepts well, but lacks details on output format beyond the example, error cases, or how parameters like 'verbosity' affect behavior, making it adequate but not fully comprehensive.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all parameters. The description adds minimal value by listing concepts and providing an example that implies the 'concept' parameter usage, but does not explain parameter interactions or semantics beyond what the schema provides.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose with specific verb ('Get') and resource ('FOL axioms for category theory concepts'), and distinguishes it from siblings by focusing on retrieving axioms rather than operations like proving or verifying. The list of available concepts further specifies the scope.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides clear context for when to use this tool by listing available concepts and including an example, but it does not explicitly state when not to use it or mention alternatives among sibling tools (e.g., 'prove' or 'verify-commutativity').
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
List all premises in a session's knowledge base.
When to use: Review what has been asserted so far.
Example: session_id: "abc-123..." → Returns: { premises: ["all x (man(x) -> mortal(x))", "man(socrates)"] }
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | Yes | Session ID from create-session | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It discloses that the tool lists premises from a session's knowledge base and provides an example output format, which adds useful behavioral context. However, it doesn't mention potential limitations like pagination, error conditions, or performance characteristics, leaving some gaps for a tool with no annotation coverage.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with a clear purpose statement, usage guidelines, and an example, all in three concise sentences. Every sentence adds value without redundancy, and it's front-loaded with the core functionality.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given no annotations, no output schema, and 2 parameters with full schema coverage, the description is mostly complete. It covers purpose, usage, and provides an output example, but lacks details on error handling or behavioral constraints. For a read-only list tool, this is adequate but could be more comprehensive.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already fully documents both parameters (session_id and verbosity). The description doesn't add any parameter-specific information beyond what's in the schema, such as explaining the impact of verbosity levels on the output. Baseline 3 is appropriate when the schema does the heavy lifting.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the verb 'List' and resource 'premises in a session's knowledge base', making the purpose specific. It distinguishes from siblings like 'assert-premise' (adds premises) and 'query-session' (queries premises) by focusing on listing all premises without modification or querying.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explicitly includes a 'When to use' section stating 'Review what has been asserted so far', providing clear context for usage. It distinguishes from alternatives by implying this is for listing all premises rather than querying specific ones (vs. 'query-session') or modifying them (vs. 'assert-premise', 'retract-premise').
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Prove a logical statement using resolution.
When to use: You have premises and want to verify a conclusion follows logically. When NOT to use: You want to find counterexamples (use find-counterexample instead).
Example: premises: ["all x (man(x) -> mortal(x))", "man(socrates)"] conclusion: "mortal(socrates)" → Returns: { success: true, result: "proved" }
Common issues:
"No proof found" often means inference limit reached, not that the theorem is false
Try increasing inference_limit for complex proofs
| Name | Required | Description | Default |
|---|---|---|---|
| premises | Yes | List of logical premises in FOL syntax | |
| conclusion | Yes | Statement to prove | |
| inference_limit | No | Max inference steps before giving up (default: 1000). Increase for complex proofs. | |
| enable_arithmetic | No | Enable arithmetic predicates (lt, gt, plus, minus, times, etc.). Default: false. | |
| enable_equality | No | Auto-inject equality axioms (reflexivity, symmetry, transitivity, congruence). Default: false. | |
| engine | No | Reasoning engine: 'prolog' (Horn clauses), 'sat' (general FOL), 'auto' (select based on formula). Default: 'auto'. | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It effectively describes key behaviors: the tool performs logical proof via resolution, explains that 'No proof found' often means inference limit reached (not theorem false), and suggests increasing inference_limit for complex proofs. It also provides an example of the return format. While comprehensive, it could mention more about error handling or performance characteristics.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with clear sections (purpose, usage guidelines, example, common issues), each sentence adds value, and it's front-loaded with the core purpose. There's no redundant or wasted text, making it highly efficient for an AI agent to parse.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (7 parameters, logical reasoning), no annotations, and no output schema, the description does a strong job. It explains the tool's purpose, usage context, provides an example output, and addresses common pitfalls. However, without an output schema, it could more explicitly detail the full range of possible return values or error conditions beyond the example.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all 7 parameters thoroughly. The description adds minimal parameter-specific information beyond the schema (e.g., it mentions inference_limit in the 'Common issues' section). This meets the baseline of 3 where the schema does the heavy lifting, but the description doesn't significantly enhance parameter understanding.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description explicitly states the tool's purpose: 'Prove a logical statement using resolution.' It specifies the verb ('prove'), resource ('logical statement'), and method ('using resolution'), clearly distinguishing it from siblings like 'find-counterexample' or 'find-model' which serve different logical functions.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description includes dedicated 'When to use' and 'When NOT to use' sections, explicitly stating to use this tool for verifying conclusions from premises and to use 'find-counterexample' instead for finding counterexamples. This provides clear, actionable guidance on tool selection versus alternatives.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Query the accumulated knowledge base in a session.
When to use: After asserting premises, query for a conclusion.
Example: session_id: "abc-123..." goal: "mortal(socrates)" → Attempts to prove the goal from accumulated premises
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | Yes | Session ID from create-session | |
| goal | Yes | FOL formula to prove from the knowledge base | |
| inference_limit | No | Max inference steps (default: 1000) | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It describes the core behavior (attempting to prove a goal from accumulated premises) and includes an example showing expected inputs/outputs. However, it doesn't disclose important behavioral traits like error conditions, performance characteristics, what happens when the goal cannot be proven, or whether this is a read-only vs. mutating operation. The example adds some context but leaves gaps.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is perfectly structured and concise. It leads with the core purpose, follows with usage guidelines, and provides a concrete example. Every sentence earns its place: the first states what the tool does, the second tells when to use it, and the example illustrates practical application. No wasted words or redundant information.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the complexity (a query/proving tool with 4 parameters), lack of annotations, and no output schema, the description is moderately complete. It covers the purpose and usage context well but doesn't fully address behavioral aspects like what the response contains, error handling, or performance considerations. The example helps but doesn't substitute for explicit behavioral disclosure. For a tool of this complexity, more complete behavioral information would be beneficial.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already fully documents all four parameters. The description doesn't add any parameter-specific information beyond what's in the schema descriptions. The example shows usage of 'session_id' and 'goal' but doesn't explain their semantics further. With complete schema coverage, the baseline score of 3 is appropriate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: 'Query the accumulated knowledge base in a session.' This specifies the verb ('query') and resource ('accumulated knowledge base'), and distinguishes it from siblings like 'list-premises' (which lists premises) or 'prove' (which might be a different proving mechanism). However, it doesn't explicitly differentiate from 'find-model' or 'find-counterexample' which are also query-like operations.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides explicit usage guidance: 'After asserting premises, query for a conclusion.' This clearly states when to use the tool (after premises are asserted) and implies an alternative workflow (premises must be established first). It doesn't specify when NOT to use it or name alternatives directly, but the context is sufficiently clear for effective tool selection.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Remove a specific premise from a session's knowledge base.
When to use: You need to undo an assertion or explore alternative premises.
Example: session_id: "abc-123..." formula: "man(plato)" → Removes the exact formula if found
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | Yes | Session ID from create-session | |
| formula | Yes | Exact formula to remove (must match what was asserted) | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It states the tool 'Removes the exact formula if found,' which clarifies it's a destructive operation (mutation) with conditional execution. However, it doesn't mention error handling (e.g., what happens if formula not found), permissions, or rate limits, leaving some behavioral aspects unspecified.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is front-loaded with the core purpose, followed by a clear usage guideline and a concrete example. Every sentence earns its place: the first states what it does, the second when to use it, and the third illustrates with parameters. No wasted words, and the structure is logical and efficient.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's moderate complexity (destructive operation with conditional removal), no annotations, and no output schema, the description does well by covering purpose, usage, and parameter behavior. However, it lacks details on error cases or return values, which would be helpful for a mutation tool. It's mostly complete but has minor gaps in behavioral context.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all parameters thoroughly. The description adds minimal value beyond the schema by emphasizing 'Exact formula to remove (must match what was asserted)' in the example, reinforcing the matching requirement. With high schema coverage, the baseline is 3, but the added emphasis on exact matching justifies a slightly higher score.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the specific action ('Remove') and target resource ('a specific premise from a session's knowledge base'), distinguishing it from siblings like 'clear-session' (removes all premises) or 'delete-session' (removes entire session). The verb+resource combination is precise and unambiguous.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explicitly provides a 'When to use' section that states 'You need to undo an assertion or explore alternative premises,' giving clear context for usage. It also distinguishes from alternatives by specifying removal of 'a specific premise' rather than all premises (clear-session) or the session itself (delete-session).
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Verify that a categorical diagram commutes by generating FOL premises and conclusion.
When to use: You have a categorical diagram and want to verify path equality. When NOT to use: For non-categorical reasoning (use prove directly).
Example: path_a: ["f", "g"], path_b: ["h"] object_start: "A", object_end: "C" → Generates premises/conclusion for proving compose(f,g) = h
Output: Returns premises and conclusion to pass to the prove tool.
| Name | Required | Description | Default |
|---|---|---|---|
| path_a | Yes | List of morphism names in first path | |
| path_b | Yes | List of morphism names in second path | |
| object_start | Yes | Starting object | |
| object_end | Yes | Ending object | |
| with_category_axioms | No | Include basic category theory axioms (default: true) | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries full burden and does well by explaining the tool's behavior: it generates premises/conclusion for proving path equality, mentions the output format (premises and conclusion to pass to prove tool), and includes an example. However, it doesn't cover potential limitations like error conditions or computational constraints.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Well-structured with clear sections: purpose statement, usage guidelines, example, and output description. Every sentence adds value without redundancy, and the information is front-loaded with the core purpose first.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a tool with no annotations and no output schema, the description provides good context: purpose, usage boundaries, example, and output format. It could be more complete by explaining what happens with the 'with_category_axioms' parameter or potential failure modes, but covers the essential behavioral aspects well.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all 6 parameters thoroughly. The description adds minimal value beyond the schema through the example showing how path_a, path_b, object_start, and object_end work together. This meets the baseline for high schema coverage.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the specific verb ('verify') and resource ('categorical diagram commutes'), explaining it generates FOL premises and conclusion for path equality. It distinguishes from sibling tools like 'prove' by focusing specifically on diagram verification rather than general proving.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Explicitly provides 'When to use' (for categorical diagram verification) and 'When NOT to use' (for non-categorical reasoning, directing to 'prove' instead). This gives clear guidance on when to select this tool versus alternatives among siblings.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections. Dates show when Glama detected each change.
assert-premisecheck-well-formedclear-sessioncreate-sessiondelete-sessionfind-counterexamplefind-modelget-category-axiomslist-premisesprovequery-sessionretract-premiseverify-commutativityEach tool has a clearly distinct purpose with minimal overlap. For example, prove and find-counterexample are complementary for logical verification, while session management tools like create-session and delete-session handle specific lifecycle stages. The descriptions explicitly state when to use and when not to use each tool, preventing confusion.
Most tools follow a consistent verb-noun pattern with hyphens (e.g., assert-premise, clear-session, find-model). However, get-category-axioms and verify-commutativity slightly deviate by using more descriptive nouns, but they remain readable and fit the overall style. The naming is predictable and aids in understanding tool functions.
With 13 tools, the set is well-scoped for a logic reasoning server, covering core operations like session management, premise handling, proof verification, and model finding. Each tool serves a specific role without redundancy, such as list-premises for review and retract-premise for corrections, making the count appropriate for the domain.
The tool set provides comprehensive coverage for logical reasoning workflows, including session lifecycle (create, clear, delete), premise management (assert, list, retract), verification (prove, find-counterexample, query-session), and specialized tasks like model finding and category theory support. No obvious gaps exist; agents can perform end-to-end reasoning tasks effectively.
Unclaimed servers have limited discoverability.
If you are the server author, to access and configure the admin panel.
Deterministic reasoning stack for AI agents: simulate, decide & compute, plus cross-domain tools.
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
Conversational what-if simulation: build, diagnose and compare Petri-net models; CC0 catalog.
Agent-first CAD: editable .kcad.ts source, deterministic review, OpenCASCADE kernel.
We provide all the information about MCP servers via our MCP API.
curl -X GET 'https://glama.ai/api/mcp/v1/servers/autonull/mcplogic'
If you have feedback or need assistance with the MCP directory API, please join our Discord server
