Skip to content

Euclid-MCP: A Model Context Protocol Server for Deterministic Logical Reasoning via Prolog

Jul 2026 · arXiv.org · Vol abs/2607.21412 · 1 citation · 24 references
Computer Science

TL;DR

It is argued that semantic RAG is fundamentally unsuited for rule enforcement, and that Euclid-MCP can serve as a stable, shared reasoning substrate for both RAG-based assistants and agentic systems.

Abstract

Large Language Models (LLMs) excel at natural language understanding and generation but remain unreliable for multi-step logical reasoning, especially in safety-critical or compliance-sensitive domains. Recent neuro-symbolic approaches address this gap by coupling neural models with external symbolic engines, yet most integrations are bespoke and lack a standardized interface for tool-augmented agents. This paper presents Euclid-MCP, an open-source MCP server that provides deterministic logical reasoning via SWI-Prolog. Euclid-MCP introduces Euclid-IR, an engine-agnostic intermediate representation for Horn-clause logic that is human-readable, easy for LLMs to generate, and straightforward to compile into Prolog or alternative backends. The server exposes a compact tool interface that supports a translate-run-inspect-repair loop, enabling LLM clients to delegate inference while retaining full access to proof traces and derivation logs. We evaluate Euclid-MCP on a realistic IT security and compliance use case. Results show that while LLMs alone are sufficient on small knowledge bases, they hallucinate systematically on larger problems, whereas Euclid-MCP delivers exact answers with lower latency and more compact outputs. We argue that semantic RAG is fundamentally unsuited for rule enforcement, and that Euclid-MCP can serve as a stable, shared reasoning substrate for both RAG-based assistants and agentic systems.

View source

Similar papers

Jul 2026

FAVA: Formal Authorization for Verified Agents with Evidence-Backed Permission Graphs

This work presents FAVA (Formal Authorization for Verified Agents), a permission-carrying authorization framework for agent execution that utilizes an LLM-guided Permission Intermediate Representation to translate ambiguous natural-language tasks into structured constraints.

Yifan Zhang, Xinkui Zhao, Sai-Da Liu et al. · 3 citations
Jul 2026

AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

AoA lifts the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree.

Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang et al. · 0 citations
Open access Jul 2026

Symbolic Logic Validation of LLM Interactions in Critical Systems

This paper proposes a validation framework that combines the flexibility of LLMs with the logic reasoning capabilities of Answer Set Programming as a complementary layer to existing guardrail mechanisms and demonstrates the practical implementation through a modular architecture that supports customizable validation components.

András Gergely Deé-Lukács, Bal'azs 'Ad'am Toldi, András Földvári · 0 citations
Preprint Aug 2026

ACTS-SQL: Agentic and Critic-Oriented Tree-Structured SQL Correctness with Large Language Models

This work presents a training-free framework that formulates SQL correction as a plan-guided, tree-structured debugging process that mitigates error accumulation during iterative refinement and demonstrates the effectiveness and stability of the approach in real-world deployments.

Xinmei Huang, Jie Song, Peng Li et al. · 0 citations
#artificial intelligence Preprint Sep 2026

Harness Engineering in LLM Tool Use via Agent-Native Reusable Tool Primitives

Large language models (LLMs) augmented with external tools have demonstrated remarkable capability in solving complex real-world tasks. However, existing approaches suffer from two key challenges: brittle multi-step and multi-turn reasoning caused by incompatible tool output types and API schemas, and performance degradation under large tool catalogues. To address these, we introduce \textbf{Tool Primitives}, a design that replaces rigid API schema-based invocation with natural language as the interface for tool calling, where each tool is wrapped with an LLM interface that handles schema resolution and execution internally, enabling natural inter-tool communication for nested and multi-turn tool calling. Building on Tool Primitives, we host \textbf{ToolFace}, a centralized repository of 25,519 functions from which LLMs dynamically retrieve only the relevant tools at inference time, eliminating the need to enumerate raw API schemas in context. To orchestrate Tool Primitives and ToolFace reliably in complex settings, we further propose \textbf{HEART}, a \textbf{H}arness \textbf{E}ngineering framework via \textbf{A}gent-native, \textbf{R}eusable \textbf{T}ool Primitives, comprising a Planner, Router, and Verifier that jointly support dynamic tool invocation planning, multi-step execution, and feedback-driven recovery. Experiments on five benchmarks demonstrate that HEART outperforms SFT-based models by $10\%$ on average and surpasses GPT-5.4, Claude-4.6-Sonnet, and Gemini-3.1-Pro by $6\%$ on average while reducing API cost by up to $85\%$. On 50 real-world tasks, HEART achieves $84\%$ task completion, $3.8\times$ the average of three frontier commercial models ($22\%$).

Haibo Jin, Sui-Jin Wang, Xuchen Yu et al. · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.