Euclid-MCP: Instructions file for Codex

Euclid-MCP — Agent Guide

Deterministic logical reasoning engine. Write facts/rules in Euclid IR, engine translates to Prolog, returns solutions with proof trees.

Tools: euclid-mcp_reason, euclid-mcp_explain, euclid-mcp_diagnose, euclid-mcp_what_if, euclid-mcp_check_kb, euclid-mcp_register_kb, euclid-mcp_unregister_kb, euclid-mcp_list_kbs

Workflow

1. check_kb    → validate before reasoning (catch syntax errors, undefined predicates)
2. reason      → run deduction, get solutions + proof trees
3. explain     → turn solutions into readable, auditable reasoning steps
4. diagnose    → if result unexpected: mode="why_not" to find missing facts/rules
5. what_if     → test modifications before applying them

Always call check_kb first on new or modified knowledge bases.

knowledge/base_knowledge are optional on all reasoning tools: an empty value falls back to kb_id (if given) and then to the preloaded KB (EUCLID_KB_PATH / --kb-path). For repeated sessions, register_kb once and pass kb_id (+ an optional delta_knowledge overlay for session facts) instead of resending the KB text.

Tools

reason

Main deduction. Returns solutions with variable bindings and proof trees.

Parameter	Type	Default	Description
knowledge	string?	—	Facts & rules (falls back to kb_id, then preloaded KB)
kb_id	string?	—	Reference a KB registered via register_kb
delta_knowledge	string?	—	Session facts appended to the kb_id base
query	string?	—	Override query (optional)
max_solutions	int	5	Max solutions
max_depth	int	30	Max proof tree depth

explain

Deterministic proof-tree → natural-language reasoning steps. Cites rule_id when a rule has one. Each explanation also carries structured_steps: typed, language-independent steps (kind/goal/rule_id/body) from which the English steps are derived — use them for localized rendering.