Skip to main content
Glama
snegi26

Euclid-MCP

by snegi26
OverviewSchemaRelated ServersScoreDiscussions
Python
Hybrid

Euclid-MCP

Deterministic logical reasoning for MCP clients, with proof trees.

Reference implementation of Euclid-MCP: A Model Context Protocol Server for Deterministic Logical Reasoning via Prolog (Bogliolo, arXiv:2607.21412v1).

An LLM is good at describing a world and bad at deducing over it. Euclid-MCP splits those jobs: the model writes facts, rules and a query in a small declarative language (Euclid-IR); the server compiles that to Prolog, runs it in a sandboxed subprocess, and returns exact answers with a derivation for every one of them. On a 1,000-user RBAC knowledge base where natural-language reasoning hallucinates counts, this returns 31 and 103 — every time, with the proof attached.

┌────────────┐   Euclid-IR    ┌──────────────────────────────┐   Prolog    ┌────────────┐
│ LLM client │ ─────────────▶ │        Euclid-MCP server     │ ──────────▶ │ SWI-Prolog │
│ (MCP)      │                │  parse → lower → sanitize →  │  (subproc)  │  (deduce)  │
│            │ ◀───────────── │  run → parse JSON → typed    │ ◀────────── │            │
└────────────┘  solutions +   │  result                      │  JSON       └────────────┘
                proof trees   └──────────────────────────────┘

Install

pip install euclid-mcp

SWI-Prolog is a system dependency, not a pip dependency. You need swipl 9.0 or later on PATH:

Platform

Command

Debian/Ubuntu

apt-get install -y swi-prolog

macOS

brew install swi-prolog

Fedora

dnf install pl

Windows

swi-prolog.org/download

Check that the backend is visible:

python -m euclid_mcp --check
# euclid-mcp 0.1.0
# backend: SWI-Prolog version 9.0.4 for x86_64-linux

Or skip the install entirely and use the Docker image, which bundles SWI-Prolog:

docker build -t euclid-mcp .
docker run --rm -p 8000:8000 euclid-mcp
curl -s localhost:8000/health

Related MCP server: Pyke MCP Server

Connect an MCP client

python -m euclid_mcp speaks MCP over stdio. For Claude Desktop, Cursor, or any other MCP client, add:

{
  "mcpServers": {
    "euclid": {
      "command": "python",
      "args": ["-m", "euclid_mcp"]
    }
  }
}

Euclid-IR in one screen

One logical item per line. Predicates and constants are lowercase; variables start with $.

@version 1.0                                    # optional directive

parent(tom, bob)                                # a fact - must be ground
parent(bob, ann)

mortal($x) IF human($x)                         # a rule
ancestor($x, $y) IF parent($x, $y)
ancestor($x, $y) IF parent($x, $z) AND          # continues: line ends in AND
    ancestor($z, $y)

blocked($u) IF NOT active($u)                   # closed-world negation
stale($u) IF last_login($u, $d) AND $d > 90     # arithmetic comparison
resource(apple, $color, _, _, _, _)             # _ is a wildcard

? ancestor(tom, $who)                           # a query

Comparison operators: > >= < =< =:= =\= is. Comments: # or //, whole-line or inline.

There is also an equivalent YAML form; both load into the same AST.

version: "1.0"
facts:
  - parent(tom, bob)
rules:
  - head: ancestor($x, $y)
    body: [ parent($x, $y) ]
queries:
  - ? ancestor(tom, $who)

Deliberately not supported

Not supported

Do this instead

disjunction (OR, ;)

write several rules with the same head

lists [...]

model a collection as several facts

strings

use lowercase atoms

cut !

nothing — proofs are always complete

findall / bagof / setof

precompute counts as facts (permission_count(u, 17))

runtime assert / retract

use the what_if tool

modules

—

These restrictions are the point: they keep every proof finite, traceable and reproducible, and they keep the language portable to a second backend. Each one is rejected at parse time with a message that names the construct and the workaround.

The four tools

All four are stateless and read-only: knowledge in, typed result out.

Tool

Purpose

reason

Prove a goal; return every solution with its proof tree

diagnose

Explain a result: why, why_not, what_needs

what_if

Apply +/- fact changes and diff the before/after solutions

check_kb

Static validation — syntax, undefined predicates, cycles, duplicates

They are designed around a translate-run-inspect-repair loop:

  1. Validate — check_kb confirms the knowledge base is well-formed (no backend needed, so it is cheap).

  2. Translate — the client emits Euclid-IR: facts, rules, query.

  3. Run — reason returns answers plus derivations.

  4. Inspect — on a surprising result, diagnose with why or why_not.

  5. Repair — refine the knowledge base from the diagnosis; re-run.

  6. Explore — what_if tests a hypothetical change before committing to it.

Every failure — a parse error, an unsupported construct, an oversized payload, a timeout — comes back as ok: false with an actionable message rather than an exception, so the client can correct itself and retry.

reason

reason(knowledge="""
parent(tom, bob)
parent(bob, ann)
ancestor($x, $y) IF parent($x, $y)
ancestor($x, $y) IF parent($x, $z) AND ancestor($z, $y)
""", query="ancestor(tom, $who)")
solution_count: 2, truncated: false
  $who = ann
    ancestor(tom, ann)  [rule]
      parent(tom, bob)  [fact]
      ancestor(bob, ann)  [rule]
        parent(bob, ann)  [fact]
  $who = bob
    ancestor(tom, bob)  [rule]
      parent(tom, bob)  [fact]

An empty solutions list with ok: true is a real answer: under closed-world semantics the knowledge base does not entail the goal.

diagnose

diagnose(knowledge="human(socrates)", query="mortal(plato)", mode="why_not")
# holds: false
# findings: ["No facts or rules defined for 'mortal'"]
# conclusion: The knowledge base defines nothing for `mortal`, so any goal that
#             depends on it fails. Add the missing facts or a rule whose head uses it.

what_needs goes further and abduces the repair: given mortal($x) IF human($x) it answers that adding human(plato) would make the goal hold.

what_if

what_if(base_knowledge=rbac_kb,
        modifications="- has_role(eng_0002, intern)\n+ has_role(eng_0002, senior_dev)",
        query="user_has_permission(eng_0002, deploy_code)")
# before_count: 0, after_count: 1, delta: 1

A - line that matches no existing fact is an error, not a silent no-op: a scenario built on a false premise would give a misleading answer.

REST API

For automation platforms (n8n, Zapier, Make) and remote access. The endpoints call the same tool functions with the same Pydantic models — one schema, two surfaces.

python -m euclid_mcp --http --host 0.0.0.0 --port 8000

Method

Path

Body

Response

POST

/reason

ReasonInput

ReasonResult

POST

/diagnose

DiagnoseInput

DiagnosisResult

POST

/what-if

WhatIfInput

WhatIfResult

POST

/check-kb

CheckKBInput

KBCheckResult

GET

/health

—

{"status": "ok", "swipl": "...", "version": "..."}

OpenAPI docs are at /docs. CORS is off by default; set EUCLID_MCP_CORS_ORIGINS to a comma-separated origin list (or *) to enable it for browser clients.

Do not expose this API to an untrusted network as-is. There is no authentication, authorization or rate limiting, and nothing caps concurrent work. Every request spawns a reasoning subprocess that may run for the full 30 s timeout — and what_if and diagnose each run the backend twice, so one request can buy ~60 s of CPU. A handful of small requests will saturate every core. The CLI binds loopback by default; the container image binds 0.0.0.0.

Put a reverse proxy in front of it providing auth, rate limiting and a concurrency cap, or keep it on a trusted network. See THREATMODEL.md finding F4.

Safety

The LLM cannot make the backend do anything but deduce.

  • Size cap — knowledge over 500 KB is rejected before parsing.

  • Time bound — every program runs under a 30 s wall clock, enforced both by the subprocess and by call_with_time_limit/2 inside Prolog.

  • Allow-list — only constructors reachable from the grammar can be emitted. File I/O, network, shell, consult, use_module and runtime assert/retract are unreachable from Euclid-IR and rejected if they somehow appear.

  • Generated-text audit — the lowered program is scanned for denied built-ins before it runs, so a lowering bug cannot smuggle one through.

  • In-Prolog verification — before executing anything, the harness walks every clause body and refuses to run if it finds a goal that is not a declared knowledge-base predicate, a comparison, or a negation of those.

  • No shell=True, argv lists only, temp files removed in a finally.

What is not defended

Read THREATMODEL.md before deploying. In short:

  • Soundness is relative to the encoded rules, not to reality. The model writes the knowledge base; wrong premises yield wrong conclusions with valid proofs. The proof tree is what makes that auditable — treat the knowledge base as the security-relevant artefact and review it.

  • A zero-solution answer can mean "search depth exhausted", not "false" — the two are currently indistinguishable, and the answer can flip when max_depth rises (finding F1).

  • solution_count is what was returned, not what exists. Always check truncated before treating it as a total (F2).

  • The REST API is unauthenticated with no rate limiting (F4, above).

  • Memory is not bounded — only wall-clock time is (F5).

Determinism

Same knowledge + same query ⇒ byte-identical solution set, every run. Clauses are emitted in source order, solutions are sorted by a total order over their bindings and proofs, and nothing is seeded randomly.

Examples and benchmarks

examples/07_it_security_compliance/ is a three-layer IT-security and compliance knowledge base — CIS controls, a role hierarchy and environment/classification policy, then generated user and resource data — in a small (~30 users) and a large (~200 users) variant, so the same rules can be seen to scale unchanged.

python benchmarks/run_benchmarks.py          # accuracy + latency, exits non-zero on a miss
python benchmarks/generate_large_rbac.py     # regenerate the 1,000-user RBAC KB

evals/evaluation.xml holds ten verified question/answer pairs for MCP evaluation harnesses.

Architecture notes

The backend is a tactical choice, not an architectural dependency. ir/, tools/ and the MCP surface never mention Prolog; only lowering/ does. A Datalog or SMT backend would slot in behind the same LoweredProgram and EngineResult types.

Reasoning runs as a subprocess rather than through FFI (pyswip/MQI) for portability: no compiled extension, no persistent process, trivial to containerize. The cost is one process launch per call, roughly 30-60 ms. If that ever dominates the sub-second budget, engine/runner.py can be swapped for an MQI-backed runner behind the same signature without touching anything else.

Development

pip install -e ".[dev]"
ruff check . && ruff format --check .
mypy --strict src
pytest                      # add -m "not requires_swipl" to skip backend tests

Layout, conventions and the milestone plan are in SPEC.md, CLAUDE.md and specs/.

License

MIT. See LICENSE.

Available Tools

4 tools
check_kbA
Read-onlyIdempotent

Validate a knowledge base statically, without running it.

Cheap and backend-free: call it before reason when you have just written or edited a knowledge base. It catches syntax errors, predicates used but never defined, recursion with no base case, and duplicate facts or rules.

Returns KBCheckResult:

  • valid (bool): false only when the knowledge base does not parse.

  • errors (list of str): parse failures, with line and column.

  • warnings (list of str): undefined predicates, possible non-termination, duplicates. Warnings do not prevent reasoning.

  • facts_count, rules_count (int): items found.

  • predicates_count (int): distinct name/arity predicate symbols.

ParametersJSON Schema
NameRequiredDescriptionDefault
paramsYes

Output Schema

ParametersJSON Schema
NameRequiredDescription
validYesFalse when the knowledge base does not parse.
errorsNoProblems that prevent reasoning, with line/column.
warningsNoUndefined predicates, possible non-termination, duplicates.
facts_countNo
rules_countNo
predicates_countNoDistinct predicate symbols.

TDQS

A4.3/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare the tool as read-only, idempotent, and non-destructive. The description adds behavioral details: it is cheap, backend-free, and catches specific errors and warnings, enriching the agent's understanding beyond annotations.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured and concise, starting with the core purpose, followed by usage guidance, error types, and return fields. Every sentence adds value without redundancy.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the simple parameter schema (one string) and detailed description of the output (KBCheckResult fields), the description provides complete information for an agent to use the tool effectively.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The description does not elaborate on the single 'knowledge' parameter, but the input schema provides a thorough explanation of the format. Since the schema covers the parameter adequately, a baseline score of 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool validates a knowledge base statically without running it, and distinguishes it from 'reason' by recommending calling it before reasoning. This is specific and differentiates from siblings.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

It explicitly advises using this tool before 'reason' after editing a knowledge base, providing clear context. It does not include exclusions, but the usage context is well-defined.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

diagnoseA
Read-onlyIdempotent

Explain why a query holds, why it fails, or what would make it true.

Reach for this when reason returns something you did not expect. Modes:

  • why: the goal holds and you want the derivation.

  • why_not: the goal fails and you want the missing facts or rules named. Reports predicates with no definition at all, then the deepest sub-goals that could not be proved.

  • what_needs: the goal fails and you want the smallest set of facts that would make it true (bounded to 3 assumptions over base predicates).

Returns DiagnosisResult:

  • ok (bool): false when the request could not be evaluated.

  • holds (bool): whether the goal currently holds.

  • findings (list of str): observations, most actionable first.

  • conclusion (str): a human-readable summary; for why it includes the rendered derivation.

  • proof (object | null): the derivation tree, present when the goal holds.

  • error (str | null): a readable message when ok is false.

ParametersJSON Schema
NameRequiredDescriptionDefault
paramsYes

Output Schema

ParametersJSON Schema
NameRequiredDescription
okYesFalse when the request could not be evaluated.
errorNoReadable, actionable message when ok is False.
holdsNoWhether the goal currently holds.
proofNoDerivation, present for `why` when the goal holds.
findingsNoObservations: missing predicates, unprovable goals.
conclusionNoHuman-readable summary of the diagnosis.

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare readOnlyHint=true and destructiveHint=false, and the description adds behavioral context by explaining the three modes, return format (DiagnosisResult), error handling (ok and error fields), and limitations like bounded assumptions. No contradictions with annotations.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured with a clear opening statement, followed by mode explanations and return field details. Every sentence serves a purpose, and the information is front-loaded. No redundant or fluff content.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's complexity (diagnosis with multiple modes, specific input language, and structured output), the description covers all necessary aspects: when to use, mode details, input format, and output fields (including error conditions). Output schema exists but the description explains the fields for clarity.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema includes descriptions for all parameters, so baseline is 3. The description adds value by elaborating on query syntax, knowledge base format, and mode behavior beyond the schema's brief descriptions. For example, it explains variables with $, conjunction with AND, and the max assumptions for what_needs mode.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool's purpose: 'Explain why a query holds, why it fails, or what would make it true.' It also distinguishes from siblings by explicitly referencing the 'reason' tool and advising to use when 'reason returns something you did not expect.'

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly says 'Reach for this when reason returns something you did not expect,' providing clear context for when to use. It also details three modes with specific use cases. However, it does not explicitly mention when not to use it or compare with other siblings like what_if or check_kb.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

reasonA
Read-onlyIdempotent

Prove a goal against a knowledge base and return every solution with its proof.

Use this for any question that needs multi-step deduction over facts and rules: transitive relations, permission inheritance, property inheritance, eligibility checks, or filtering a large fact set by a rule.

The goal comes from the query parameter, or from the ? ... line(s) in knowledge when query is omitted.

Returns ReasonResult:

  • ok (bool): false when the request could not be evaluated.

  • solutions (list): each has bindings (list of {var, value}, empty for a ground yes/no query), proof (a tree of {goal, type, children} where type is fact, rule or and), and proof_text (the tree rendered as indented text).

  • solution_count (int): how many solutions are returned.

  • truncated (bool): true when more solutions existed than max_solutions.

  • error (str | null): a readable, actionable message when ok is false.

An empty solutions list with ok: true means the goal is false under closed-world semantics - the knowledge base does not entail it.

ParametersJSON Schema
NameRequiredDescriptionDefault
paramsYes

Output Schema

ParametersJSON Schema
NameRequiredDescription
okYesFalse when the request could not be evaluated.
errorNoReadable, actionable message when ok is False.
solutionsNo
truncatedNoTrue when more solutions existed than `max_solutions`.
solution_countNoNumber of solutions returned.

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

The description discloses detailed behavioral traits beyond the annotations (readOnlyHint, idempotentHint, etc.): it explains the return structure (ReasonResult with ok, solutions, proof, etc.), closed-world semantics (empty solutions with ok:true means false), query source (from parameter or knowledge lines), and truncation behavior. No contradiction with annotations.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured: a one-sentence core purpose, followed by usage scenarios, parameter interaction note, and a thorough yet concise breakdown of the return type. Every sentence is substantive, with no redundancy. The most critical information is front-loaded.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's complexity (deduction with proofs) and the presence of a detailed output schema, the description provides sufficient context: it explains the return fields, error handling, truncated results, and the meaning of empty solutions. It does not repeat schema content but adds essential usage context. Output schema exists, so return value details are adequately covered.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema already has detailed descriptions for each parameter. The description adds value by explaining the relationship between query and knowledge parameters ('The goal comes from the query parameter, or from the ? ... line(s) in knowledge when query is omitted'), which is not present in the schema descriptions. This enriches parameter understanding.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states 'Prove a goal against a knowledge base and return every solution with its proof,' providing a specific verb+resource. It further lists example use cases (transitive relations, permission inheritance, etc.) and implicitly distinguishes from siblings like 'diagnose' and 'what_if' by emphasizing multi-step deduction.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly states 'Use this for any question that needs multi-step deduction over facts and rules,' giving clear positive guidance. However, it does not explicitly state when not to use it (e.g., 'do not use for simple fact lookups'), which would strengthen differentiation from siblings like 'check_kb'.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

what_ifA
Read-onlyIdempotent

Apply hypothetical fact changes and compare the query before and after.

Use this to test a change without committing to it: promoting a user to a role, adding a resource, revoking an assignment. modifications is one change per line, + fact(...) to add or - fact(...) to remove. Only facts can be changed, not rules. A - line that matches no existing fact is an error, so a typo cannot silently produce a misleading comparison.

Returns WhatIfResult:

  • ok (bool): false when the request could not be evaluated.

  • before_count, after_count (int): solution counts on each knowledge base.

  • delta (int): after_count - before_count.

  • solutions_before, solutions_after (list): full solutions with proofs.

  • applied (list of str): the modifications as applied, normalized.

  • conclusion (str): a readable description of the impact.

  • error (str | null): a readable message when ok is false.

ParametersJSON Schema
NameRequiredDescriptionDefault
paramsYes

Output Schema

ParametersJSON Schema
NameRequiredDescription
okYesFalse when the request could not be evaluated.
deltaNoafter_count - before_count.
errorNoReadable, actionable message when ok is False.
appliedNoModifications that were applied, normalized.
conclusionNoHuman-readable description of the impact.
after_countNoSolutions on the modified knowledge base.
before_countNoSolutions on the base knowledge base.
solutions_afterNo
solutions_beforeNo

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

The description reveals detailed behavior beyond annotations: it returns a `WhatIfResult` with fields like `ok`, `before_count`, `after_count`, `delta`, `solutions_before`, `solutions_after`, `applied`, `conclusion`, and `error`. It confirms the tool is read-only (readOnlyHint=true), idempotent, and non-destructive, and adds that only facts can be mutated.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is moderately long but well-organized. It begins with the core purpose, then usage instructions, modification format, and finally a full list of return fields. Each section adds value without redundancy. Minor improvement: the return fields could be more compact, but overall it is efficient.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The description is complete for a complex tool with 5 parameters (all with 0% schema coverage) and an output schema. It covers input syntax, error conditions, and all return fields. There are no gaps; the agent can use this tool correctly based solely on the description.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters5/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Although the input schema has 0% description coverage, the description compensates fully. It explains the `modifications` syntax (`+ fact(...)` / `- fact(...)`), the `query` format (Euclid-IR body syntax), and the `base_knowledge` format (text or YAML with facts, rules, queries). It also notes that variables start with `$`, `_` is a wildcard, and `NOT` is closed-world negation.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description opens with a clear action: 'Apply hypothetical fact changes and compare the query before and after.' It explains the tool's value (test without committing) and gives concrete examples (promoting a user, adding a resource, revoking an assignment). The purpose is distinct from sibling tools like 'reason' and 'diagnose' which focus on non-hypothetical reasoning.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly states when to use the tool ('test a change without committing to it') and provides examples. It also clarifies limitations ('Only facts can be changed, not rules') and warns about errors ('A `-` line that matches no existing fact is an error'). Although alternatives are not named, the usage context is clear and well-documented.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections. Dates show when Glama detected each change.

  1. 4 tool updatesv0.1.0
    • First observedcheck_kb
    • First observeddiagnose
    • First observedreason
    • First observedwhat_if
Install Server
RayrunBuild, deploy, and operate MCP servers without becoming an infrastructure team.ray.runAd

TDQS

A4.6/5.0
Disambiguation5/5

Each tool has a clearly distinct purpose: reason for proving, diagnose for understanding unexpected results, what_if for hypothetical changes, and check_kb for static validation. There is no overlap; an agent can easily select the appropriate tool.

Naming Consistency5/5

All tool names use snake_case with imperative verbs or common phrases: reason, diagnose, what_if, check_kb. The naming pattern is consistent and predictable, making it easy for an agent to infer functionality.

Tool Count5/5

With only 4 tools, the server is tightly scoped to logical reasoning tasks. Each tool serves a critical function without redundancy, and the count is well-suited for its domain.

Completeness4/5

The tool surface covers reasoning, diagnostics, hypotheticals, and validation. Minor gaps exist, such as no direct tool to list all facts/rules or permanently modify the knowledge base, but the core workflow is well-supported.

Maintenance

ActivitySlowing
ResponsivenessSyncing

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

Related MCP Servers

  • MCP-Logic

    angrysky56
    A
    license
    Not graded
    quality
    B
    maintenance
    MCP-Logic is a server that provides AI systems with automated reasoning capabilities, enabling logical theorem proving and model verification using Prover9/Mace4 through a clean MCP interface.
    46
    MIT

  • Pyke MCP Server

    NewJerseyStyle
    A
    license
    Not graded
    quality
    C
    maintenance
    An MCP server for the Pyke logic programming engine that enables LLMs to perform logical reasoning using knowledge bases with facts, rules, and queries. It supports session management, forward chaining inference, and bulk loading of programs in Logic-LLM format.
    MIT

  • Chiasmus

    yogthos
    A
    license
    Not graded
    quality
    B
    maintenance
    MCP server that gives LLMs access to formal verification via Z3 and SWI-Prolog, plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results with mathematical certainty, and analyzes call graphs for reachability, dead code, and impact analysis.
    79
    210
    Apache 2.0

  • Atom of Thoughts

    dioptx
    A
    license
    A
    quality
    D
    maintenance
    Structured reasoning MCP server that decomposes problems into atomic steps (premise, reasoning, hypothesis, verification, conclusion) with confidence scoring, live visualization, and approval feedback.
    3
    87
    MIT

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/snegi26/euclidMCPPaper'

If you have feedback or need assistance with the MCP directory API, please join our Discord server