PrologMCP: A Standardized Prolog Tool Interface for LLM Agents

# PrologMCP: A Standardized Prolog Tool Interface for LLM Agents
Source: [https://arxiv.org/html/2606.14935](https://arxiv.org/html/2606.14935)
\\copyrightclause

Copyright for this paper by its authors\. Use permitted under Creative Commons License Attribution 4\.0 International \(CC BY 4\.0\)\.

\\conference

Joint Workshop on Statistics and Knowledge Integration for Logic, Learning, Ethical Decisions, and LLMs, 18 July 2026, Lisbon

\[email=agnieszka\.mensfelt@rhul\.ac\.uk, \] \[email=adarsh\.prabhakaran@rhul\.ac\.uk, \] \[email=adrian\.haret@rhul\.ac\.uk, \] \[email=vince\.trencsenyi@rhul\.ac\.uk, \] \[email=kostas\.stathis@rhul\.ac\.uk, \]

Adarsh PrabhakaranAdrian HaretVince TrencsenyiKostas StathisDepartment of Computer Science, Royal Holloway, University of London, UK

\(2026\)

###### Abstract

Frontier reasoning\-tuned language models still fail on deductive tasks at depth, and the cost of improved performance through extended internal reasoning scales poorly\. Symbolic delegation offers a complementary route: a language model translates the problem, while a solver performs the inference\. However, current autoformalization pipelines for logic programming are typically bespoke integrations tied to particular tasks or agents\. We introducePrologMCP, a task\-agnostic, open\-source server that exposes Prolog as a stateful tool through the Model Context Protocol \(MCP\)\. Its compact tool interface, structured error reporting, and per\-session isolation make the*translate–run–inspect–repair*loop a reusable primitive for MCP\-capable agents\. We evaluate a formalizer agent enhanced withPrologMCPagainst standard and reasoning LLMs \(Claude Sonnet 4\.6, GPT\-4\.1, and o4\-mini\) on two subsets ofPARARULE\-Plus: a general\-purpose sample and a more challenging one targeting a specific failure mode of natural\-language reasoning\. On the general sample, the formalizer matches or exceeds reasoning LLMs \(accuracy 1\.00 vs\. 1\.00 / 0\.998\), with the largest gains over standard models \(0\.762 for GPT\-4\.1\)\. On the challenging subset, the formalizer remains near\-perfect \(1\.00 / 0\.99\) while reasoning LLMs drop to 0\.95 / 0\.94\. These results suggest that delegating inference to Prolog via MCP is a robust and inspectable alternative to extended natural\-language reasoning\.

###### keywords:

Prolog\\sepModel Context Protocol\\sepAutoformalization\\sepLarge Language Models\\sepSymbolic Reasoning

## 1Introduction

Since the dawn of artificial intelligence, reasoning has been considered a constitutive component of intelligent behaviour\[mccarthy1959,kowalski1974,newell1976\]\. Large language models, after initially underperforming on reasoning benchmarks, have made rapid progress; however, important limitations remain\.

First, accuracy degrades on long deductive chains, even for strong reasoning\-tuned models\. Unlike a symbolic solver, for which multi\-step rule application preserves correctness by construction, a language model has no mechanism ensuring that each generated step is a valid logical consequence of the previous one\. This lack of stepwise guarantees makes long chains fragile: errors can accumulate, and successful reasoning depends on maintaining a coherent derivation\. Lin et al\.\[lin2025zebralogic\]demonstrate this collapse on grid\-style logic puzzles, where frontier reasoning models suffer significant accuracy drops as problem complexity increases\. Kazemi et al\.\[kazemi2025bbeh\]likewise report that frontier reasoning models remain far from saturation on a hard reasoning benchmark\. Earlier analyses of compositional tasks\[dziri2023faith\]and template\-based variants of standard mathematics benchmarks\[mirzadeh2025gsm\]attribute such failures to pattern matching over training\-distribution structure rather than genuine multi\-step deduction, with accuracy degrading as the number of required reasoning steps grows\.

Second, the cost of additional reliability scales poorly\. Current reasoning\-tuned models attempt to improve reliability by allocating more internal reasoning, orthinking, tokens\. However, this increases inference cost while providing no guarantee that the additional tokens correspond to valid deductive steps\. On tasks whose rules are simple but whose search space is combinatorially branching, additional generation can therefore yield diminishing returns\. Recent work characterising these limits\[shojaee2025illusion,lin2025zebralogic\]finds that increasing the thinking budget yields diminishing returns beyond a problem\-complexity threshold, with reasoning models in some cases even reducing their thinking\-token usage as problems become harder\. By contrast, symbolic solvers—Prolog for rule\-based deduction, SAT and CSP solvers for combinatorial search—routinely handle problems many orders of magnitude beyond the thresholds at which reasoning\-tuned models collapse\.

These solvers offer two properties that natural\-language reasoning lacks: predictable compute scaling and answers that are correct by construction\. This motivates an established alternative—the tool\-use paradigm\[schick2023toolformer,gao2023pal\]—in which, rather than perform every reasoning step internally, a model delegates well\-specified tasks to external tools\. For instance, arithmetic and general computation can be handled by code interpreters; factual lookup by retrieval systems; and reasoning problems by symbolic solvers\. This latter direction is closely related to*autoformalization*\[wu\_autoformalization\_2022,mensfelt2026towards\], which has explored several classes of formal systems and solvers\. Logic programming is an especially natural fit for many deductive\-reasoning tasks, since it combines declarative representation with automated inference\. Yet, compared with code execution and retrieval, logic programming remains comparatively under\-served as a standardized tool for language\-model agents\.

A growing line of work has explored combinations of LLMs and Prolog\.\[borazjanizadeh2024reliable\]use an off\-the\-shelf LLM to generate Prolog programs and re\-try on execution failure;\[mensfelt2024generative\]autoformalize game\-theoretic scenarios into executable Prolog with an iterative solver\-feedback correction loop—a close precedent for thetranslate–run–inspect–repairpattern we propose here\.\[yang2024arithmetic\]fine\-tune LLMs to generate Prolog for arithmetic word problems, while\[tan2024thought\]use a Prolog engine to produce verified reasoning trajectories that an LLM imitates as structured chain\-of\-thought\. Closely related,\[mellgren2025training\]fine\-tune a small model with GRPO to use Prolog as a callable tool with internal repair, motivating the primitive thatPrologMCPexposes as a standardized interface\. Other recent work\[zunjare2026neuroprolog,he2025protoreasoning\]incorporates structured Prolog representations during training\.

However, existing systems are largely bespoke: each defines its own interface, execution model, and error\-handling strategy, limiting portability across models and agent frameworks\. In particular, no standardized interface currently lets agents discover, invoke, inspect, and repair Prolog programs in a uniform way\. This paper presentsPrologMCP, a Model Context Protocol \(MCP\) server that exposes Prolog as a stateful tool to any MCP\-capable language\-model agent\. It supports a reusable*translate–run–inspect–repair*loop: the agent translates a natural\-language problem into Prolog, executes queries against a symbolic solver, inspects structured outputs or errors, and revises the formalization when necessary\. Our contributions are:

1. I\.A standardized Prolog tool interface, implemented as an MCP server, supporting structured interaction, error reporting, and session\-level isolation \(Section[3](https://arxiv.org/html/2606.14935#S3)\)\.
2. II\.A formalizing LLM agent, translating natural\-language problems into Prolog, executing queries using the server, and iteratively refining its representations using structured feedback \(Section[4](https://arxiv.org/html/2606.14935#S4)\)\.
3. III\.An empirical evaluation of the formalizer agentonPARARULE\-Plus\[bao2022multi\], comparing it against standard LLM and reasoning\-model inference \(Section[4](https://arxiv.org/html/2606.14935#S4)\)\.

## 2Background

#### Logic Programs in Prolog\.

Logic programs, most prominently implemented in Prolog\[korner2022fifty,wielemaker2012swi\], provide a declarative representation based on Horn clauses: universally quantified implications of the form “ifb1b\_\{1\}, …,bnb\_\{n\}, thenhh”, which map naturally onto facts \(clauses with no body\), rules \(clauses with one or more body literals\), and queries \(goals to be proved\)\. Reasoning combinesunificationof terms,SLD\-resolution\[kowalski1971linear\]to reduce a query to subgoals against matching clause heads, and goal\-directed search with backtracking\. Prolog extends SLD with SLDNF, i\.e\., negation\-as\-failure\[clark1978negation\], whereby a negated goal is treated as satisfied when the system cannot prove the corresponding positive goal\.

Horn clauses align closely with the surface form of natural\-language rules \(“if X is kind then X is nice” becomesnice\(X\) :\- kind\(X\)\.\), and Prolog’s goal\-directed inference, support for negation\-as\-failure, and persistent clause state across calls make it a natural target for autoformalization in deductive\-reasoning tasks\. Competing approaches such as SAT, SMT, or CP require translation into satisfiability formulas, background theories, or explicit variable domains, and SAT and CP solvers are typically stateless per invocation, which fits multi\-turn agent reasoning over a growing knowledge base less well\.

#### Model Context Protocol\.

The Model Context Protocol\[anthropic2024mcp,Hou2026e\]provides a standard interface for exposing tools to LLM agents, with conventions for tool discovery, typed argument schemas, and structured error reporting\. A tool exposed via MCP can be used by any MCP\-aware agent without model\-specific glue code\. MCP also accommodates stateful tools such as Prolog: across a sequence of calls, an agent can assert clauses, inspect program state, issue queries, receive structured diagnosticss, and refine the formalization\. The closest precedent is the MCP\-Solver discussed in\[szeider2025bridging\], which exposes constraint, SAT, SMT and answer sets backends \(MiniZinc, PySAT, Z3 and clingo\) but not Prolog\-style SLDNF resolution with unification and backtracking over a database of clauses\.

#### Autoformalization\.

*Autoformalization*is the automatic translation of an informal\-language expression into a semantically corresponding expression in a formal language\. The term originates in formal mathematics\[wu\_autoformalization\_2022\], and has since broadened to cover pipelines in which a model emits a formal artefact—a logic program, constraint model, SMT formula, or planning specification—passed to a sound external reasoning procedure\. A recent unifying account\[mensfelt2026towards\]parameterises autoformalization by an informal languageLiL\_\{i\}and a formalizable subset thereof, a formal reasoning languageLfL\_\{f\}with precise semantics, and a semantic equivalence criterionEEspecifying which aspects of meaning must be preserved\. BecauseEEis itself informal and not directly checkable, practical pipelines introduce a computable*validation criterion*VVthat approximatesEE, for example by executing the formal artefact with a solver and comparing its output against an expected result\.

![Refer to caption](https://arxiv.org/html/2606.14935v1/x1.png)Figure 1:PrologMCP architecture\.

## 3Architecture

PrologMCPis an MCP server that exposes Prolog to LLM agents as a stateful tool\. Three properties drive the design: \(ii\)*statefulness*—clauses persist across calls, so the agent builds a knowledge base incrementally instead of resubmitting it on every goal; \(i​iii\)*structured error reporting*—compile\- and runtime diagnostics are returned as typed JSON; \(i​i​iiii\)*isolation*—each session runs in a dedicated interpreter subprocess with bounded resources\. Currently, the server supports only SWI\-Prolog\. Tool signatures and JSON schemas are given in Appendix[B](https://arxiv.org/html/2606.14935#A2)\. The source code is available on GitHub \([https://github\.com/dicelab\-rhul/PrologMCP](https://github.com/dicelab-rhul/PrologMCP)\)\.

### 3\.1Components

The system has three tiers \(Figure[1](https://arxiv.org/html/2606.14935#S2.F1)\), forming a single path from an agent’s tool call down to a Prolog subprocess and back:

1. 1\.A Python MCP serverthat presents the tool interface of Section[3\.3](https://arxiv.org/html/2606.14935#S3.SS3)to the agent: it declares each tool’s input schema, validates and dispatches incoming calls to the appropriate session, and maps harness outcomes—including failures—onto MCP’s structured tool\-result format\. The server holds no Prolog state of its own; it is a thin protocol adapter over the session registry\.
2. 2\.A session registrythat owns a pool of Prolog sessions, indexed by aload\_idreturned on session creation\. The registry is thread\-safe, caps concurrent sessions at a configurable limit, evicts LRU \(least\-recently\-used\) sessions on overflow, and reaps sessions idle beyond a TTL \(time\-to\-live\) from a background thread\.
3. 3\.A Prolog harness\(harness\.pl\), loaded into each session’sswiplsubprocess, that reads newline\-delimited JSON commands onstdin, dispatches them to handlers, and writes newline\-delimited JSON responses onstdout\. Stderr is reserved for uncaptured diagnostics\.

### 3\.2Session Semantics

A session is created byconsult\_text\(source, dialect\): the registry allocates a freshload\_id, spawns aswiplsubprocess with the harness, writessourceto a file in the session’s temporary directory, and issues aconsultcommand\. Ifsourcelacks a module declaration, the registry prepends:\- module\(m\_⟨load\_id⟩, \[\]\)\.so that subsequently defined predicates live in a per\-session module disjoint from the harness and from other sessions\. Module\-qualified goal evaluation \(Module:Goal\) is used throughout, so predicate resolution is unambiguous regardless of the module in whichsourcewas written\.

Syntax errors, singleton warnings, and similar diagnostics are captured by amessage\_hook/3installed in the harness, so a consult that raises errors still loads the clauses it can rather than aborting\. Captured diagnostics are returned as amessagesarray, each entry carrying a severity, a kind drawn from a fixed vocabulary, a message string, and, when the diagnostic is attributable to a specific clause, the source line that triggered it\. Because the successfully loaded predicates remain callable after a failed consult, the agent can repair the source withreplace\_predicate; consultation is thus*non\-fatal*\.

The subprocess is held open for the session’s lifetime; sessions close explicitly viaclose\_session, implicitly on TTL expiry, or by LRU eviction under load\.

### 3\.3Tool Interface

ToolBehaviourconsult\_textOpen a session from a source string, returning itsload\_id, an optional inventory of defined predicates, and any diagnostics raised during consultation\.run\_goalEvaluate a goal string withfindnsols/4wrapped incall\_with\_depth\_limit/3, reporting typed bindings, the number of solutions, and whether the depth bound was hit\.inspect\_predicateReport a predicate’s clauses, arity, type \(static \| dynamic \| foreign\), export status, and clause count; if no exact match exists, suggest predicates with similar names\.get\_sourceRebuild the module’s source by traversingpredicate\_property/2andclause/2\.replace\_predicateRetract a predicate withabolish/1, then reload a single\-predicate patch into the session module viaload\_files/2\.list\_messagesRetrieve the diagnostics gathered over the current session\.run\_testsConsult an optionalplunitfile and execute every registered unit, returning pass, fail, and blocked tallies alongside per\-test results\.trace\_goalRun a depth\-bounded meta\-interpreter over a goal, yielding a proof tree and its node count\.close\_sessionTear down the subprocess and remove its temporary directory\.Table 1:Tools exposed over MCP\. All arguments and return values are JSON; every error is reported as\{ok: false, error: \{kind, message, prolog\_term\}\}without terminating the session\.The server exposes eight operational tools plus one administrative tool \(Table[1](https://arxiv.org/html/2606.14935#S3.T1)\)\. Each tool corresponds to one primitive the harness supports directly, and the Python layer does no orchestration of its own beyond dispatch and error mapping\.

We bound goal evaluation in two ways: by the number of solutions returned per call and by inference depth\. A goal that exhausts the depth limit returns withdepth\_exceeded: trueand any solutions found so far, rather than raising an exception\. Both bounds are surfaced in the response, so the agent can retry with a larger limit when a partial result is inconclusive\. A goal that exhausts the depth limit returns withdepth\_exceeded: trueand any solutions found so far, rather than an exception\. These bounds are surfaced in the response so that the agent can retry with a larger limit if the partial result is inconclusive\.

## 4Evaluation

### 4\.1Agent implementation

![Refer to caption](https://arxiv.org/html/2606.14935v1/x2.png)Figure 2:Architecture of the Prolog\-augmented Formalizer agent\.We evaluate three agents that differ in how they produce a final answer: aStandardbaseline, aReasoningbaseline, and a Prolog\-augmentedFormalizer\. All agents receive the same natural\-language context and yes/no question\.Standardis a single\-call baseline\. The model receives the context and question, prefaced by a system prompt that frames the task as logical reasoning under thePARARULE\-Plusnegation semantics\. It is instructed to answer with exactly one word,trueorfalse, without elicited intermediate reasoning\.Reasoninguses the same task formulation as the Standard baseline, but runs it through each provider’s reasoning\-augmented inference path\. For Anthropic models, this corresponds to Extended Thinking mode; for OpenAI models, we use a dedicated reasoning model in place of the standard GPT model\.

Formalizerdelegates inference toPrologMCP\. Given the natural\-language context and question, the model generates a Prolog program together with a query goal\. The agent loads the generated program through the MCPconsult\_texttool, executes the query throughrun\_goal, and interprets the result \(Figure[2](https://arxiv.org/html/2606.14935#S4.F2)\)\. To make this interaction robust, the model is instructed to emit the program and goal inside<prolog\>…</prolog\>and<goal\_true\>…</goal\_true\>tags\. A parser extracts these fields; missing or malformed fields are treated as format errors\. If parsing fails, if the Prolog program cannot be loaded, or if execution reports an error, the agent returns the structured error message to the model and retries, up tomax\_attemptsattempts\.

The source code for the evaluation framework and experimental logs are available on GitHub \([https://github\.com/dicelab\-rhul/MCPFormalizer\)](https://github.com/dicelab-rhul/MCPFormalizer))\. The prompts used in the evaluation are provided in Appendix[C](https://arxiv.org/html/2606.14935#A3): the Formalizer prompt appears in Appendix[C\.1](https://arxiv.org/html/2606.14935#A3.SS1), and the Standard prompt appears in Appendix[C\.2](https://arxiv.org/html/2606.14935#A3.SS2)\.

### 4\.2Dataset

ThePARARULE\-Plusdataset\[bao2022multi\]is a large\-scale synthetic dataset for multi\-step deductive reasoning over natural language, extending the original PARARULE\[Clark2020p\]with deeper inference chains\. Each instance is a set of natural\-language facts and rules plus a Boolean query \(examples in Appendix[A](https://arxiv.org/html/2606.14935#A1)\)\.PARARULE\-Pluscovers reasoning depths 2–5 with≈\\approx100 000100\\,000samples each, generated over simple people\- and animal\-attribute domains\.

The dataset uses a specific, non\-standard interpretation of negation\. A body\-level\\\+ P\(x\)succeeds iffP\(x\)is not in the*initial*fact base, regardless of whether it is derivable by rules—resembling negation in semi\-positive Datalog\[abiteboul1995foundations\], where negation is restricted to the extensional database\. Queries, by contrast, use the standard closed\-world reading over both extensional and intensional facts: a negated query\\\+ P\(x\)is true iffP\(x\)is neither stated nor derivable\. Both standard SLDNF and stratified negation\[AptBlairWalker1988\]would instead apply the closure uniformly at both levels\. This non\-standard reading is required to reproduce the ground\-truth labels and is passed on to the LLMs in the prompts \(Appendix[C](https://arxiv.org/html/2606.14935#A3)\)\. This reading is passed to the LLMs by instructing the formalizer agent to record each base fact additionally asinitially\(pred, entity\)and to render every body\-level negation as\\\+ initially\(pred, X\)\(keepinginitially/2out of the goal\), and by telling the standard and reasoning LLMs to check body\-level negations against initial facts only but negated questions against the full closure\.

### 4\.3Experimental setup

SystemModelReasoning budgetStandardsonnet\-4\-6—Reasoningsonnet\-4\-610,000 tokensFormalizersonnet\-4\-6—Standardgpt\-4\.1—Reasoningo4\-minimedium effortFormalizergpt\-4\.1—\(a\)Per\-system model and reasoning\-budget settings\.
ParameterValueRandom seed42Max formalization attempts5Max tokens \(Standard, Formalizer\)4,096Max tokens \(Reasoning\)11,024Temperature \(Standard, Formalizer\)0Temperature \(Reasoning\)n/a\(b\)Global parameters held constant across all conditions\.

Table 2:Experimental configuration\.We evaluate each agent on two frontier models, Anthropic’s Claude Sonnet 4\.6 and OpenAI’s GPT\-4\.1, with the Reasoning condition substituting o4\-mini in place of GPT\-4\.1 on the OpenAI side\. Per\-system parameters are summarised in Table[2\(a\)](https://arxiv.org/html/2606.14935#S4.T2.st1)and global parameters in Table[2\(b\)](https://arxiv.org/html/2606.14935#S4.T2.st2)\. Temperature is fixed at zero for the Standard and Formalizer conditions to make outputs deterministic, but cannot be set uniformly across the evaluation: Anthropic’s Extended Thinking and OpenAI’s o4\-mini both disable temperature control by API constraint, exposing only their respective reasoning\-budget parameters in its place\. The two Reasoning conditions are therefore compared at the qualitative setting recommended by each provider, namely a10 00010\\,000\-token thinking budget for Extended Thinking and medium reasoning effort for o4\-mini\.

The MCP server was started fresh per process via theprolog\-mcpCLI entry point, and each instance received its own isolated Prolog session, created byconsult\_textand closed on completion\. Accuracy is reported as the fraction of instances where the predicted answer matches the ground\-truth label, with instances returningerrororunknowncounted as incorrect; no instances returnederrorin any run\.

We evaluatePrologMCPalong two complementary axes\. Section[5\.1](https://arxiv.org/html/2606.14935#S5.SS1)reports results on a depth\-stratified sample ofPARARULE\-Plus, reflecting the natural distribution of the benchmark across reasoning depths and rule types\. Section[5\.2](https://arxiv.org/html/2606.14935#S5.SS2)then reports results on a targeted subset that isolates instances where the dataset’s negation semantics provably diverges from standard SLDNF evaluation\. Together, these evaluations test both the average\-case reliability of symbolic delegation and its robustness under adversarial semantic conditions\.

## 5Results

### 5\.1Depth\-stratified evaluation

#### Dataset

We sampled 400 instances fromPARARULE\-Plus, stratified by reasoning depth, rule type, and domain\. AlthoughPARARULE\-Plusdiffers from SLDNF in its treatment of negation, the sampled subset contains substantial overlap between the two semantics because many body\-level negations occur in cases where the distinction is not observable\. In 45% of negated predicates, the negated predicate appears only as a base fact and is never derived by any rule\. For such predicates, checking absence from the initial facts is equivalent to checking failure of proof, since no rule can derive the predicate\. In the remaining 55%, the negated predicate does have derivation rules, so the two semantics can in principle disagree\. However, for many specific entities, those rules do not derive the predicate being negated\. The proof\-theoretic difference is therefore present but not activated by the particular query and knowledge base\. Disagreement arises only when the negated predicate is both derivable by rules and actually derived for the entity under consideration; this occurs in 6 instances\. Non\-termination would also arise when proving the negated predicate requires exploring recursive rule cycles under SLDNF; this would occur in 15 instances\.

#### Main results\.

SystemAccuracyInputOutputTotalSec\.ClaudeStandard LLM0\.9886881608493\.57Reasoning1\.0007172409574\.64Formalizer \(Prolog\)1\.000100342314265\.11GPT/o4\-miniStandard LLM0\.76265326550\.98Reasoning0\.998652896154811\.27Formalizer \(Prolog\)1\.00088130811894\.23Table 3:Overall results onPARARULE\-Plus\(400 instances\)\.Table[3](https://arxiv.org/html/2606.14935#S5.T3)reports the main results for the three systems described in Section[4\.1](https://arxiv.org/html/2606.14935#S4.SS1): the Standard baseline, which answers without an explicit reasoning configuration; the Reasoning condition, which uses a reasoning\-enabled inference path or dedicated reasoning model; and the Formalizer, which translates the instance into Prolog and delegates inference to the MCP server\.

Overall, both reasoning\-augmented approaches improve accuracy over standard LLMs, with the effect most pronounced for the OpenAI models\. For Claude Sonnet 4\.6, the Standard baseline is already strong, achieving 0\.988 accuracy while using the fewest tokens and lowest runtime\. Both the Reasoning condition and the Formalizer reach perfect accuracy, but at higher computational cost\. One caveat is that, despite the prompt instruction to answer with a single word, Claude Sonnet 4\.6 in the Standard condition sometimes produces explanatory reasoning traces\. This increases its output\-token usage and makes the condition less sharply separated from the explicit reasoning setting\.

For the OpenAI models, GPT\-4\.1 follows the one\-word response instruction more closely in the Standard condition, but its accuracy is much lower, at 0\.762\. Replacing GPT\-4\.1 with the reasoning model o4\-mini raises accuracy to 0\.998, while the GPT\-4\.1 Formalizer reaches perfect accuracy\. The Formalizer is particularly effective in this setting: it achieves the best accuracy with lower total token usage and substantially lower runtime than the reasoning\-model condition\. These results suggest that symbolic delegation can provide a favourable reliability–cost trade\-off when the base model is less reliable, while direct natural\-language inference may remain more efficient when the base model is already highly accurate\.

#### Accuracy by depth\.

Systemd=2d=2d=3d=3d=4d=4d=5d=5ClaudeStandard LLM1\.0001\.0000\.9700\.980Reasoning1\.0001\.0001\.0001\.000Formalizer \(Prolog\)1\.0001\.0001\.0001\.000GPT/o4\-miniStandard LLM0\.7400\.7700\.7700\.770Reasoning1\.0001\.0001\.0000\.990Formalizer \(Prolog\)1\.0001\.0001\.0001\.000\(a\)Accuracy by reasoning depth\.
SystemNegationStandardClaudeStandard LLM0\.9751\.000Reasoning1\.0001\.000Formalizer \(Prolog\)1\.0001\.000GPT/o4\-miniStandard LLM0\.6700\.855Reasoning0\.9951\.000Formalizer \(Prolog\)1\.0001\.000\(b\)Accuracy by rule type \(n=200n=200per cell\)\.

Table 4:Per\-system accuracy broken down by reasoning depth and by rule type\.The depth\-wise results in Table[4\(a\)](https://arxiv.org/html/2606.14935#S5.T4.st1)show that standard models become less reliable as reasoning depth increases, whereas both reasoning\-augmented approaches remain robust\. For Claude Sonnet 4\.6, the Standard baseline is perfect at depths 2 and 3, but drops slightly at depths 4 and 5\. By contrast, both the Reasoning condition and the Prolog Formalizer achieve perfect accuracy at every depth\.

The effect is stronger for the OpenAI models\. GPT\-4\.1 standard prompting remains below 0\.80 at every depth, while o4\-mini Reasoning reaches perfect accuracy through depth 4 and drops only slightly at depth 5\. The GPT\-4\.1 Formalizer achieves perfect accuracy across all depths, suggesting that explicit symbolic formalization provides the most stable performance as reasoning complexity increases\.

One notable exception to a simple depth\-scaling pattern is GPT\-4\.1 in the Standard condition: its lowest accuracy occurs at depth 1 rather than at the deepest levels\. This suggests that the Standard model’s errors are not driven solely by reasoning\-chain length\. Instead, they may reflect reliance on shallow pattern matching, rather than systematic multi\-step deduction\.

#### Accuracy by rule type\.

![Refer to caption](https://arxiv.org/html/2606.14935v1/x3.png)\(a\)Claude
![Refer to caption](https://arxiv.org/html/2606.14935v1/x4.png)\(b\)GPT/o4\-mini

Figure 3:Standard\-mode accuracy by reasoning depth and rule type\.Table[4\(b\)](https://arxiv.org/html/2606.14935#S5.T4.st2)reports accuracy by rule type, and Figure[3](https://arxiv.org/html/2606.14935#S5.F3)reports accuracy by rule type across reasoning depths\. For Claude Sonnet 4\.6 in both the Standard and Reasoning conditions, and for o4\-mini in the Reasoning condition, all errors occur in instances that contain negation in the rules\. For Claude Sonnet 4\.6 in the Standard condition, these failures are concentrated at depths 4 and 5 \(Figure[3\(a\)](https://arxiv.org/html/2606.14935#S5.F3.sf1)\)\. This pattern suggests that the non\-standard negation semantics ofPARARULE\-Plusmay pose a challenge even for strong reasoning models, because it requires them to suppress more familiar interpretations of negation\.

GPT\-4\.1 in the Standard condition is the only setting in which errors also affect instances without rule\-level negation\. Figure[3\(b\)](https://arxiv.org/html/2606.14935#S5.F3.sf2)shows accuracy by depth for both rule types\. For GPT\-4\.1 Standard, accuracy on instances with negation increases with reasoning depth, while accuracy on instances without negation decreases\. This non\-monotonic pattern is consistent with the hypothesis that GPT\-4\.1 Standard relies partly on shallow regularities in the input distribution, rather than performing systematic deductive reasoning\.

#### Token usage by depth\.

![Refer to caption](https://arxiv.org/html/2606.14935v1/x5.png)\(a\)Claude
![Refer to caption](https://arxiv.org/html/2606.14935v1/x6.png)\(b\)GPT/o4\-mini

Figure 4:Token usage by reasoning depth for Claude and GPT models\.Figure[4](https://arxiv.org/html/2606.14935#S5.F4)shows token usage by reasoning depth\. Token consumption increases with depth for all systems, but the magnitude of this growth differs substantially\. For Claude Sonnet 4\.6, total token usage rises moderately across all methods: Standard increases from 741 tokens atd=2d=2to 971 atd=5d=5, Reasoning from 857 to 1068, and the Formalizer from 1257 to 1595\. For the OpenAI systems, the increase is steepest in the Reasoning condition, where o4\-mini grows from 1296 tokens atd=2d=2to 1835 atd=5d=5\. By contrast, the GPT\-4\.1 Formalizer increases more moderately, from 1075 to 1303 tokens, while GPT\-4\.1 Standard remains relatively flat, ranging from 598 to 713 tokens across depths\.

Overall, reasoning\-based approaches, especially o4\-mini Reasoning, incur a substantial token overhead as depth increases\. The Formalizer uses more tokens than Standard models but its token usage grows predictably with context length and shows the lowest variation across questions\. This suggests that symbolic delegation provides a more controlled token\-scaling profile than extended natural\-language reasoning, while still achieving higher reliability than Standard models\.

#### Runtime by depth\.

![Refer to caption](https://arxiv.org/html/2606.14935v1/x7.png)\(a\)Claude
![Refer to caption](https://arxiv.org/html/2606.14935v1/x8.png)\(b\)GPT

Figure 5:Time elapsed by reasoning depth for Claude and GPT models\.Execution time follows a similar trend to token usage, increasing with reasoning depth for all systems, but with substantial differences in scaling \(Figure[5](https://arxiv.org/html/2606.14935#S5.F5)\)\. For Claude Sonnet 4\.6, runtime grows gradually across all methods: Standard increases from 3\.04 seconds atd=2d=2to 4\.27 seconds atd=5d=5, Reasoning from 3\.97 to 5\.45 seconds, and the Formalizer from 4\.40 to 5\.78 seconds\. At depths 3–5, the mean runtime of the Reasoning condition approaches that of the Formalizer, suggesting that the additional overhead of symbolic delegation becomes comparatively smaller as reasoning depth increases\.

For the OpenAI systems, the contrast is sharper\. The o4\-mini Reasoning condition rises from 9\.48 seconds atd=2d=2to 13\.37 seconds atd=5d=5, reflecting the latency cost of extended reasoning\. By contrast, the GPT\-4\.1 Formalizer increases only from 3\.61 to 4\.71 seconds, while GPT\-4\.1 Standard remains nearly constant at around one second across depths\. These results indicate that deeper reasoning consistently increases computational cost, but that symbolic delegation has substantially better runtime scaling than the reasoning\-model condition, particularly when the non\-tool baseline model is less reliable\.

SystemCorrectIncorrectClaudeStandard843±143843\\pm 143\(n=395\)\(n=395\)1281±1421281\\pm 142\(n=5\)\(n=5\)Reasoning957±222957\\pm 222\(n=400\)\(n=400\)–\(n=0\)\(n=0\)Formalizer1426±1731426\\pm 173\(n=400\)\(n=400\)–\(n=0\)\(n=0\)GPT/o4\-miniStandard656±53656\\pm 53\(n=305\)\(n=305\)649±48649\\pm 48\(n=95\)\(n=95\)Reasoning1547±5061547\\pm 506\(n=399\)\(n=399\)18801880\(n=1\)\(n=1\)Formalizer1189±1131189\\pm 113\(n=400\)\(n=400\)–\(n=0\)\(n=0\)

Table 5:Token usage \(mean±\\pmstd\) by system and evaluation outcome\.
#### Token usage by correctness\.

Table[5](https://arxiv.org/html/2606.14935#S5.T5)reports token usage separately for correct and incorrect predictions\. Except for GPT\-4\.1 in the Standard condition, incorrect answers use more tokens on average than correct answers\. This pattern is consistent with prior observations that reasoning models often generate more tokens on harder instances\[lin2025zebralogic\]\. However, the number of failures in the reasoning\-augmented conditions is very small\.

#### Causes of errors\.

ModelSystemTotalIncorrectIn SLDNF↓\\downarrowIn loopClaudeStandard400532ClaudeReasoning400000GPT/o4\-miniStandard4009521GPT/o4\-miniReasoning400101Table 6:Error breakdown under SLDNF evaluation\. SLDNF↓\\downarrowstands for evaluating to a different label than the gold label under SLDNF\.Motivated by the observation that most reasoning failures, except for GPT\-4\.1 in the Standard condition, occur on instances with negation in the rules, we further analysed the evaluation set under standard SLDNF semantics\. We identified two classes of instances: \(i\) instances whose answer under SLDNF differs from thePARARULE\-Plusgold label, and \(ii\) instances for which SLDNF evaluation does not terminate because of recursive rule cycles\. Table[6](https://arxiv.org/html/2606.14935#S5.T6)reports the breakdowns\.

For Claude, all five Standard errors fall into one of these two SLDNF\-related categories: three correspond to instances where SLDNF gives a different label from the dataset semantics, and two correspond to non\-terminating SLDNF evaluations\. The single o4\-mini Reasoning error also occurs on an instance that loops under SLDNF\. By contrast, GPT\-4\.1 Standard has many errors that are not explained by these categories, which is consistent with the earlier observation that its failures are not limited to the dataset’s non\-standard negation semantics\. These findings suggest that SLDNF\-related semantic mismatch may be the dominant residual failure mode for the strongest systems, but the depth\-stratified sample contains too few activating instances \(6 diverging answers and 15 non\-terminating evaluations\) to test this directly\. We therefore complement the present evaluation with a targeted set of SLDNF\-diverging instances in Section[5\.2](https://arxiv.org/html/2606.14935#S5.SS2)\.

#### Case study\.

On instanceNegationRule\-D5\-28653, with queryCharlie is smartand gold answer*true*, the two reasoning models diverge\. The intended derivation requires treatingCharlie is dullas unresolved against the initial facts \(it is not stated\), soCharlie is not dullevaluates to true, after which two rules \(if someone is not dull then they are kind;if someone is kind then they are smart\) yield the conclusion\. Claude follows exactly this chain\. GPT/o4\-mini instead pursuesCharlie is dullas an open subgoal, derives it via forward chaining from other rules, and so concludes the query is false—applying standard SLDNF rather than the prompt’s initial\-facts reading and constituting a reasoning failure\.

#### Discussion\.

Across depths and rule types, explicit reasoning and symbolic formalization both substantially improve over standard LLMs, with the largest gains where the base model is weakest: the GPT\-4\.1 Standard baseline reaches only 0\.762, while o4\-mini Reasoning and the GPT\-4\.1 Formalizer reach 0\.998 and 1\.000 respectively\. Most residual errors \(except for GPT\-4\.1 Standard\) occur on negation instances and concentrate on cases that either loop or receive a different label under SLDNF, consistent with the case\-study failure mode of defaulting to standard negation\-as\-failure rather than the dataset’s initial\-facts reading\. The depth\-stratified sample contains too few such cases to test this directly, motivating the targeted evaluation that follows\.

### 5\.2Targeted evaluation: SLDNF\-diverging instances

#### Dataset\.

To test the hypothesis that the residual errors observed in Section[5\.1](https://arxiv.org/html/2606.14935#S5.SS1)stem from semantic mismatch rather than reasoning depth, we constructed a dedicated set of SLDNF\-diverging instances from the negation\-type portion ofPARARULE\-Plus\. Each instance was converted to SWI\-Prolog and evaluated twice: once with the intendedPARARULE\-Plusencoding, in which body\-level negation is checked only against the initial fact base, and once with standard SLDNF variant\. Instances for which the two evaluations produced different Boolean answers or would loop under SLDNF were labelled*diverging*\. We collected 100 such instances at depth 4 and 100 at depth 5, giving a stratified targeted set of 200 instances\. All instances in this subset have expected answer*false*under thePARARULE\-Plussemantics\.

Table 7:Results on the 200 SLDNF\-diverging instances at reasoning depths 4 and 5\. All instances have expected answer*false*\. Acc\. = accuracy; Tok/q = mean total tokens per question; s/q = mean wall\-clock seconds per question\.SystemAcc\. \(all\)Acc\. D4Acc\. D5Tok/qs/qClaudeReasoning0\.950\.950\.910\.910\.990\.991345\.41345\.49\.59\.5Formalizer1\.001\.001\.001\.001\.001\.001548\.41548\.46\.26\.2GPT\-4/o4\-miniReasoning0\.940\.940\.940\.940\.940\.942070\.02070\.011\.911\.9Formalizer0\.990\.990\.980\.981\.001\.001191\.71191\.73\.13\.1
#### Discussion\.

Table[7](https://arxiv.org/html/2606.14935#S5.T7)shows that the targeted SLDNF\-diverging subset is substantially more challenging for natural\-language reasoning than the depth\-stratified sample, while the Formalizer remains near\-perfect\. Claude Reasoning drops from 1\.00 to 0\.95 and o4\-mini Reasoning from 0\.998 to 0\.94, while the Formalizer is essentially unchanged \(1\.00 for Claude, 1\.00–0\.99 for GPT\-4\.1\)\. The reliability advantage of symbolic delegation is therefore largest precisely where natural\-language reasoning is most fragile\.

This robustness is structural: the generated program encodes thePARARULE\-Plussemantics explicitly, checking body\-level negations against the fixed extensional database rather than against the full derivable closure\. The solver is never asked to apply raw SLDNF to those negations, so the main difficulty is shifted from inference to producing a faithful formalization\. The depth\-wise pattern supports the same interpretation: Claude Reasoning is less accurate at depth 4 than at depth 5, and o4\-mini Reasoning is stable across both, so the failures are not explained by reasoning depth but by whether the derivation activates a predicate that is absent from the initial facts yet derivable through rules—the configuration in whichPARARULE\-Plusand SLDNF disagree\.

The cost results reinforce the broader reliability–efficiency trade\-off: the Formalizer is faster than the Reasoning condition for both model families \(6\.2 s vs\. 9\.5 s for Claude; 3\.1 s vs\. 11\.9 s for the OpenAI systems\), and the GPT\-4\.1 Formalizer is simultaneously more accurate and substantially faster than o4\-mini Reasoning while using fewer tokens\. Externalising the formal inference step to a Prolog solver is most beneficial when the task departs from interpretations the model would default to, rather than simply requiring longer reasoning chains\.

## 6Conclusions

We introducedPrologMCP, an MCP\-based interface that lets LLM agents delegate symbolic reasoning to a Prolog solver, separating two capabilities often conflated in LLM evaluations: translating an informal problem into a formal representation, and carrying out the resulting inference\. The model is responsible for formalization; the solver performs the deductive step\.

We evaluatedPrologMCPonPARARULE\-Plusalong two axes: a depth\-stratified sample, and a targeted subset that isolates instances where the dataset’s negation semantics diverges from standard SLDNF\. The Formalizer reached perfect accuracy on the depth\-stratified sample for both model families, with the clearest gains over the weaker GPT\-4\.1 Standard baseline and lower latency than o4\-mini Reasoning\. On the targeted SLDNF\-diverging subset the Formalizer remained near\-perfect \(1\.00 for Claude, 0\.99 for GPT\-4\.1\) while the Reasoning conditions dropped to 0\.95 and 0\.94—exposing a failure mode where models default to standard negation\-as\-failure even when instructed otherwise\. By encoding the intended semantics in the generated Prolog program, the Formalizer sidesteps this and shifts the burden from inference to translation\. The approach does not remove the need for accurate semantic translation, motivating future work on validation of generated logic programs and broader benchmark coverage\.

## 7Limitations and Future Work

The current evaluation relies on a single synthetic benchmark and a closed, frontier\-only model set; the cross\-system comparison is also not architecturally controlled\.PrologMCPitself supports only SWI\-Prolog, and its lexical sandbox is not a security boundary\. Because all instances formalised on the first attempt, onlyconsult\_textandrun\_goalwere thoroughly exercised\. Immediate next steps include broader and harder benchmarks, weaker and open\-source models, fine\-tuning small models for the formalization step, additional Prolog dialects, container\-level isolation, and a routing layer over domain\-specialised MCP servers that dispatches sub\-problems to the appropriate solver\.

###### Acknowledgements\.

This work was supported by a Leverhulme Trust International Professorship Grant \(LIP\-2022\-001\)\.

## Declaration on Generative AI

During the preparation of this work, the author\(s\) used Claude Code in order to: Generate code\. Further, the author\(s\) used Claude in order to: Improve writing style\. After using these tool\(s\)/service\(s\), the author\(s\) reviewed and edited the content as needed and take\(s\) full responsibility for the publication’s content\.

## References

## Appendix APARARULE\-Plus

Example instance: non\-negation, peopleInstance ID:NonNegationRule\-D2\-11112Context\.Charlie is strong\. Charlie is high\. Charlie is huge\. Bob is thin\. Bob is small\. Erin is quiet\. Erin is smart\. Erin is kind\. Anne is bad\. Anne is sad\. Anne is rough\. Strong people are quiet\. If someone is thin and small then they are short\. If someone is bad and sad then they are poor\. If someone is quiet and smart then they are wealthy\. All short people are little\. All quiet people are smart\. All wealthy people are nice\. All poor people are dull\.Query\.Charlie is not smart\.

Example instance: negation, peopleInstance ID:NegationRule\-D2\-6305Context\.Alan is big\. Alan is high\. Gary is small\. Gary is thin\. Fiona is smart\. Harry is bad\. Harry is poor\. If someone is not strong then they are bad\. If someone is not sad then they are nice\. If someone is smart then they are kind\. If someone is kind and not rough then they are quiet\. If someone is bad and not strong then they are dull\. If someone is small and thin then they are rough\. If someone is rough and not kind then they are poor\. All nice people are wealthy\.Query\.Fiona is quiet\.

Example instance: non\-negation, animalInstance ID:NonNegationRule\-Animal\-D2\-13824Context\.The wolf is dull\. The wolf is sleepy\. The wolf is slow\. The wolf sees the mouse\. The bald eagle chases the rabbit\. The bald eagle is heavy\. The bald eagle is big\. The mouse is smart\. The mouse is kind\. The mouse is round\. The rabbit is lovely\. The rabbit is small\. The rabbit is cute\. Smart animals are lovely\. If something is sleepy then it attacks the mouse\. If something attacks the mouse then it is rough\. If something is dull and sleepy then it is slow\. If something is lovely and small then it is furry\. If something is heavy and big then it is awful\. All slow animals are lazy\. All lovely animals are small\. All awful animals are strong\. All furry animals are beautiful\.Query\.The wolf is not lazy\.

Example instance: negation, animalInstance ID:NegationRule\-Animal\-D2\-3081Context\.The bald eagle is sleepy\. The bald eagle is rough\. The leopard is heavy\. The leopard is fierce\. The bald eagle visits the rabbit\. The leopard sees the dog\. The rabbit is nice\. The dog is nice\. The dog is furry\. The dog is lovely\. If something is not nice then it needs the rabbit\. If something needs the rabbit then it is slow\. If something is not round then it is heavy\. If something is not strong then it is cute\. If something is furry then it is lovely\. If something is lovely and not big then it is small\. If something is heavy and not round then it is awful\. If something is sleepy and rough then it is big\. If something is big and not lovely then it is fierce\. All cute animals are beautiful\.Query\.The bald eagle is awful\.

## Appendix BTool schemas

consult\_textload Prolog source into a new sessionReturns aload\_idused by all other tools\.``` { "type": "object", "properties": { "source_text": {"type": "string"}, "dialect": {"type": "string", "enum": ["swi"], "default": "swi"}, "module_name": {"type": "string"}, "include_predicates": {"type": "boolean", "default": false} }, "required": ["source_text"] } ``` Response keys\.load\_id\(string\),module\_name\(string\),dialect\("swi"\),messages\(list of\{severity, kind, message, line, column\}\), and — wheninclude\_predicatesistrue—predicates\(list of predicate descriptors\)\. Compile\-time errors are reported throughmessagesrather than as a top\-level error: the session is created so the agent can inspect and repair\.

run\_goalexecute a goal in an existing session``` { "type": "object", "properties": { "load_id": {"type": "string"}, "goal": {"type": "string"}, "max_answers": {"type": "integer", "default": 10}, "time_limit": {"type": "number", "default": 30.0}, "max_depth": {"type": "integer", "default": 1000000}, "allow_side_effects": {"type": "boolean", "default": true} }, "required": ["load_id", "goal"] } ``` Response keys\.outcome\("success"∣\\mid"failure"∣\\mid"timeout"∣\\mid"depth\_exceeded"\),answers\(list of variable\-binding maps with typed values\),output\(any capturedstdoutfrom the goal\),truncated\(boolean:truewhen more answers were available thanmax\_answersreturned\)\. Goal exceptions are returned as a top\-level error withkinddrawn fromtype\_error,existence\_error,instantiation\_error,permission\_error, orexecution\_exception\.

inspect\_predicatereturn the live definition of a named predicate``` { "type": "object", "properties": { "load_id": {"type": "string"}, "name": {"type": "string"}, "arity": {"type": "integer"} }, "required": ["load_id", "name", "arity"] } ``` Response keys\.found\(boolean\),type\(static∣\\middynamic∣\\midforeign∣\\midundefined\),exported\(boolean\),clause\_count\(integer\),clauses\(list of source\-form clauses\)\. On miss,candidateslists predicates whose name matches up to fuzzy comparison, suitable for repair\.

list\_messagesreturn diagnostics accumulated for a session``` { "type": "object", "properties": { "load_id": {"type": "string"}, "min_severity": {"type": "string", "enum": ["info", "warning", "error"], "default": "info"} }, "required": ["load_id"] } ``` Response keys\.messages\(list of\{severity, kind, message, line, column\}records\)\. Messages accumulate across all calls in the session; the caller filters bymin\_severity\.

run\_testsrunplunittests in the sessionOptionally loads additional test source first\.``` { "type": "object", "properties": { "load_id": {"type": "string"}, "test_source_text": {"type": "string"} }, "required": ["load_id"] } ``` Response keys\.passed,failed,skipped,total\(integers\);results\(list of per\-test records with name, status, and failure message if applicable\)\.

trace\_goaltrace a goal via a depth\-bounded meta\-interpreterReturns a structured proof tree\.``` { "type": "object", "properties": { "load_id": {"type": "string"}, "goal": {"type": "string"}, "max_depth": {"type": "integer", "default": 10}, "max_nodes": {"type": "integer", "default": 200} }, "required": ["load_id", "goal"] } ``` Response keys\.tree\(nested object withgoal,rule,children\),node\_count\(integer\)\. Implemented through a custom meta\-interpreter rather than SWI\-Prolog’s tracer; output is structured rather than line\-oriented\.

replace\_predicatereplace the clauses of a single predicatesource\_textmust define only the target name/arity\.``` { "type": "object", "properties": { "load_id": {"type": "string"}, "name": {"type": "string"}, "arity": {"type": "integer"}, "source_text": {"type": "string"} }, "required": ["load_id", "name", "arity", "source_text"] } ``` Response keys\.predicate\(echo ofname/arity\),messages\(list of diagnostics from the patch load, with line and column locators referring to the replacement source\)\. The session is left in its prior state if the patch fails to compile; partial replacement is never observed\.

get\_sourcereturn the current source of a sessionReconstructed from all live clauses; reflects any replacements made since load\.``` { "type": "object", "properties": { "load_id": {"type": "string"} }, "required": ["load_id"] } ``` Response keys\.source\(string\)\.

close\_sessionterminate a session and release resourcesReleases the subprocess and the session’s temporary directory\.``` { "type": "object", "properties": { "load_id": {"type": "string"} }, "required": ["load_id"] } ``` Response keys\.closed\(boolean\)\. Sessions are also released automatically when the registry’s TTL expires or when LRU eviction triggers; explicit close is a courtesy for long\-running agents\.

## Appendix CExperimental prompts

### C\.1Formalizer\-agent system prompt

Formalizer agent``` You are a mechanical translator from English to SWI-Prolog. Your job is \ purely syntactic: map each English sentence to its Prolog equivalent \ one-by-one. Do not trace, evaluate, or solve the reasoning problem. Given a CONTEXT (facts and rules) and a yes/no QUESTION, produce: 1. Valid SWI-Prolog source code that captures every fact and rule. 2. A single query goal: - goal_true -- SUCCEEDS when the answer is TRUE If goal_true fails, the answer is FALSE (closed-world assumption: anything not provable from the given facts and rules is false). SWI-Prolog conventions: - All atom names are lowercase and use underscores for spaces: ‘anne‘, ‘is_kind‘, ‘likes_fish‘ - Facts: ‘kind(anne).‘ ‘likes(bob, alice).‘ - Rules: ‘nice(X) :- kind(X).‘ - Negation-as-failure: ‘\\+‘ (e.g. ‘not_big(X) :- \\+ big(X).‘) - Variables start with uppercase: ‘X‘, ‘Y‘, ‘Who‘ - Do NOT add a module declaration; the server handles namespacing. - Do NOT add ‘‘:- discontiguous‘‘ declarations; the server injects them automatically for any predicate with multiple clauses. - For every predicate that appears ONLY inside ‘‘\\+‘‘ and is not defined by any fact or rule, add ‘‘:- dynamic pred/arity.‘‘ -- otherwise SWI-Prolog throws existence_error instead of failing cleanly. Negation -- critical rule (no exceptions, apart from goal): Every ‘‘\\+‘‘ in a rule body MUST check ‘‘initially/2‘‘, never the derived predicate directly. Do not reason about whether a predicate could be derived -- apply this rule unconditionally to every negation: - Assert every base fact in TWO forms: ‘‘pred(entity).‘‘ and ‘‘initially(pred, entity).‘‘ - Write ‘‘\\+ initially(pred, X)‘‘ for EVERY negation in every rule body. Example -- "if someone is not high then they are dull": dull(X) :- \\+ initially(high, X). % correct dull(X) :- \\+ high(X). % WRONG -- high/1 may be derived Example -- "if someone is sad and not quiet then they are rough": rough(X) :- sad(X), \\+ initially(quiet, X). % correct rough(X) :- sad(X), \\+ quiet(X). % WRONG -- quiet/1 may be derived Do **not** put ‘‘initially/2‘‘ in the goal. Example goal -- "Anne is not sad." \\+sad(anne). Response format -- output ONLY the XML tags below, no reasoning text: <prolog> % facts and rules fact(entity). initially(fact, entity). conclusion(X) :- premise(X). </prolog> <goal_true>query_predicate(entity)</goal_true> ```

### C\.2Standard\-LLM \(and Reasoning\) system prompt

Standard LLM&reasoning``` You are a logical reasoning expert. Given a context (a set of facts and \ rules) and a yes/no question, determine the answer using only the information \ provided. Use the closed-world assumption: if something cannot be derived \ from the given facts and rules, treat it as false. Negation has two different readings depending on where it appears. (1) Negation inside a rule body -- initial-facts reading. When a rule condition says "not X", check only whether X appears as a \ directly stated fact in the initial context -- not whether X can be derived \ through rules. Even if a person acquires property X through a chain of \ rules, they still satisfy "not X" in other rule bodies, because X was not \ initially stated for them. Example: if "rough" is not stated for Anne but can later be derived, then \ the rule "if someone is not rough then they are smart" still fires for \ Anne -- she counts as "not rough" because rough was not an initial fact. (2) Negation in the question -- full-derivation reading. When the question itself asks whether "not X" holds of someone, use \ both facts and rules: "not X(a)" is true \ iff X(a) cannot be derived from the facts and rules (whether directly \ stated or obtained through any chain of rule applications). Do not apply \ the initial-facts reading here -- it is specific to rule bodies. Example: if "energetic" is not stated for Bob but can be derived for \ Bob via some rule chain, then the question "is Bob not energetic?" is \ false, because energetic(Bob) is derivable. The question "is Bob not \ energetic?" is true only if energetic(Bob) is neither stated nor \ derivable. Procedure: when evaluating rule bodies, freeze the set of initial facts \ and check negated conditions against that frozen set; when evaluating the \ question, run the full derivation and check negated questions against the \ closure. Reply with exactly one word: true or false. - true -- the question follows from the context - false -- the question does not follow from the context ```