XLOG: A CUDA-Native Engine for Neurosymbolic Integration

# XLOG A CUDA-Native Engine for Neurosymbolic Integration
Source: [https://arxiv.org/html/2609.27203](https://arxiv.org/html/2609.27203)
Nikita PospelovKirill SabitovAffiliation:Brainyblaze Dynamics Inc\.Affiliation:levi@brainyblaze\.com,nikita\_pospelov@brainyblaze\.com,kirill@brainyblaze\.comAffiliation:[https://github\.com/BrainyBlaze/xlog](https://github.com/BrainyBlaze/xlog)Affiliation:Technical Whitepaper

July 2026

###### Abstract

xlog is a CUDA\-native logic programming engine that couples neural perception with deterministic Datalog, probabilistic inference, and epistemic reasoning over world views through a shared typed frontend and provider\-owned CUDA runtime\. The routes share device data planes but not one universal execution boundary: ordinary Datalog and exact inference are host\-orchestrated, while the certified resident recursive and Monte Carlo sampled cores record zero tracked host–device transfers and then return one bounded terminal receipt\. End\-to\-end gradients are realized through the probabilistic path\. A CUDA\-backed knowledge\-compilation pipeline \(provenance→\\toCNF→\\toDecision\-DNNF→\\tocircuit\) turns neural outputs into a differentiable circuit whose forward pass is exact weighted model counting and whose backward pass yields exact gradients\. The final smoothed circuit is certified against its back\-end source formula before it is cached or evaluated: bounded status and error scalars are observed by the host, while resolution\-proof traces are checked on the GPU\. A resident Monte Carlo alternative covers supported programs for which approximate inference is selected\. Circuit caching yields a2\.74×2\.74\\timesMNIST\-addition training speedup, and a worst\-case\-optimal join subsystem a27\.96×27\.96\\timesgeometric\-mean gain over xlog’s own binary\-join baseline\. Against external engines the picture is mixed: MNIST\-addition accuracy matches Scallop’s \(0\.95610\.9561against0\.94680\.9468\) and we make no per\-epoch speed claim, because the baseline’s epoch time is not monotone in the host’s CPU quota; across five hub\-skewed triangle\-counting cases the Soufflé\-to\-fused\-xlog execution\-time ratio*grows with the input*, from0\.88×0\.88\\timesat150150k edges — where Soufflé is the faster engine — to5\.54×5\.54\\timesat1\.21\.2M, while fused peak device allocations stay between8585and1,0331\{,\}033MB against3,2873\{,\}287to44,97944\{,\}979MB for the materializing arm, and every arm completes; and exact inference is correctness\-equivalent to but slower than ProbLog2\. On a public video benchmark, a proximity predicate trained through symbolic credit alone, never shown a distance label, replaces hand\-set geometry at no cost in held\-out accuracy; the same detector inside the Event\-Calculus rule search does not survive ten\-fold cross\-validation, and on a leak\-free split the committed clause does not transfer\. On a maritime corpus of thousands of gold events, weighted clauses beat crisp selection by0\.0650\.065F1, and a single chronological training pass reproduces that result exactly\.

## 1Introduction

Neurosymbolic systems combine neural perception with symbolic reasoning, but established integrations often place the two halves on different processors\. Deep learning frameworks—PyTorch, JAX—execute dense tensor computation on the GPU through optimized CUDA kernels, while systems such as DeepProbLog\[[25](https://arxiv.org/html/2609.27203#bib.bib5)\]and NeurASP\[[43](https://arxiv.org/html/2609.27203#bib.bib6)\]use CPU\-side symbolic backends\. Their integration can therefore cross the PCIe bus for network outputs, symbolic results, or gradients\. At scale, repeated host–device movement can dominate wall\-clock time and bandwidth\.

The transfer wall is one half of the problem; fragmented interfaces are the other\. Existing neurosymbolic frameworks commonly bridge a neural network to one symbolic backend \(DeepProbLog to probabilistic logic, NeurASP to answer\-set programming\)\. GPU logic efforts, conversely, accelerate focused workloads such as deterministic Datalog\[[36](https://arxiv.org/html/2609.27203#bib.bib1),[34](https://arxiv.org/html/2609.27203#bib.bib2)\]or SAT\[[28](https://arxiv.org/html/2609.27203#bib.bib7)\]\. xlog explores how a typed language and shared CUDA services can support deterministic, probabilistic, epistemic, and neural\-symbolic use without pretending that those routes have identical execution or differentiability properties\.

xlog is a CUDA\-native logic programming language whose compiler and runtime treat a neural network as an ordinary predicate\. Network outputs can become weighted facts for probabilistic knowledge compilation, where exact query gradients flow back to the network\. Other reasoning modes reuse the typed relational and solver interfaces without claiming the same gradient semantics\. Device\-resident buffers carry facts, deltas, circuits, solver state, and gradients, while the host performs orchestration, I/O, compilation, and bounded control reads\. The certified resident recursive and Monte Carlo sampled cores provide the stronger measured boundary: no tracked host–device transfers inside the core, followed by one terminal receipt\. Verified knowledge compilation certifies the final smoothed circuit against its back\-end formula before use, and DLPack\[[14](https://arxiv.org/html/2609.27203#bib.bib15)\]exports device gradient buffers directly into PyTorch’s autograd graph\.

The principal contributions of this paper are:

- •A shared neurosymbolic integration model\.A neural network is a predicate, and typed device\-buffer interfaces connect it to the supported reasoning routes\. End\-to\-end gradient training is realized specifically through the probabilistic knowledge\-compilation path \([Sections2](https://arxiv.org/html/2609.27203#S2)and[6](https://arxiv.org/html/2609.27203#S6)\)\.
- •CUDA relational execution with a certified resident route\.Semi\-naive Datalog evaluation with stratified negation and aggregation uses custom CUDA relational kernels\. Eligible recursive query plans are selected automatically for a resident conditional graph whose measured core has no tracked transfers; the wider ordinary executor remains host\-orchestrated\. A worst\-case\-optimal join \(WCOJ\) subsystem avoids the intermediate\-relation blowup of binary\-join plans on skewed cyclic queries \(a measured27\.96×27\.96\\timesgeometric\-mean ablation,[Section4](https://arxiv.org/html/2609.27203#S4)\)\.
- •Verified knowledge compilation\.A CUDA\-backed provenance→\\toCNF→\\toDecision\-DNNF→\\tocircuit pipeline certifies the final smoothed circuit against its back\-end source formula before caching or evaluation\. The host observes bounded solver status and error scalars; resolution\-proof traces are checked on the GPU\. Structural invariants required for weighted model counting are established separately by construction \([Section5](https://arxiv.org/html/2609.27203#S5)\)\.
- •End\-to\-end differentiable training with zero\-copy interop\.Compiled circuits are cached across iterations and evaluated as level\-parallel forward/backward kernels, with gradients exported zero\-copy via DLPack and Arrow; circuit caching yields a measured2\.74×2\.74\\timestraining speedup\. Term embeddings and differentiable ILP ride the same device\-resident path \([Section6](https://arxiv.org/html/2609.27203#S6)\)\.
- •Perception learned through symbolic credit on an external benchmark\.On the CAVIAR video\-event corpus, under a direct per\-timestep target, the rule search returns the same theory whether its proximity predicate is the hand\-set geometric one that dedicated rule learners are handed or a network trained by the logic’s own credit alone, never shown a distance label or any target of its own, at no cost in held\-out accuracy\. Event\-Calculus rules over the precomputed predicate are induced under pre\-registered gates; substituting the learned detector inside*that*search is where the result currently fails \([Section7](https://arxiv.org/html/2609.27203#S7)\)\.
- •Rule induction at scale\.On the Brest AIS maritime corpus \(3,548 goldrendezVousintervals\) the same protocol, over pair\-level folds and permutation\-null gates, measures in isolation the two mechanisms the published Event\-Calculus learners are built on\. Weighting the clauses of the same gated pool raises micro F1 by0\.0650\.065over crisp selection, against our own prior expectation that it would not, and learning those weights in a single chronological pass reproduces the batch predictions exactly, for a reason we can name\. We draw no comparison with the published maritime figure, whose temporal grid differs from ours \([Section8](https://arxiv.org/html/2609.27203#S8)\)\.
- •Reasoning beyond probability\.Epistemic reasoning over world views \(know/possibleunder founded and Gelfond\-style semantics\) and well\-founded semantics execute on the same substrate over finite supported programs, including positive modal fixpoints and supported recursion through negation evaluated by GPU\-backed well\-founded semantics, reusing the CDCL, join, and circuit machinery instead of a separate engine \([Section9](https://arxiv.org/html/2609.27203#S9)\)\. The accepted fragment and its bounds are in[Section12](https://arxiv.org/html/2609.27203#S12)\.

Target workloads\.Avoiding repeated data\-plane copies matters most where the symbolic workload is large and repeated: program\-analysis queries over millions of ground atoms, probabilistic logic with many training iterations that share one compiled circuit, and knowledge\-graph reasoning with trainable entity embeddings\. Small tasks such as MNIST addition exercise the integration end\-to\-end but sit below this regime\. They demonstrate correctness and the circuit\-caching effect, with the measured transfer component secondary: approximately 10% of a training step at a standard batch and lost in run\-to\-run variation when a step makes only a handful of neural→\\tosymbolic handoffs \([Section10\.6](https://arxiv.org/html/2609.27203#S10.SS6)\)\. Accordingly, xlog targets NVIDIA\-GPU workloads whose byte working set and fixed capacities fit the selected route \([Section12](https://arxiv.org/html/2609.27203#S12)\) and that need neural perception coupled to exact, verified probabilistic inference rather than fuzzy relaxations\.

[Section2](https://arxiv.org/html/2609.27203#S2)presents the integration model and system architecture\.[Section3](https://arxiv.org/html/2609.27203#S3)describes the xlog language\.[Section4](https://arxiv.org/html/2609.27203#S4)details the GPU\-resident symbolic substrate\.[Section5](https://arxiv.org/html/2609.27203#S5)presents verified knowledge compilation, the central technical result\.[Section6](https://arxiv.org/html/2609.27203#S6)ties the pieces together as end\-to\-end neurosymbolic learning\.[Section7](https://arxiv.org/html/2609.27203#S7)puts that surface on an external video\-event benchmark, and[Section8](https://arxiv.org/html/2609.27203#S8)carries the same induction protocol to a larger maritime corpus\.[Section9](https://arxiv.org/html/2609.27203#S9)extends the substrate to epistemic and other reasoning modes\.[Section10](https://arxiv.org/html/2609.27203#S10)reports evaluation results,[Section11](https://arxiv.org/html/2609.27203#S11)surveys related work,[Section12](https://arxiv.org/html/2609.27203#S12)discusses limitations and future work, and[Section13](https://arxiv.org/html/2609.27203#S13)concludes\.

## 2Integration Model and Architecture

### 2\.1The integration model

In xlog a neural network*is*a predicate\. A declaration binds a network to a predicate symbol; evaluating that predicate runs a forward pass, and the network’s softmax over a label set can become a distribution over weighted facts\. Typed device\-buffer interfaces make those values available to the supported reasoning routes\. Exact gradients of query values flow back through the probabilistic knowledge\-compilation route; deterministic and epistemic execution reuse the integration surface without claiming that gradient semantics\. Facts, circuit values, and gradient buffers remain device\-resident at their data\-plane handoffs, while orchestration and bounded control reads remain host responsibilities\.

### 2\.2GPU residency model

xlog keeps runtime data\-plane state in GPU memory and does not silently spill it or switch to a host executor\. The provider owns one device handle, stream pool, asynchronous resource, runtime, and memory manager\. Exceeding a configured byte budget raisesRESOURCE\_EXHAUSTED; exhausting a fixed row, tuple, sample, or other count capacity raisesCAPACITY\_EXCEEDED; and a bounded fixpoint that reaches its iteration limit raisesCONVERGENCE\_FAILURE\. Transfer counters delimit measured claims\. In particular, the certified resident recursive and Monte Carlo sampled cores record zero tracked transfers, then return one bounded terminal receipt whose status is authoritative\.

The payoff is bandwidth asymmetry\. PCIe 4\.0×16\\times 16delivers roughly 32 GB/s, while GPU HBM provides 1–3 TB/s\. A single unnecessary D2H round\-trip for a moderate relation \(10M tuples at 16 bytes,≈160\{\\approx\}160MB\) costs about 5 ms\. Keeping fact stores, deltas, circuit values, solver state, and gradient buffers on the GPU avoids copying those data planes through host memory; this claim does not erase the bounded control observations documented for each route\.

### 2\.3Crate architecture

Tier 4interfacesPython API \(PyO3\)pyxlogcommand\-line interfacexlog\-cliTier 3pipelinesdeterministicxlog\-gpuprobabilistic⋅\\cdotPIR⋅\\cdotverified KCxlog\-probneural\-symbolicxlog\-neuralxlog\-induceTier 2subsystemslanguage frontendxlog\-logicGPU runtime executorxlog\-runtimeGPU CDCL⋅\\cdotlocal searchxlog\-solveTier 1ir & deviceservicesrelational / epistemic IRsxlog\-irCUDA wrapper, Arrow/DLPackxlog\-cudaruntime statisticsxlog\-statsTier 0corescalar types⋅\\cdoterrors⋅\\cdotsymbol table⋅\\cdotmemory budgetsxlog\-coreruntime data plane⋅\\cdotgpu\-residentdepends onhost: orchestration⋅\\cdotI/O⋅\\cdotcompilationhost\-side foundation: shared types & traitsFigure 1:xlog crate hierarchy\. Each tier depends only on lower tiers; the shaded device plane marks GPU\-resident runtime data planes, while the host provides orchestration, I/O, compilation, and bounded control reads\.The workspace is organized into five tiers with strict layering: no crate depends on a peer or a higher tier \([Figure1](https://arxiv.org/html/2609.27203#S2.F1)\)\. A leaf*core*crate defines shared scalar types, error and memory\-budget types, canonical boolean parsing, and a bidirectional symbol table for dictionary\-encoded strings\. Above it, a tier of intermediate representations and device services wraps CUDA via cudarc\[[9](https://arxiv.org/html/2609.27203#bib.bib21)\], resolves embedded kernel modules, and exposes Arrow and DLPack interoperability\. Each CUDA provider owns its complete runtime resource graph; there is no process\-wide runtime singleton or alternate provider path\. The three core subsystems \(the typed language frontend of[Section3](https://arxiv.org/html/2609.27203#S3), the GPU runtime executor, and the GPU CDCL/local\-search solver\) compose into integrated pipelines for deterministic, probabilistic, and neural\-symbolic execution, which a PyO3\[[30](https://arxiv.org/html/2609.27203#bib.bib20)\]extension module \(pyxlog\) and a command\-line binary surface to users\.

### 2\.4From program to GPU plan

A program is compiled to a GPU\-executable plan in five stages\.

Parsing\.A PEG parser built with pest produces an AST covering the full surface, including probabilistic facts, annotated disjunctions, epistemic literals, and neural\-predicate declarations\.

Dependency analysisbuilds a graph with positive, negative, aggregate, probabilistic, and modal edges and computes its strongly connected components \(SCCs\) with Tarjan’s algorithm\. It establishes a deterministic stratum order for the ordinary monotone core and classifies supported nonmonotone components for their dedicated plans\.

Loweringfans out from the normalized AST into three reasoning IRs: deterministic and reduced ordinary rules become relational\-IR trees, probabilistic provenance becomes PIR, and modal programs retain their semantics in EIR\. Neural predicates compose with the applicable route\. SAT/MaxSAT and verification use a separate shared service instead of a fourth reasoning IR\.

Optimizationpushes predicates through joins, while lowering chooses a deterministic greedy join order\. Shape\-specific selectivity rewrites cover recognized triangle and four\-cycle plans; general dynamic\-programming join ordering is not active\. Eligible multiway rules are promoted to the WCOJ subsystem, and bound recursive queries can be rewritten via magic sets \([Section4](https://arxiv.org/html/2609.27203#S4)\)\.

Plan assemblyemits the route\-specific execution plan, whose relational work is dispatched to CUDA kernels\. Supported negated recursion uses GPU\-backed well\-founded semantics instead of the ordinary semi\-naive schedule\.

### 2\.5Reasoning IRs and circuit format

Three reasoning IRs keep the backends decoupled; probabilistic knowledge compilation also emits a downstream circuit format\. Each form has one role\.

RIR \(Relational IR\)is the algebraic tree \(Scan,Filter,Project,Join,GroupBy,Union,Distinct,Diff,Fixpoint, and the worst\-case\-optimalMultiWayJoin/ChainJoin\) carrying cardinality, skew, and delta\-vs\-full metadata\. Deterministic execution and reduced ordinary subprograms consume RIR; the other backends preserve additional semantics in their own IRs\.

PIR \(Provenance IR\)is the weighted Boolean formula \(Lit,NegLit,And,Or,Decision\) derived from provenance tracking over a probabilistic program, capturing its structure without execution order\.

XGCF \(xlog GPU Circuit Format\)is the compiled, device\-resident form: a levelized DAG whose level offsets let every node at one topological level evaluate in a single kernel launch, with forward \(log\-space weighted model counting\) and backward \(adjoint\) passes\.

EIR \(Epistemic IR\)preserves modal operators for world\-view reasoning and lowers to a dedicated GPU execution plan instead of ordinary relational algebra \([Section9](https://arxiv.org/html/2609.27203#S9)\)\.

GpuCnf and CDCLform a shared solver service, not a fourth reasoning IR\. Callers provide a device\-resident CNF formula for SAT/MaxSAT search or verification\. The CDCL service consumes that formula directly; XGCF remains the circuit format produced only by probabilistic knowledge compilation\.

## 3The xlog Language

Probabilistic facts \(p::f\.\) and neural predicate declarations \(nn/k\) are language\-level constructs covered in[Sections5](https://arxiv.org/html/2609.27203#S5)and[6](https://arxiv.org/html/2609.27203#S6)\.

### 3\.1Design principles

Three principles shape the surface, each chosen to enable GPU execution\.Typed predicates:every predicate has a statically known signature over a closed set of scalar types \(u32,u64,i32,i64,f32,f64,bool,symbol\), supplied by apreddeclaration or inferred during compilation, so argument mismatches are caught before any kernel is generated and allocation stays bounded and columnar\.Classified dependencies:negation, aggregation, modal operators, and recursion interact through SCC analysis on the predicate dependency graph\. The ordinary deterministic core requires a monotone or stratified schedule, while supported nonmonotone probabilistic and epistemic components enter dedicated plans, including GPU\-backed well\-founded semantics for supported recursion through negation\.One language for many paradigms:probabilistic facts, annotated disjunctions, neural predicates, and SAT constraints share the syntactic core of deterministic Datalog; parsing, normalization, and dependency analysis are shared, while backend\-specific lowering preserves the semantics needed by each plan\. Unsupported shapes and unbounded terms are rejected before execution; there is no implicit fallback\.

A minimal program exhibits the core surface:

prededge\(u32,u32\)\.

predreach\(u32,u32\)\.

edge\(1,2\)\.edge\(2,3\)\.edge\(3,4\)\.

reach\(X,Y\):\-edge\(X,Y\)\.

reach\(X,Z\):\-reach\(X,Y\),edge\(Y,Z\)\.

?\-reach\(1,N\)\.

Listing 1:Minimal xlog program: typed predicates, facts, a recursive rule, a query\.

### 3\.2Type system

Every predicate is assigned a schema over the eight scalar types, withf32/f64following IEEE 754\. Apreddeclaration supplies that schema explicitly; when it is omitted, compilation infers the schema from facts, rule heads, typed body columns, and arithmetic bindings\. String literals \("alice"\) map tosymbolthrough a global symbol table, giving the runtime dense integer identifiers while preserving source\-level readability;domaindeclarations introduce named aliases\. Type consistency is enforced by predicate schemas and lowering\-time checks: variable occurrences must agree with known column types, constants are validated against their destination columns, and arithmetic expressions preserve scalar types\.

prednode\(u32,symbol\)\.

predconnected\(u32,u32\)\.

predbridge\(u32,u32\)\.

node\(1,"alice"\)\.node\(2,"bob"\)\.

connected\(1,2\)\.

bridge\(A,B\):\-

connected\(A,B\),

node\(A,\_\),node\(B,\_\)\.

Listing 2:A well\-typed xlog program: typed bridge predicate\.
Declaringbridgeso that its head argument is constrained at two incompatible types \(e\.g\.symbolin the head butu32throughconnected\) rejects the program at compile time\.

### 3\.3Expressions, arithmetic, and user\-defined functions

Rule bodies may contain arithmetic, comparisons, and calls\. Arithmetic bindings use theisoperator \(D is X \+ Y\); the right\-hand side supports\+ \- \* / %, the built\-insabs,min,max,pow,cast, and user\-defined functions\. Comparisons compile toFilternodes and push below joins where profitable\. Float comparison uses a total ordering, soNaNand signed zeros yield deterministic results instead of contaminating downstream aggregations\.

predpoint\(u32,f64,f64\)\.

predclose\(u32,u32\)\.

point\(1,0\.0,0\.0\)\.

point\(2,0\.5,0\.5\)\.

point\(3,5\.0,5\.0\)\.

close\(A,B\):\-

point\(A,Xa,Ya\),

point\(B,Xb,Yb\),

A<B,

Dis\(Xa\-Xb\)\*\(Xa\-Xb\)

\+\(Ya\-Yb\)\*\(Ya\-Yb\),

D<1\.0\.

Listing 3:Arithmetic in rule bodies: pairwise proximity via squared Euclidean distance\.
A user\-defined function \(UDF\) is introduced withfunc, with optional parameter types and a return type after\-\>\. Arithmetic bodies \(optionally withif/then/else\) inline into the sameExprtrees as built\-in arithmetic and participate in the same predicate\-pushdown and expression\-level optimization\. A predicate body, as infunc get\_parent\(Child\) = Parent :\- parent\(Child, Parent\)\., contributes its relational literals immediately before the callingisbinding in an ordinary rule or integrity constraint\. Its relation may contribute zero, one, or many caller rows; the function syntax does not impose uniqueness, while ordinary set semantics deduplicates identical projected tuples\. Each invocation alpha\-renames its non\-parameter result and body\-local variables, and multiple calls expand from left to right\. Nested expansion is depth\-bounded; relational calls in conditional result branches and non\-term arithmetic arguments are rejected rather than hoisted or coerced with changed semantics\.

predraw\_score\(u32,f64\)\.

prednorm\_score\(u32,f64\)\.

funcclamp01\(X:f64\)\-\>f64=

ifX<0\.0then0\.0

elseifX\>1\.0then1\.0

elseX\.

raw\_score\(1,\-0\.3\)\.

raw\_score\(2,0\.7\)\.

raw\_score\(3,1\.4\)\.

norm\_score\(Id,N\):\-

raw\_score\(Id,R\),Nisclamp01\(R\)\.

Listing 4:User\-defined function:clamp01normalizes a raw score into the unit interval\.

### 3\.4Modules and imports

Programs decompose into\.xlogmodules on a search path\. Theusedirective loads a module \(use graph\.\) or selectively imports names \(use utils/math::\{abs, clamp\}\.\); aprivatemodifier hides declarations from importers\. The resolver traverses the import graph, detects cycles, validates participating declarations, and performs bounded cross\-module schema inference for undeclared predicate contributions before merging them\. The resulting logical program then undergoes full compiler type inference, dependency analysis, and route\-specific execution planning, so imported rules participate as if written inline\.

prededge\(u32,u32\)\.

predreach\(u32,u32\)\.

edge\(1,2\)\.edge\(2,3\)\.edge\(3,4\)\.

reach\(X,Y\):\-edge\(X,Y\)\.

reach\(X,Z\):\-reach\(X,Y\),edge\(Y,Z\)\.

Listing 5:Modulegraph\_lib\.xlog: predicate declarations and recursive reach rules\.
usegraph\_lib\.

?\-reach\(1,N\)\.

Listing 6:Entrygraph\_main\.xlog: importsgraph\_liband queriesreach\.

### 3\.5Aggregations and constraints

Aggregation operators—count,sum,min,max,logsumexp—appear at rule heads with an explicit aggregation variable and lower toGroupBynodes executed as radix\-sort\-and\-reduce kernels; the stratifier rejects aggregation inside a recursive SCC\. Integrity constraints are headless rules \(:\- body\.\) asserting thatbodyis unsatisfiable once evaluation reaches fixpoint; a violation raises a diagnostic\.logsumexpis included because it is the workhorse aggregation for probabilistic circuits, where log\-space numerical stability is essential \([Section5](https://arxiv.org/html/2609.27203#S5)\)\.

prededge\(u32,u32\)\.

preddegree\(u32,u32\)\.

edge\(1,2\)\.edge\(1,3\)\.

edge\(1,4\)\.edge\(2,3\)\.

degree\(X,count\(Y\)\):\-edge\(X,Y\)\.

:\-edge\(X,\_\),notdegree\(X,\_\)\.

?\-degree\(X,N\)\.

Listing 7:Stratified aggregation: per\-source out\-degree with an integrity constraint\.

### 3\.6Completeness over finite domains

The surface extends toward language completeness while preserving GPU\-native execution: accepted constructs normalize into the typed AST and lower through their semantic backend, while forms that cannot be lowered safely are rejected at compile time, since there is no hidden CPU interpreter to execute them\. The accepted extensions are finite typed lists \(\[\],\[H\|T\], thelist<T\>column type\), statically\-resolvable meta\-predicates \(ground,functor,=\.\., source\-factfindall,maplist\), explicit stratified negation\-as\-failure over deterministic relations, magic\-set rewriting of bound recursive queries, and finite probabilistic aggregates\. Deterministic extensions lower to relational joins and aggregations in RIR; probabilistic aggregates preserve their probabilistic intermediate representation\. Open\-ended generators, dynamic database mutation, unrestrictedcall/N, and runtime\-variable predicate names remain outside the contract\.

## 4GPU\-Native Symbolic Substrate

The deterministic Datalog engine supplies CUDA relational operators and device\-resident relation storage used across the system\. The algorithmic approach—semi\-naive fixpoint iteration over stratified programs—is well established; the contribution here is engineering\. The ordinary executor is host\-orchestrated\. For eligible recursive query plans, automatic selection instead uses a certified resident conditional graph: its core runs one recorded launch and synchronization with zero tracked host–device transfers, then returns one pinned terminal receipt carrying status, counters, trace metadata, and schema selection rather than tuple data\.

### 4\.1Semi\-naive evaluation on GPU

The executor processes an execution plan as strata ordered by the dependency analysis of[Section2](https://arxiv.org/html/2609.27203#S2)\. Non\-recursive SCCs evaluate each rule once, dispatching its RIR tree to the appropriate kernel and merging results per head predicate\. Recursive SCCs run semi\-naive iteration \([Algorithm1](https://arxiv.org/html/2609.27203#alg1)\): each rule is re\-evaluated through delta\-rewritten variants \(one per recursive scan occurrence, so a self\-join such asp\(X,Y\), p\(Y,Z\)contributes two variants\) and the new tuples are unioned, differenced against the full relation, and deduplicated, all on\-device, until no predicate produces new tuples\. The profiler records per\-operator timing, row counts, and peak memory, feeding the optimizer\.

Algorithm 1GPU semi\-naive evaluation of a recursive SCC\. All buffers are device\-resident\.1:SCC rules

ℛ\\mathcal\{R\}; relation store

SS\(device\-resident\)

2:least fixpoint of

ℛ\\mathcal\{R\}merged into

SS
3:foreach rule

r∈ℛr\\in\\mathcal\{R\}do

4:

Δr←Eval​\(r,S\)∖S\\Delta\_\{r\}\\leftarrow\\textsc\{Eval\}\(r,S\)\\setminus S⊳\\trianglerightseedΔ\\Delta; set difference on device

5:repeat

6:foreach rule

r∈ℛr\\in\\mathcal\{R\}, recursive scan

iiin

rrdo

7:

Tr,i←Eval​\(r⁡\[Δ​at​i\],S\)T\_\{r,i\}\\leftarrow\\textsc\{Eval\}\(r\[\\Delta\\text\{ at \}i\],S\)⊳\\trianglerightoneΔ\\Delta\-variant per self\-join

8:foreach head predicate

ppdo

9:

Δp←Dedup​\(\(⋃r,i​for​pTr,i\)∖Sp\)\\Delta\_\{p\}\\leftarrow\\textsc\{Dedup\}\\big\(\\big\(\\textstyle\\bigcup\_\{r,i\\text\{ for \}p\}T\_\{r,i\}\\big\)\\setminus S\_\{p\}\\big\)
10:

Sp←Sp∪ΔpS\_\{p\}\\leftarrow S\_\{p\}\\cup\\Delta\_\{p\}⊳\\trianglerightunion \+ sorted dedup on device

11:untilall

Δp=∅\\Delta\_\{p\}=\\emptysetoriteration cap reached

12:free all

Δ\\Deltabuffers

### 4\.2Relational kernels

xlog implements its relational algebra as direct CUDA kernels rather than wrappers over cuBLAS, cuSPARSE, or Thrust\. Bespoke kernels make allocation, synchronization, and host staging explicit and keep relational intermediate buffers on\-device\.[Table1](https://arxiv.org/html/2609.27203#S4.T1)summarizes them\.

Table 1:Core relational CUDA kernels\.The filter kernel makes a correctness\-critical choice for floating point\. Equality uses standard IEEE 754 semantics \(NaN≠NaN\\mathrm\{NaN\}\\neq\\mathrm\{NaN\}\); ordered comparisons use a total\-ordering transform that maps anf64bit pattern to ani64whose integer order matches the IEEE 754totalOrderpredicate \(−NaN<−Inf<\-\\mathrm\{NaN\}<\-\\mathrm\{Inf\}<negatives<−0\.0<\+0\.0<<\-0\.0<\+0\.0<positives<\+Inf<\+NaN<\+\\mathrm\{Inf\}<\+\\mathrm\{NaN\}\), so Datalog programs produce deterministic results for all floating\-point inputs\.

### 4\.3Adaptive join planning

The optimizer performs predicate pushdown using runtime statistics, decomposing filters above joins into left\-, right\-, and cross\-predicates\. Lowering chooses join order with a deterministic greedy heuristic\. A selectivity pass recognizes triangle and four\-cycle shapes, and prior execution statistics can be exported and merged before a later compilation\. A general dynamic\-programming join ordering is not active; configuration fields that resemble such a threshold do not change this planning path\.

### 4\.4Worst\-case\-optimal joins

Binary\-join plans can materialize intermediates asymptotically larger than the final result, the classic pathology for cyclic queries such as triangle enumeration\. This is not a corner case for xlog’s target workloads: program\-analysis queries \(points\-to, call\-graph and reachability inference over code\-dependency graphs\) can contain cyclic, skewed joins where intermediate size governs cost\. xlog addresses this with a worst\-case\-optimal join \(WCOJ\) subsystem\[[27](https://arxiv.org/html/2609.27203#bib.bib26),[38](https://arxiv.org/html/2609.27203#bib.bib27),[40](https://arxiv.org/html/2609.27203#bib.bib28)\]\. A pure\-Rust hypergraph planner analyzes rule bodies for multiway\-join eligibility, derives a deterministic variable ordering from cardinality and selectivity statistics, and emits aMultiWayJoin/ChainJoinnode when promotion preserves output semantics; other rules retain their ordinary binary\-join plan\.

The GPU kernel executes the join via count→\\todevice prefix scan→\\tomaterialize over flat sorted\-column storage, with a four\-byte metadata D2H total and no count\-vector transfer\. Coverage spans the triangle, 4\-cycles,KK\-clique templates \(K=5K\{=\}5–88\), recursive/SCC integration, and helper\-relation splitting that exposes inner skew to root\-level histograms\. A default\-on skew classifier decides per query whether to dispatch WCOJ: high\-skew inputs take the WCOJ path, while uniform or empty inputs select the binary\-join chain\.[Section10\.2](https://arxiv.org/html/2609.27203#S10.SS2)reports the measured speedup\.

### 4\.5Runtime optimization

Interactive and long\-running deployments \(REPL sessions, iterative solver loops, incremental training\) repeatedly evaluate similar queries over relations that change little between calls\. A stateless executor rebuilds join indices and recomputes shared subplans each time, paying the dominant cost repeatedly\. Three optimizations exploit this between\-call stability, each with explicit controls and zero added data\-plane transfers\. Common\-subexpression elimination caches safe deterministic subplans within an evaluation\. Adaptive re\-optimization adopts a compiler\-supplied candidate plan when mis\-plan telemetry crosses a configurable ratio, with output\-equivalence checks and rollback\. And a persistent hash\-index manager, keyed on relation generation, schema, and device, retains built indices across repeated sessions with deterministic LRU eviction \([Section10](https://arxiv.org/html/2609.27203#S10)\)\.

### 4\.6Reversible symbols

Datalog programs operate on strings, but GPU kernels operate on fixed\-width numeric columns\. xlog interns each unique string to a dense, sequentialu32identifier and resolves it back inO⁡\(1\)O\(1\)at output time\. Symbol columns then*are*ordinaryu32columns \(join, sort, filter, and dedup kernels operate on them with no special\-casing\) and the string table stays host\-side, since variable\-length data is needed only at ingestion and output\. Thesymboltype maps to Arrow’sDictionary\(UInt32, Utf8\), so export to columnar consumers \(cuDF, Polars, DuckDB\) is zero\-copy while preserving the compact internal representation\.

## 5Verified Knowledge Compilation

Knowledge compilation is the route that makes a neural network and a probabilistic logic program differentiable end\-to\-end\. A network’s softmax becomes a distribution over weighted facts; provenance tracking yields a weighted Boolean formula; and that formula compiles into an arithmetic circuit whose forward pass is exact weighted model counting and whose backward pass yields exact gradients\. Probabilistic systems such as ProbLog\[[16](https://arxiv.org/html/2609.27203#bib.bib4)\]follow this compile\-once/evaluate\-many model on the CPU\. xlog instead keeps the compilation and evaluation data planes in CUDA buffers while the host orchestrates stages and reads bounded control state\. Before use, xlog certifies the final smoothed circuit against its back\-end source formula; this certificate does not cover provenance extraction or CNF encoding\.

### 5\.1The compilation pipeline

The pipeline transforms a probabilistic program into a GPU\-resident arithmetic circuit \(the XGCF format\) through five host\-orchestrated stages \([Figure2](https://arxiv.org/html/2609.27203#S5.F2)\)\. Their intermediate data stays in device buffers, while solver completion is observed through bounded status and error scalars\.

provenanceφ\\varphihash\-consingCNFΦ\\Phi\(Tseitin\)prefix\-sum var IDsd\-DNNF \(D4\)BFS \+ block DFSXGCF circuitCClevelized DAGevaluateforwardlog⁡Z\\log Zbackward∇\\nabla✓on\-GPU CDCL equivalence certificateφ∧¬C\\varphi\\wedge\\lnot CandC∧¬φC\\wedge\\lnot\\varphibothunsat⇒C≡φ\\Rightarrow C\\equiv\\varphiresolution proofs checked on\-devicecomplete proof, not samplingφ\\varphiCCprovenC≡φC\\equiv\\varphi×\\timestyped verification errorotherwisegpu\-resident data planeFigure 2:Verified knowledge\-compilation pipeline\. The data plane uses CUDA kernels and device\-resident state under host orchestration\. The final smoothed circuitCCreaches evaluation only through the equivalence gate \(✓\): an on\-GPU CDCL solver provesφ∧¬C\\varphi\\wedge\\lnot CandC∧¬φC\\wedge\\lnot\\varphiboth unsatisfiable; the host observes bounded status and error scalars, and any failed or incomplete proof returns a typed error\.Provenance extraction\.Provenance over deterministic evaluation produces a weighted Boolean formula\[[19](https://arxiv.org/html/2609.27203#bib.bib37)\]\. An on\-device interner hash\-conses node batches through an atomic GPU hash table, deduplicating structurally identical subformulas; this is essential because grounding can produce exponentially many redundant subformulas, and interning on the host would force the uninterned graph into host memory—reintroducing the very transfer the pipeline exists to avoid\.

CNF encoding\.A Tseitin\[[37](https://arxiv.org/html/2609.27203#bib.bib18)\]transformation lowers the formula to CNF on the GPU, using parallel prefix sums to assign compact, gap\-free variable IDs and emit clauses into a device\-resident compressed\-sparse\-row structure\.

D4 compilation\.The CNF compiles into a Decision\-DNNF \(d\-DNNF\) circuit\[[11](https://arxiv.org/html/2609.27203#bib.bib34)\]via a GPU\-native variant of the D4 algorithm\[[23](https://arxiv.org/html/2609.27203#bib.bib14)\]: a BFS frontier exposes parallelism, per\-block DFS workers perform component detection, decision\-variable selection by VSIDS\-like activity\[[26](https://arxiv.org/html/2609.27203#bib.bib38)\], and recursive decomposition\. A smoothing pass forces every branch of an OR/decision node to mention the same variable set, and the result is levelized so each topological level evaluates in one kernel launch\. Decomposability, determinism, and smoothness \(the structural properties that make weighted model counting over a Decision\-DNNF correct\[[10](https://arxiv.org/html/2609.27203#bib.bib35),[8](https://arxiv.org/html/2609.27203#bib.bib36)\]\) are established by construction\. Certification runs after smoothing and therefore gates the exact final circuit that is cached and evaluated\.

### 5\.2Verification: a machine\-checked certificate

xlog does not trust the final compilation stage; it proves the final smoothed circuitCCequivalent to its back\-end source formulaφ\\varphi\([Algorithm2](https://arxiv.org/html/2609.27203#alg2)\)\. It solvesφ∧¬C\\varphi\\land\\lnot CandC∧¬φC\\land\\lnot\\varphion a GPU CDCL solver, and both must be unsatisfiable forC≡φC\\equiv\\varphi\. UNSAT results carry resolution proofs checked on\-device\. The host reads bounded status and error scalars before accepting that GPU proof result; a wrong, incomplete, or budget\-limited result returns a typed error and never reaches circuit caching or evaluation\.

The certificate says that the circuit computes the same Boolean function asφ\\varphi; the count\-correctness invariants are guaranteed separately, by construction\. The compilation back\-end thus becomes a machine\-checked stage instead of an assumption, closing the failure mode in which a silently miscompiled circuit would corrupt every downstream probability and gradient\. The check covers the back\-end stage specifically: provenance extraction and CNF encoding are trusted, and the certificate says nothing about them\. CPU\-side certified knowledge compilation exists\[[6](https://arxiv.org/html/2609.27203#bib.bib40)\]; the contribution here is performing the check on\-device, sharing the GPU substrate\. The same device\-resident CDCL substrate is reused for SAT/MaxSAT queries and for epistemic candidate validation \([Section9](https://arxiv.org/html/2609.27203#S9)\)\.

Algorithm 2Verified knowledge compilation\. The final smoothed circuit is accepted only if proven equivalent to its back\-end source formula\.1:weighted Boolean formula

φ\\varphi\(device\-resident\)

2:verified circuit

CC\(XGCF\), or typed error

3:

φ←InternHashCons​\(φ\)\\varphi\\leftarrow\\textsc\{InternHashCons\}\(\\varphi\)⊳\\trianglerightdedup via atomic GPU hash table

4:

Φ←TseitinCNF​\(φ\)\\Phi\\leftarrow\\textsc\{TseitinCNF\}\(\\varphi\)⊳\\trianglerightprefix\-sum variable IDs; CSR clauses

5:

C←D4​\(Φ\)C\\leftarrow\\textsc\{D4\}\(\\Phi\);

C←SmoothLevelize​\(C\)C\\leftarrow\\textsc\{SmoothLevelize\}\(C\)
6:

u1←CDCL​\(φ∧¬C\)u\_\{1\}\\leftarrow\\textsc\{CDCL\}\(\\varphi\\land\\lnot C\);

u2←CDCL​\(C∧¬φ\)u\_\{2\}\\leftarrow\\textsc\{CDCL\}\(C\\land\\lnot\\varphi\)
7:observe bounded status and error scalars for

u1,u2u\_\{1\},u\_\{2\}on host

8:if

u1≠Unsatu\_\{1\}\\neq\\textsc\{Unsat\}or

u2≠Unsatu\_\{2\}\\neq\\textsc\{Unsat\}then

9:returntyped verification error

10:check resolution proofs of

u1,u2u\_\{1\},u\_\{2\}on\-device

11:return

CC⊳\\trianglerightcache the exact circuit that was certified

The verified circuit supports a level\-parallel forward pass \(log\-space weighted model counting, one kernel per level, yieldinglog⁡Z\\log Z\) and a reverse\-order backward pass that accumulates per\-variable gradients\. Both leave their results in GPU\-resident buffers consumable directly by PyTorch via DLPack \([Section6](https://arxiv.org/html/2609.27203#S6)\)\.

### 5\.3Circuit caching

Building and certifying a circuit is the most expensive stage, on the order of a minute for a cold start on the MNIST\-addition benchmark, and a naive implementation pays it every epoch\. Measured separately, it is the equivalence proof and not the D4 compile that dominates that time \([Section10\.6](https://arxiv.org/html/2609.27203#S10.SS6)\)\. The key observation is that the circuit*structure*depends on the propositional structure of the grounded program and the evidence pattern, but*not*on the numerical weights\. When neural parameters change between iterations, the weights on probabilistic facts change while the Boolean formula and its compiled circuit stay identical\. The certified final smoothed circuit is therefore cached, keyed by a structural hash of the provenance graph and evidence configuration; subsequent iterations update only the weight buffers and run the forward/backward kernels\. On MNIST addition that amortization is what the circuit\-cache ablation of[Section10\.3](https://arxiv.org/html/2609.27203#S10.SS3)measures\.

### 5\.4Monte Carlo alternative

When the user selects approximate inference, xlog provides a GPU\-parallel Monte Carlo engine for its supported fragment\. It draws values for probabilistic facts on the GPU and evaluates the deterministic program in each sampled world, using rejection sampling or, when every evidence atom is a Bernoulli fact, evidence clamping that forces observed values and eliminates rejection waste\. Both methods report confidence intervals\. The resident sampler evaluates all worlds in a single device launch with a bounded device\-side fixpoint\. Its sampled core records zero tracked transfers; after synchronization, one pinned receipt returns status, counts, and trace metadata\. That receipt’s convergence status is authoritative: reaching the iteration bound returnsCONVERGENCE\_FAILURE, even if partial counters exist\. Fixed\-count exhaustion returnsCAPACITY\_EXCEEDED, byte\-budget exhaustion returnsRESOURCE\_EXHAUSTED, and unsupported fragments return their typed diagnostic; none selects a host execution path\.

## 6Neurosymbolic Integration

This section is where the relational substrate \([Section4](https://arxiv.org/html/2609.27203#S4)\), verified probabilistic knowledge compilation \([Section5](https://arxiv.org/html/2609.27203#S5)\), and device\-buffer interoperability meet\. Network outputs feed weighted facts into the probabilistic route; the final smoothed circuit is certified before use; and DLPack carries device gradient buffers into the neural optimizer without copying them through host memory\. Host orchestration and bounded control reads remain outside that zero\-copy data\-plane handoff\.

### 6\.1Neural predicates

In xlog a neural network*is*a predicate\. Thenn/4declaration embeds a network directly into the program:

nn\(network\_name,\[input\_vars\],output\_var,

\[output\_labels\]\)::predicate\(args\)\.

Listing 8:Neural predicate declaration \(nn/4\)\.This is not a foreign\-function escape hatch: it states that evaluatingpredicate\(args\)requires a forward pass through the named network, whose softmax over the label set becomes a distribution over probabilistic facts feeding the knowledge\-compilation pipeline of[Section5](https://arxiv.org/html/2609.27203#S5)\. On the Python side a PyTorch module is registered against the predicate:

program\.register\_network\("mnist\_net",net,optimizer\)

Listing 9:Registering a PyTorch module against a neural predicate\.Registration goes by type rather than by name\. A caller may state the arity of the network’s predicate, and that claim is checked against everynn/4declaration bound to the network in the program and rejected on mismatch: the program’s own declaration is the authority\. Per\-argument catalog sort identifiers may accompany the arity \(one per declared argument, refused without an arity or at the wrong length\) and an opaque content hash may identify the registered network, so a retrained one mints a new identity when it is registered again\. The engine interprets neither; both are carried for consumers, which read them back through a queryable metadata view together with each declaration’s predicate, predicate arity, input arity, and label set\. A downstream rule learner can therefore check a candidate against what the program declares instead of against a naming convention—the property[Section6\.5](https://arxiv.org/html/2609.27203#S6.SS5)relies on\.

The dataflow runs in two directions\.Forward:when evaluation reaches annn/4\-backed predicate, the registered module runs, and its softmax vector is decomposed into weighted probabilistic facts, one per label, and fed into the knowledge\-compilation pipeline of[Section5](https://arxiv.org/html/2609.27203#S5), whose circuit cache carries across iterations\.Backward:after the circuit computes the forward log\-probability and backward gradients via level\-parallel kernels, the per\-leaf gradient buffers are exported as DLPack tensors and injected into PyTorch’s autograd graph, and the optimizer updates the network as usual\. The GIL is released during GPU work, so CUDA execution does not block the interpreter\. A neural predicate is not confined to a query head: it may also appear inside rule bodies, so that the trainable object becomes a whole rule and not only a single perceptual predicate \([Section6\.4](https://arxiv.org/html/2609.27203#S6.SS4)\)\.

### 6\.2End\-to\-end training

The canonical example is MNIST addition \(the DeepProbLog benchmark\): given two digit images, predict their sum, with supervision only on sums: the network never sees individual digit labels\. The entire reasoning structure is two rules:

nn\(mnist\_net,\[X\],Y,\[0,1,2,3,4,5,6,7,8,9\]\)

::digit\(X,Y\)\.

addition\(X,Y,Z\):\-

digit\(X,D1\),digit\(Y,D2\),ZisD1\+D2\.

Listing 10:MNIST addition: a CNN\-backed digit predicate and an addition rule\.Thenn/4declaration connects the CNN todigit/2; the addition rule computes every consistent decomposition of a sum through probabilistic marginalization\. Each queryaddition\(i, j, s\)trains by minimizing−log⁡P​\(addition​\(i,j,s\)\)\-\\log P\(\{\\texttt\{addition\}\}\(i,j,s\)\)under the compiled circuit\. The driver compiles the program, registers the network, and runs the loop, which batches queries sharing a circuit template and runs forward/backward over the cached circuit:

program=pyxlog\.Program\.compile\(SRC\)

program\.register\_network\("mnist\_net",net,optimizer\)

program\.add\_tensor\_source\("train",train\_images\)

history=pyxlog\.train\_model\_tensor\(

program,queries,

epochs=epochs,batch\_size=batch\_size\)

Listing 11:Python driver: compile, register, train\.neural networkPyTorch forwardsymbolic groundingrules⋅\\cdotprovenanceverified circuitproven once⋅\\cdotcachedloss−log⁡P\-\\log Pper\-query NLL✓circuit backwardlevel\-parallel adjointoptimizer stepPyTorch autogradsoftmax→\\toweighted factsforwardlog⁡P\\log Pbackwardper\-leaf gradients exported via DLPack \(zero\-copy\)updateθ\\thetaone training iteration — circuit & proof reused across iterationszero tracked data\-plane transfers in the measured circuit hot regiongpu device\-residentPyTorchxlog substrateverified \([Figure2](https://arxiv.org/html/2609.27203#S5.F2)\)Figure 3:One neurosymbolic training iteration\. Neural tensors, circuit values, and gradient buffers occupy one CUDA device \(shaded plane\); the measured circuit hot region records zero tracked data\-plane transfers\. The host still orchestrates stages and observes bounded control state\. The final smoothed circuit is compiled and certified once \(✓,[Figure2](https://arxiv.org/html/2609.27203#S5.F2)\), then reused across iterations, and gradients re\-enter PyTorch’s autograd graph zero\-copy through DLPack\.The decisive performance property \([Figure3](https://arxiv.org/html/2609.27203#S6.F3)\) is that compilation and verification happen once, on the first forward pass\. Every later iteration reuses the cached circuit, executing only the weight update and the level\-parallel forward/backward kernels\. This is the mechanism behind the2\.74×2\.74\\timestraining speedup; the loss reduction across seeds confirms that gradients flow from circuit evaluation through the logic program back to the CNN, and the full timing breakdown is reported in[Section10](https://arxiv.org/html/2609.27203#S10)\.

### 6\.3Zero\-copy interoperability

A GPU\-native engine is only useful if results reach the frameworks researchers already use, without copies that would reintroduce the transfer wall\. xlog exposes its device\-resident state through four standard interfaces\.

DLPack\.Each relation column or gradient buffer becomes a managed DLPack\[[14](https://arxiv.org/html/2609.27203#bib.bib15)\]tensor whose GPU memory is reference\-counted and freed only when every consumer releases it; on import, xlog validates device, dtype, contiguity, and alignment, optionally against an expected schema\. In Python the protocol surfaces as a capsule, sotorch\.from\_dlpackyields a live CUDA tensor backed by the very memory xlog wrote\.

Arrow\.For columnar tools \(Polars, DuckDB, cuDF\), relations export through the Arrow\[[2](https://arxiv.org/html/2609.27203#bib.bib16)\]C Device Data Interface; symbol columns export as Arrow dictionary arrays, so a consumer reads symbolic columns as native string dictionaries while xlog keeps the compact integer representation\.

Python bindings\.Thepyxlogextension \(PyO3\[[30](https://arxiv.org/html/2609.27203#bib.bib20)\]\) exposes compilation, evaluation, training, and result extraction; tensor\-valued results are returned as DLPack capsules, and long\-running GPU operations release the GIL so data\-loader threads proceed concurrently\.

PyTorch autograd\.The circuit behaves as a differentiable function inside PyTorch: the network’s grad\-enabled forward feeds the circuit, the scalar loss is exported via DLPack and re\-imported, and a batched path stacks inputs into one forward pass and runs a single backward, so gradients flow from the logic layer back tonn\.Moduleparameters with no custom autogradFunction\.

### 6\.4Trainable rule bodies

Placing a neural predicate in a rule body lifts xlog from learning a single perceptual predicate to learning whole rules\. The tensor and circuit data planes remain device\-resident; route\-specific orchestration and control observations are documented separately\.

Mixed bodies\.A trainable body may interleave neural\-evaluated atoms with ordinary symbolic literals\. The symbolic literals act as hard join conditions: they gate which groundings can fire but carry no probability mass or gradient\. The head probability therefore factors as a0/10/1indicator of the symbolic condition times the neural probability scaled by a learned per\-rule weightσ⁡\(w\)\\sigma\(w\), and gradients flow only through the network outputs and the rule weight, never through the ground facts\.

Existential joins\.When an existential \(non\-head\) body variable is a neural predicate’s input, xlog grounds that predicate over the*real*join domain*inside*the circuit instead of stripping the join as a pre\-filter: the neural occurrence expands into one circuit leaf per domain event, and provenance OR\-aggregates∃e\.neural⁡\(e\)∧join⁡\(e,ℎ𝑒𝑎𝑑\)\\exists\\,e\.\\ \\mathrm\{neural\}\(e\)\\wedge\\mathrm\{join\}\(e,\\mathit\{head\}\)at each head binding\. This makes “does supporting evidence exist?” rules learnable, reasoning over a whole domain of events instead of only per\-instance classification\.

Joint multi\-rule mixtures\.Several same\-head trainable clauses combine as a noisy\-OR mixture,P⁡\(ℎ𝑒𝑎𝑑i\)=1−∏k\(1−rk​\[i\]​mk​\[i\]​σ​\(wk\)\)P\(\\mathit\{head\}\_\{i\}\)=1\-\\prod\_\{k\}\\bigl\(1\-r\_\{k\}\[i\]\\,m\_\{k\}\[i\]\\,\\sigma\(w\_\{k\}\)\\bigr\)\. Hererk​\[i\]r\_\{k\}\[i\]is a candidate’s relational eligibility,σ⁡\(wk\)\\sigma\(w\_\{k\}\)its learned rule weight, andmk​\[i\]m\_\{k\}\[i\]an optional graded confidence in\[0,1\]\[0,1\]carried per binding, for example a fact’s confidence trajectory over time\. Rule learning thus moves from binary rule eligibility to a continuous, differentiable weighting of competing and cooperating rules\.

Learned body gates\.Inside that mixture a candidate may also carry a neural conjunct over a per\-binding entity featureϕ⁡\(x\)\\phi\(x\): its eligibility becomes its relational grounding*and*a straight\-through\-thresholded gategθ​\(ϕ⁡\(x\)\)≥τg\_\{\\theta\}\(\\phi\(x\)\)\\geq\\tau\. A gated clause then competes against ungated ones on the same noisy\-OR terms, andgθg\_\{\\theta\}trains jointly with the rule weights under the same held\-out selector\. By defaultϕ\\phiis detached where it enters the engine: gradient reachesθ\\thetaand the rule weight but stops at the neural head, leaving the feature producer frozen\. Training the producer too is an explicit opt\-in per candidate: one flag leavesϕ\\phiattached, so gradient flows on into the backbone that computed it\. Only the autograd linkage changes; the values uploaded are identical either way\.

These trainable\-rule paths share the verified circuit and the zero\-copy substrate of the simpler predicate case, and extend to recursive programs now that provenance converges on two\-sided recursive strongly\-connected components\.[Section7](https://arxiv.org/html/2609.27203#S7)carries the surface onto a public benchmark: the perceptual predicate inside an induced Event\-Calculus rule body is trained through symbolic credit alone, cross\-validated under pre\-registered gates\.[Section12](https://arxiv.org/html/2609.27203#S12)states what that evidence does and does not support\.

### 6\.5Engine\-mode credit and candidate selection

Which of the candidate bodies the engine enumerates should the learner keep, and on what evidence? Learning a rule body is not only a gradient problem: it is also a decision about which candidate to keep, and the two need different evidence\. Engine\-mode training separates them\. The engine already enumerates the candidate space \(the well\-formed pairs of body relations over the program’s own binary relations\) and already holds the join extensions those candidates read, so training scores that space directly instead of a reconstruction of it\.

A candidate’s score on a fact is a noisy\-OR over the witnesses the engine reports for that fact: a neural body relation contributes a probability per witness, read at the fact’s own label, while a purely relational one contributes a fixed\{0,1\}\\\{0,1\\\}cover\. Candidates combine as a softmax over their logits, and the resulting negative log\-likelihood is a single autograd graph, so one backward pass updates the candidate logits and the network behind the probabilities together\.

A worked instance\.Take one head fact and two candidates for its body, one relational and one neural\. The relational candidate covers the fact or does not, so its score there is11or00\. The neural candidate’s score is the noisy\-OR over the witnesses the engine reports for that fact, each read at the fact’s own label: two witnesses at probability0\.50\.5give1−0\.5⋅0\.5=0\.751\-0\.5\\cdot 0\.5=0\.75, above a relational candidate that does not cover the fact and below one that does\. Those are training scores, and the arbiter never reads them\. It rescores both on the held\-out facts by the same witness semantics, drops either whose held\-out score falls below the fit gate, and keeps the relational one when the two land within the score quantum; if that narrowing leaves two relational candidates the data cannot separate, it abstains rather than pick one\.

The candidate pool is validated against the typed registry of[Section6\.1](https://arxiv.org/html/2609.27203#S6.SS1)instead of being trusted by name: a neural relation whose declared arity the credit has no witness semantics for is refused at registration, and a pool that filtering empties reports its per\-filter counts instead of silently shrinking\. And because raw engine constants index the caller’s feature rows directly, that identity is accepted only when the witness domain is exactly the dense row range; a misalignment that would stay in bounds while gathering another event’s probability draws a refusal instead of a guess\.

Selection on held\-out generalization\.Training credit cannot distinguish a crisp but coincidental rule from a soft but correct one, even in principle; generalization can\. Selection therefore never reads the trained weight\. The facts are split into folds; each fold trains on the rest and rescores every candidate on the held\-out facts by its own witness semantics; the arbiter ranks the fold\-averaged scores\. A*fit gate*then drops any candidate whose held\-out score falls below a threshold, since a rule that cannot fit held\-out data is not a rule\.

Ties within the score quantum break toward the relational candidate on Occam grounds, but only when that narrowing leaves exactly one: preferring a relational explanation over a neural one is licensed, choosing among relational duplicates the data cannot separate is not\. When neither step is decisive the arbiter returns no rule and says why; abstention is one of the selector’s outcomes\. The held\-out score may be accuracy or F1, and the choice matters: at a rare positive class accuracy sits on the all\-negative base\-rate plateau, where a candidate that predicts nothing outranks the best real detector, which is why the benchmark protocol of[Section7](https://arxiv.org/html/2609.27203#S7)selects on held\-out F1 instead\.

Masked witnesses and withheld evidence\.A per\-witness mask lets evidence be withheld rather than denied: a masked witness leaves the candidate’s index entirely, contributing zero credit and zero gradient instead of a coerced false, and the facts it thereby leaves uncertain are excluded from the held\-out score and counted against a coverage gate that runs before the fit gate, so no candidate is killed by facts it was never allowed to see\. The channel rides the accuracy axis only and is refused up front beside the F1 holdout, whose measurability derives from raw labels a mask can hide\.

Acceptance without retraining\.The same machinery also runs as an acceptance instrument: given an externally trained detector, a frozen entry point scores every enumerated candidate against it with no optimizer, no gradient and no folds and applies exactly the arbiter’s gates, so where the cross\-validated path asks whether a detector can be trained for a rule, this one asks whether a rule is right given the detector one already has\. A training\-mode module is refused rather than quietly switched, since batch\-norm statistics and dropout would de\-determinize the bit\-identical scores the entry point exists to provide\.

### 6\.6Term embeddings and differentiable ILP

Term embeddingsattach dense, optionally trainable vectors to logical symbols\. Wherenn/4maps perception to discrete facts, embeddings give logical entities a continuous representation that participates in neural computation, with gradients flowing through the embedding lookup: knowledge\-graph entity representations, for instance, trained jointly with neural perception\.

Differentiable ILPlearns first\-order rules instead of network weights\. Candidate rules are represented as sparse bitmasks over the ground\-atom space, credit assignment runs entirely on\-device via scatter–gather, and a promotion pipeline decides which rules enter the program\.

Four kinds of judgement sit on these two paths, and[Table2](https://arxiv.org/html/2609.27203#S6.T2)separates them\. Convergence and the supply of explicit held\-out examples are preconditions checked before any gate runs: with neither held\-out positives nor held\-out negatives supplied, the pipeline returns for manual review before a gate is evaluated, so the always\-run gates cannot promote on their own\.

The benchmark runs of[Section7](https://arxiv.org/html/2609.27203#S7)exercise the last row only\. Its permutation\-null threshold is not an extra gate but the holdout arbiter’s own fit threshold, derived per fold from label permutations instead of fixed at a constant; the promotion gates above it belong to the differentiable\-ILP path and are not on that route\.

Table 2:What judges what, on which path: the promotion pipeline of differentiable ILP or the holdout arbiter of[Section6\.5](https://arxiv.org/html/2609.27203#S6.SS5)\. Convergence and supplied held\-out examples are preconditions, not gates: without them the pipeline returns for manual review before any row below runs\.Both paths ride the device\-resident bridge of[Section6\.3](https://arxiv.org/html/2609.27203#S6.SS3)\. Where the trainable rule bodies of[Section6\.4](https://arxiv.org/html/2609.27203#S6.SS4)learn rule*weights*and per\-binding confidences, differentiable ILP learns rule*structure*; the two are complementary\. This sparse, GPU\-resident formulation avoids the cubic blowup of dense rule materialization\. Unlike the trainable\-body surface, this path is not exercised on the benchmark of[Section7](https://arxiv.org/html/2609.27203#S7), and it is a beta subsystem \([Section12](https://arxiv.org/html/2609.27203#S12)\)\.

## 7Learning Event Rules from Perception

The preceding sections build the machinery; this one puts it on an external benchmark\. The task is symbolic event\-rule induction over video surveillance data, and the perceptual predicate the induced rules depend on is itself learned through the logic credit alone, with no perceptual supervision anywhere in the loop\.

The Event Calculus is the standard logical formalism for narrative reasoning over time: a*fluent*is a time\-varying property of the world, for instance that two tracked people aremeeting, and the two event predicatesinitiatedAt\(F,T\)andterminatedAt\(F,T\)say when something at timeTmakes fluentFbegin or makes it stop\. A domain\-independent axiom of inertia closes the loop, so that a fluent*holds at*a time if it was initiated earlier and not terminated since\. Reasoning is therefore cheap and generic once the initiation and termination rules are known; the whole difficulty is obtaining them\.

Those rules are classically hand\-written by a domain expert\. The line of systems that learns them instead, inductive logic programming over Event\-Calculus theories, learns them from a symbolic input vocabulary that somebody else has already computed\. On the CAVIAR video benchmark the learner is handed a relation such asclose\(P1,P2,T\), already reduced from raw tracker coordinates by a hand\-chosen distance threshold, alongside per\-person activity states\. Rule induction thus starts one layer above perception, and the perceptual layer’s quality enters as a fixed input that the learning does not explain\.

In the runs below the proximity predicate is not given\. It isclose\_nn, a small network over the raw pair coordinates, and it is never shown a distance label, a threshold, or any target of its own\. Its only gradient arrives through the induced rules: a candidate clause containingclose\_nnin its body is scored by how well the resulting Event\-Calculus theory explains the frame\-level annotations, and that score is what propagates back to the network’s weights\.

This is the trainable rule bodies of[Section6\.4](https://arxiv.org/html/2609.27203#S6.SS4)on a real benchmark instead of a demonstration: the neural atom sits inside a rule body, and the symbolic literals beside it act as hard join conditions that gate which groundings fire without carrying gradient\. These runs take the engine\-mode credit path of[Section6\.5](https://arxiv.org/html/2609.27203#S6.SS5): the rule learner’s own negative log\-likelihood is the network’s loss, so structure search and weight training are one differentiable object rather than two pipelines in sequence\. The compiled route of[Sections6\.4](https://arxiv.org/html/2609.27203#S6.SS4)and[6\.3](https://arxiv.org/html/2609.27203#S6.SS3), with its machine\-checked equivalence certificate and its zero\-copy DLPack export, is the one the MNIST\-addition measurements of[Section10](https://arxiv.org/html/2609.27203#S10)exercise;close\_nnhere is trained by a different route\.

### 7\.1Protocol

Two targets are searched throughout this section\. The*direct*target asks, per timestep, whether the fluent holds; the*Event\-Calculus*target asks when it is initiated and terminated, and infers holding through inertia\. They carry different class balances, and the guarantees below are stated per target\. Except where a table says otherwise, F1 is micro\-averaged over pooled per\-fold counts, as the published evaluations compute it\.

Each guarantee below was fixed before the run it governs and covers that run alone: the corpus was already in hand while the gates were being designed\.

Leak\-free scene\-family splitting\.The distributed CAVIAR corpus used by the published Event\-Calculus learners is a dump of 26 video segments, and it is not clean\. A frame\-level audit of everymeetingtransition event in the dump against the original ground\-truth XML classifies 21 of 25 events as real, 3 as duplicates and 1 as a splice artifact\. Two source videos appear in both the dump’s train and its test file, and one video alone contributes 855 duplicated gold pair\-frames\. Cross\-validating over segments therefore permits same\-scene transfer\. The clean protocol folds over*scene families*recovered from the source XML instead, so no scene appears on both sides of a split\.

Recall\-aware holdout\.Scoring candidates by held\-out accuracy is useless at this class balance \(roughly ten positive transitions against tens of thousands of rows\), because every candidate sits on the all\-false base\-rate plateau, and the ranking provably inverts: the best real detector scores below the empty theory\. Candidate selection in the Event\-Calculus searches uses per\-fold held\-out F1 instead\. The direct per\-timestep target does not have this problem, since it carries thousands of positives per fold and not a handful of transition events, so its searches are left at their defaults, held\-out accuracy with a fixed0\.750\.75fit gate\. This guard and the next therefore govern the Event\-Calculus route only\.

Permutation\-null fit gate\.A candidate must beat what label shuffling alone achieves on its own fold\. Each fold derives its own threshold from 1000 label permutations \(seed 7\) as the 95th percentile of the pool\-maximum mean per\-fold F1, computed per target and on the training side only\. A theory whose clauses do not clear that bar is not returned: the search abstains and reports an empty theory\. Abstention is a first\-class outcome of this protocol\.

Two fold structures\.The direct per\-timestep runs reuse the three folds the distributed dataset file ships, whose datapoints are fixed\-length windows of consecutive frames for one person pair \(the*windowed folds*\); the Event\-Calculus runs fold over whole video segments, or over scene families under the clean protocol\.

### 7\.2Results

Perception learned through logic credit\.On the windowed\-fold protocol with a direct per\-timestep target, the search finds the same two\-clause theory on every fold in both modes \(\):

holdsAt\_meeting\(PP,T\):\-both\_inactive\(PP,T\),close\*\(PP,T\)\.

holdsAt\_meeting\(PP,T\):\-both\_active\(PP,T\),close\*\(PP,T\)\.

Listing 12:The two\-clause theory the search returns on every fold, in both the relational and the neural mode\.whereclose\*is the precomputed geometric predicate in the relational mode and the learnedclose\_nnin the neural mode\. Held\-out F1 per fold is0\.9215/0\.6804/0\.76950\.9215/0\.6804/0\.7695with the precomputed predicate \(mean0\.79050\.7905\) and0\.9215/0\.7918/0\.76950\.9215/0\.7918/0\.7695with the learned one \(mean0\.82760\.8276\)\. The learned detector matches the precomputed predicate’s result exactly on two folds and outperforms it on the third, where a soft learned boundary survives the train/test geometry shift better than a hard threshold\. That is this section’s main positive result: a perceptual predicate trained through nothing but symbolic credit stands in for hand\-set geometry without loss, and rests on no published comparison\.

Protocol\-matched cross\-validation\.Under the full Event\-Calculus target, the combined 26\-segment corpus \(32,360 co\-visible pair\-frames, 1,833 goldmeetingframes\) was cross\-validated ten\-fold by video segment with every gate re\-derived inside each fold\. The result is precision0\.65800\.6580, recall0\.82710\.8271, F10\.73290\.7329\. The same initiation clause,both\_active & close, is selected on all ten folds, each time over that fold’s own permutation null; the termination theory is empty on all ten, so the fluent persists by inertia to the end of each co\-visible pair\-run\.

Published figures on the same corpus\.This protocol matches the published Event\-Calculus learners on the axis that matters most for the metric: F1 is computed onholdsAtinferred through inertia, on the same distributed corpus, with the same micro\-aggregation\. The published figures formeetingon that corpus are0\.7350\.735for hand\-crafted rules,0\.7820\.782and0\.7920\.792for OLED\[[21](https://arxiv.org/html/2609.27203#bib.bib9)\]\(the latter as reported by its authors, the former as re\-run in the WOLED paper\[[22](https://arxiv.org/html/2609.27203#bib.bib10)\]\) and0\.8870\.887for WOLED\-ASP; they are tabulated beside ours in[Section10](https://arxiv.org/html/2609.27203#S10)\. Ours sits just under that group’s lowest figure\. We draw no ordering from any of these differences, in either direction\. Five protocol deltas separate the rows and they do not all point the same way: the fold structure, the scope of the learned theory, the body\-length limit and the way the reported settings were chosen all differ, and the shared metric is the only reason the comparison is drawn at all\.[Table11](https://arxiv.org/html/2609.27203#S10.T11)prints the five deltas in full beside the figures\.

A second vocabulary iteration\.Two pair\-level transition relations were added to the Event\-Calculus vocabulary, one for a pair crossing the proximity threshold outward and one for strictly growing distance, and the identical folds, seeds and gates were re\-run\. The result rises to precision0\.73570\.7357, recall0\.82600\.8260, F10\.77820\.7782\(1514 true positives, 544 false positives, 319 false negatives\), with a termination theory now learned on seven of the ten folds\. That figure falls inside the0\.7350\.735–0\.8870\.887span the published systems occupy, but it must never be read as the headline: its vocabulary was chosen*after*the first run’s test\-side failure mode was known, on the same folds\. Everything else about it is pre\-registered; the vocabulary is not\. Against published estimates selected as the best of several tried, the smaller number declared in advance is the stronger scientific claim, which is why it leads here and0\.77820\.7782appears only with this label attached\.

The learned detector under the Event\-Calculus target\.Substituting the learnedclose\_nndetector for the precomputed proximity predicate inside the Event\-Calculus initiation search does not survive cross\-validation: precision0\.12500\.1250, recall0\.00050\.0005, F10\.00110\.0011over the same ten folds \([Table12](https://arxiv.org/html/2609.27203#S10.T12)gives the counts\)\. Only one fold commits a clause, the sameboth\_active & close\_nnshape the geometric predicate selects there, and probed directly against held\-out ground\-truth proximity that clause scores precision1\.01\.0at recall0\.270\.27, so the network has learned the geometric relation\. The failure is one of scale in the selection rule, not of perception: the initiation search scores coverage against transition*events*, a handful per fold, and a probability\-thresholded gate newly covers fewer of them than a deterministic predicate does, so nine of ten folds reject the candidate for insufficient new coverage\.

The leak\-free protocol\.Re\-run on the deduplicated, scene\-family\-grouped corpus, themeetingfluent yields F10\.00\.0on both routes, and mostly by committing a rule that earns nothing rather than by declining to commit one\. The direct route selectsboth\_inactive & closeon nine of the ten folds, and that clause returns no true positive anywhere \(0 tp, 106 fp, 1,812 fn\)\. The Event\-Calculus route commitsboth\_active & closeon one fold, whose 120 false positives are its entire error mass \(0/120/1,812\), and abstains on the other nine, recording insufficient new coverage or an abstaining selector; its termination search returns nothing on any fold, most often because no body passed that fold’s fit gate\. Both routes produce false positives, which an empty theory cannot: the search ran, and what failed is transfer\.

The reason is visible in the data\. One scene family carries 1,323 of the 1,812meeting\-positive frames and, under honest grouping, sits in exactly one fold; the clause that explains those frames holds*only*there, covering zero of the 489 positives on all eight remainingmeeting\-bearing segments\. Both outcomes follow from that\. Where the clause is committed, it is committed on a training side that contains the concentrated family, and it covers nothing outside it\. The one fold on which the direct route abstains is precisely the fold that holds that family out, leaving a training side on which the clause covers 0 of 489 positives and 106 negatives\.

Where the gate abstains, it is because the candidate’s held\-out score has collapsed for the same reason\. The statistical bar itself did not rise: the per\-fold null thresholds under this protocol are essentially those of the like\-for\-like distributed\-corpus run\. Training with the family learns a clause that transfers nowhere; training without it cannot learn the clause at all\. With eleven observablemeetinginitiations and fivemovingones, the clean corpus does not carry enough evidence for a cross\-validated theory in either direction\.

The machinery is not broken under this protocol\. Onmovingthe direct route still selects the canonical published rule shape on nine of ten folds \(micro F10\.44500\.4450\), and themeetingclause applied to the concentrated family’s own fold, an in\-family fit and not a transfer test, scores frame F10\.8900\.890there\. What it establishes is narrower and more specific than an abstention: a two\-literal state vocabulary does not carry CAVIARmeetingacross scene families at all\.

Table 3:Runs reported in this section\. Micro F1 over pooled per\-fold counts, except the windowed rows, which are fold means\. The*\+ termination relations*row is the second, adaptive vocabulary iteration\. The clean\-protocol zeros are scored predictions, not empty theories, except themovingEvent\-Calculus row, whose initiation theory is empty on every fold; the census behind them is in the text\. Published figures for the same benchmark are tabulated separately in[Section10](https://arxiv.org/html/2609.27203#S10)\.### 7\.3Discussion

Two of the findings above concern the method\. A perceptual predicate can be learned end\-to\-end through symbolic credit alone and stand in for hand\-set geometry without loss on a real benchmark\. And Event\-Calculus rules can be induced under fully pre\-registered gates and land within a couple of points of the range published Event\-Calculus learners report on the corpus they share\.

The other two concern that corpus\. It carries a measurable duplication defect, and under a leak\-free split of it the inducedmeetingrule does not transfer: the search still commits the canonical clause on most folds, and that clause scores zero out of family\.

None of this ranks the system against the published learners \([Section12](https://arxiv.org/html/2609.27203#S12)\)\. Termination programs are not learned in the pre\-registered run either, and the empty termination theory is the dominant source of false positives there\. Nor is the learned detector a drop\-in replacement for the geometric predicate everywhere: under Event\-Calculus cross\-validation it is not\. And it is one benchmark in one domain\. What the section does show is that the structure search and the perception underneath it can be one differentiable object instead of two systems in sequence\.

## 8Rule Induction at Scale: Maritime Rendezvous

The previous section ends on an evidence problem: under a leak\-free split CAVIAR carries eleven observablemeetinginitiations, too few for a cross\-validated claim about rule learning\. This section moves the same machinery to the other public corpus the Event\-Calculus learners report on, the Brest AIS maritime stream\[[31](https://arxiv.org/html/2609.27203#bib.bib11),[29](https://arxiv.org/html/2609.27203#bib.bib12)\], whose target fluentrendezVous\(two vessels close together, stopped or moving slowly, in open water\) carries 3,548 gold intervals\.

It is large enough to separate three questions CAVIAR could not\. Does a*crisp*rule search, selecting clauses that each fire with weight one as in[Section7](https://arxiv.org/html/2609.27203#S7), land where the declared ceiling says it will? How much is gained by*weighting*the clauses of the same gated pool instead of selecting them? And what does it cost to learn those weights in one chronological pass over the stream? The six runs of[Table5](https://arxiv.org/html/2609.27203#S8.T5)answer them, covering the published systems’ three training settings: enumerated rule search, weighted clauses, single\-pass weight training\.

Two of the three answers came out better than we expected\.

### 8\.1Corpus and labels

The inputs are two public exports of RTEC\[[3](https://arxiv.org/html/2609.27203#bib.bib13)\], a hand\-written Event\-Calculus rule engine, over the Brest AIS stream: the composite events it recognised \(Zenodo record 2557290\) and its own input, the*critical points*of the compressed trajectories\[[29](https://arxiv.org/html/2609.27203#bib.bib12)\], the timestamps at which a vessel stops, turns, changes speed or loses signal\. Those points are the only temporal grid the corpus carries\. A deterministic converter reduces the two into a*pair\-time corpus*: one row per \(vessel pair, timestamp\), eleven relations that hold or do not for that pair then, and the gold label\.[Table4](https://arxiv.org/html/2609.27203#S8.T4)sizes it\. The conversion uses no randomness: the corpus is a pure function of the archives\.

Table 4:The pair\-time corpus, as the converter leaves it\. The negative pairs are drawn by fixed stride from the2,0142\{,\}014pairs that come within proximity but carry no interval\.Three properties bound what a number measured on it can mean\. The supervision is synthetic: the gold labels are a hand\-crafted RTEC rule’s output over the same interval streams the vocabulary comes from, so their perfect alignment with those streams says the conversion is faithful, not that the labels are right\. The published learners share this regime; the WOLED paper notes that the maritime ground truth is synthetic and its learning curves consequently alike\[[22](https://arxiv.org/html/2609.27203#bib.bib10)\]\. What every system here measures is the*reconstruction of a known rule*under a vocabulary that does not contain all of it\.

The vocabulary is incomplete by construction\. Its eleven pair\-time relations \(proximity,both\_lowspeed,both\_stopped\_far,both\_open\_sea,became\_proximate, and so on\) omit the gold rule’s two remaining discriminators, its240240s minimum\-duration threshold and its exclusion of tug and pilot pairs, so perfect reconstruction in the base vocabulary is impossible\.

And the grid is sparse:≈1\.009\{\\approx\}1\.009positive rows per gold interval, the covering row almost always the interval’s start boundary, so pointwise and interval F1 coincide here \([Section8\.4](https://arxiv.org/html/2609.27203#S8.SS4)\)\.

### 8\.2Protocol

Metric\.The primary metric is pointwise F1 on the positive class, F1 over individual rows, never accuracy, which the empty predictor saturates here\. Interval figures accompany it, a gold interval counting as matched when a predicted row falls inside it in the same episode of the pair’s timeline, and symmetrically\.

The declared ceiling\.Each run’s hypotheses and parameters were fixed before it was executed, beginning with the ceiling the base vocabulary imposes\. The gold rule’s definitional body isproximity & both\_low\_or\_stopped & both\_open\_sea, the middle literal being the disjunction ofboth\_lowspeedandboth\_stopped\_far; all three are in the vocabulary, so the body is expressible either way\. It reaches recall1\.01\.0at pointwise precision≈0\.49\{\\approx\}0\.49, hence F1≈0\.66\{\\approx\}0\.66: the two inexpressible discriminators are exactly what separate its false positives from its true ones\.

A direct evaluation of that body on the archives, the*ceiling probe*, hits the operating point exactly: F10\.65990\.6599, no false negative \([Table6](https://arxiv.org/html/2609.27203#S8.T6)\)\. It also decomposes them:733733in negative pairs, the pair\-exclusion class,2,9562\{,\}956in predicted runs shorter than240240s, and*none*outside the two pre\-identified discriminators\.

Folds are vessel pairs\.A pair’s rows are never split across folds, because the positive mass is concentrated: the top pair carries33\.4%33\.4\\%of all positive rows and the top four60\.2%60\.2\\%, so a finer split would leak the dominant encounter across the boundary\. The protocol uses five folds where CAVIAR uses ten, assigned by a deterministic greedy longest\-processing\-time rule with no seed, stratified by positive mass, none differing from another by more than the largest pair’s count\. The consequence is stated openly: held\-out fold 0 is the top pair plus one negative pair, so per\-fold figures are necessarily unequal and the micro number never stands alone\.

Search and gate as on CAVIAR\.The crisp run uses the relational sequential\-covering search of[Section7](https://arxiv.org/html/2609.27203#S7)under the CAVIAR limits: bodies of at most three literals, at most four clauses, per\-fold held\-out F1 for candidate selection, at least two newly covered positives per clause\. Its permutation\-null fit gate is the CAVIAR one:1,0001\{,\}000label permutations per fold, threshold at the9595th percentile of the pool\-maximum per\-fold F1, derived on the training side\. One seed,77, drives the permutations and the candidate\-selection holdout\. The target is the direct per\-row positive label; induction through inertia is out of scope here, with almost no interior rows to fill\.

Weights\.The weighted runs keep vocabulary, folds and gate, replacing crisp selection with weights\. The body pool is every conjunction of one to three literals passing the same per\-fold permutation\-null procedure, thresholds re\-derived per run, each body carrying one weight\. A row’s score is the noisy\-OR1−∏c\(1−σ⁡\(wc\)​coverc\)1\-\\prod\_\{c\}\\bigl\(1\-\\sigma\(w\_\{c\}\)\\,\\mathrm\{cover\}\_\{c\}\\bigr\)of[Section6\.4](https://arxiv.org/html/2609.27203#S6.SS4), every clause purely relational, trained by binary cross\-entropy with Adam and thresholded at0\.50\.5:300300steps at learning rate0\.050\.05from every weight at−2\.0\-2\.0, so every clause starts switched off \(σ⁡\(−2\)≈0\.12\\sigma\(\-2\)\\approx 0\.12\)\. The single\-pass variants replace that optimisation with*one*pass over the fold in ascending global time, its pairs interleaved as in a stream, in mini\-batches of1,0001\{,\}000rows, one Adam step per batch, at the same rate\. Adam is kept instead of WOLED’s AdaGrad, so exactly one variable separates the regimes\. Pool and gate are still computed on the training side, which makes this single\-pass*weight*learning, semi\-online in that only the weights see the stream; the structure is never learned online\.

### 8\.3Results

Crisp search on the base vocabulary\.The first run is the CAVIAR search unchanged\. It lands where the ceiling mechanism predicted, precision near one half at recall near one, for micro pointwise F10\.6746\\mathbf\{0\.6746\}\([Table5](https://arxiv.org/html/2609.27203#S8.T5)\)\.

On every fold it commits both disjunctive branches of the gold body:both\_open\_sea & both\_stopped\_far & proximityandboth\_lowspeed & both\_open\_sea & proximity\. Three folds add a further clause, on two of them the subsuming disjunction relation itself\. No clause is ever accepted below its fold’s null gate\.

The learned operator is not literally the definitional body, its precision being0\.51090\.5109against the body’s0\.49240\.4924, so the evidence is about the mechanism, not operator identity\. The per\-fold spread of[Table6](https://arxiv.org/html/2609.27203#S8.T6)is the pair\-concentration effect: the fold with the top pair’s long clean encounters scores highest, while folds of many small pairs concentrate the duration\-threshold false positives\. Improvement past this run has to come from expressiveness rather than tuning\.

Weighted clauses on the same pool\.The second run changes one thing: the pool’s clauses are weighted rather than selected\. We expected it to stay within\[0\.66,0\.70\]\[0\.66,0\.70\], the ceiling being a property of the vocabulary\.

The hypothesis was rejected in the favourable direction\. Micro F1 is0\.7398\\mathbf\{0\.7398\},\+0\.0652\+0\.0652over the crisp run on the same vocabulary, folds and gate, at markedly higher precision and lower recall; the abstract and[Section1](https://arxiv.org/html/2609.27203#S1)round that gain to0\.0650\.065\.

The expectation was wrong for an instructive reason: the0\.660\.66ceiling is the F1 of the definitional body’s operating point, crisp reconstruction at recall near one, and weights are not confined to it\. Training moved the operating point to high precision at lower recall, which carries more F1\.

Fold by fold the picture is mixed\. The weighted run wins the micro figure and the median but only two of the five folds, and its weakest fold is worse than the crisp run’s\. That weights over the same clauses beat crisp selection of them is the gain the published line attributes to weighting\[[22](https://arxiv.org/html/2609.27203#bib.bib10)\]\.

Both runs again with the duration relation\.The third and fourth runs add one relation,sustained\_240: a row carries it whenproximity∩both\_low\_or\_stopped∩both\_open\_sea\{\\texttt\{proximity\}\}\\cap\{\\texttt\{both\\textunderscore\\hskip 0\.0ptlow\\textunderscore\\hskip 0\.0ptor\\textunderscore\\hskip 0\.0ptstopped\}\}\\cap\{\\texttt\{both\\textunderscore\\hskip 0\.0ptopen\\textunderscore\\hskip 0\.0ptsea\}\}holds continuously through a stretch of at least240240s containing it\. The constant is the gold generator’s own, so the addition is language parity with RTEC, not a look at the data\.

The ceiling probe was re\-run on the widened vocabulary before any cross\-validated run, against an expectation of≈0\.907\{\\approx\}0\.907on the assumption that duration removes only the short\-run false positives\. The ceiling came out higher, at F10\.99690\.9969, again with no false negative\.

Duration also eliminates at least711711of the733733negative\-pair false positives, the excluded pairs’ body\-condition episodes being almost always shorter than240240s\. The bound is a lower one because the2222false positives the widened probe still makes are not decomposed by class\. Two consequences were predicted from that: the pair exclusion is largely redundant with duration here, and the duration vocabulary saturates, so the informative weighted\-against\-crisp comparison is the base\-vocabulary one\.

Both held\. Crisp search on the widened vocabulary lands exactly on the derived ceiling and the weighted run equals it on every fold, so the directional hypothesis, weighted no worse than crisp on the median, holds trivially, with no headroom for weights\.

Weighted clauses learned in a single pass\.The last two runs change only how the second run’s weights are trained, replacing batch optimisation with a single chronological pass\. They use the base vocabulary only:sustained\_240at timettdepends on how long the current interval will last, a leak in a streaming setting, and was excluded before the run\.

Three hypotheses were fixed beforehand: the single pass should lose at most0\.040\.04micro F1 against the batch run, with anything below0\.700\.70a negative result; a*reverse*chronological pass should land within0\.020\.02of the forward one; and the prequential error, scored on each batch before that batch is trained on, should fall along the stream\.

The measured degradation is zero\. The single pass reproduces the batch run’s thresholded predictions exactly: the same counts on every fold and, as re\-scoring with the stored weights confirms, the same decision on every row, at the same micro F1\. The reverse pass is identical as well, and the prequential error falls from the first half of the stream to the second on all five folds in both orders \(forward, fold 0:0\.0078→0\.00360\.0078\\to 0\.0036\)\. Halves are the one criterion of these runs settled as the results were written up instead of before them\.

Identical predictions are a statement about the decision structure, not evidence that the single\-pass path silently fell through to the batch one: the weights themselves differ substantially between the three regimes \([Table5](https://arxiv.org/html/2609.27203#S8.T5)\)\. The mechanism is simpler than robustness to the training regime\. In all fifteen fold\-by\-regime cases exactly one body hasσ⁡\(w\)\>0\.5\\sigma\(w\)\>0\.5, alwaysbecame\_proximate & both\_open\_sea & both\_stopped\_far, and the second\-ranked body stays between0\.150\.15and0\.460\.46, so the noisy\-OR of the others never reaches the threshold on any held\-out row\. All three trainings reduce to the same crisp rule, and the predictions agree because that rule does\.

The agreement is fragile\. The highest score of a row*not*covered by the top body reaches0\.4930\.493in fold 1 under the batch weights,0\.0070\.007below the threshold\.

That fold has1,2701\{,\}270rows between0\.30\.3and0\.50\.5: a small change of learning rate, step count or initialisation could push the second body over and move the counts by hundreds of rows\. The declared scope is narrow\. Prediction identity holds for this pool, corpus and threshold, hangs on the discrete structure of a thresholded decision, and is not a theorem\.

Table 5:MaritimerendezVous: five\-fold cross\-validation over whole vessel pairs, seed 7\. P, R and F1 are pointwise micro\-averages over pooled per\-fold counts; the last column is the median of the five per\-fold values\. The three base\-vocabulary weighted rows are identical row by row, though their weights are not: fold 0’s top body carriesσ⁡\(w\)=0\.6476\\sigma\(w\)=0\.6476in batch,0\.58800\.5880in the forward pass and0\.83980\.8398in the reverse, and theL∞L\_\{\\infty\}distance between the logit vectors of any two regimes is1\.061\.06–2\.952\.95\. Interval\-level F1: 0\.6772 \(crisp, base; 3,545 of the 3,548 gold intervals matched\), 0\.7435 \(weighted, base\), 0\.9970 \(both duration rows\)\. No published figure appears here \([Section8\.4](https://arxiv.org/html/2609.27203#S8.SS4)\)\.Table 6:Per\-fold F1 on the base vocabulary and the pooled counts behind[Table5](https://arxiv.org/html/2609.27203#S8.T5)\. The three weighted regimes share a row because their predictions are identical\. The probe rows evaluate the gold rule’s definitional body directly; the duration probe’s2222residual false positives are what its0\.99690\.9969ceiling reflects\.
### 8\.4Discussion

The published figure forrendezVouson this corpus is0\.980\.98for OLED and both variants of WOLED, MLN\- and ASP\-based alike, with theories of eighteen literals, measured on a train/test split of halves\[[22](https://arxiv.org/html/2609.27203#bib.bib10)\]\. A second published experiment, on a six\-sequence fragment, compares WOLED\-ASP with batch learners and reports figures from0\.910\.91to0\.970\.97in a bar chart\. None of them stands beside the rows of[Table5](https://arxiv.org/html/2609.27203#S8.T5), because the two sets of numbers are not on one axis\.

Theirs live on a dense grid, the critical points of every vessel with inertia filling each interval’s interior\. Ours live on the sparse per\-pair grid the converter produces, and we do not reproduce the published per\-timepoint reading on it\. A split of halves is not a pair\-level five\-fold cross\-validation either, and for the same reason we do not compare pass times with published training times\.

What is comparable is comparable in kind only\. The published systems saturate on their preprocessing of the same stream, and ours too once the duration discriminator is expressible, at the declared ceiling\. And the gain the published line reports between OLED and WOLED on CAVIAR, and attributes to weighting, is reproduced here as\+0\.0652\+0\.0652micro F1 with everything else held fixed, on a corpus with3,5483\{,\}548gold intervals instead of eleven events, and again without loss when the weights are learned in one pass\.

Within those bounds the findings are concrete\. The crisp search reconstructs the gold body on every fold of a corpus two orders of magnitude richer in positive events, and lands on the declared ceiling\. Weighting the same pool adds0\.06520\.0652micro F1 and0\.03320\.0332to the median against the expectation declared for it, on two folds of five\. Duration saturates both search modes and makes the pair exclusion largely redundant\. And single\-pass weights reproduce the batch predictions exactly, for the reason named above\.

No ranking against OLED or WOLED onrendezVousfollows from any of it \([Section12](https://arxiv.org/html/2609.27203#S12)\)\. Nor does it say anything about detecting rendezvous in the wild: every number here is a rule\-reconstruction figure\. It does not demonstrate online structure learning, the pool and gate being computed on the training side, nor a general robustness of thresholded noisy\-OR predictors to the training regime\. And it exercises none of the GPU substrate: every run here is a deterministic CPU procedure\.

What it does show is that the induction protocol of[Section7](https://arxiv.org/html/2609.27203#S7), its declared gates, pair\-level folds and permutation nulls, carries intact to a corpus where its verdicts are measurements and not anecdotes\. There, weighted clauses and single\-pass training, the two mechanisms the published line rests on, are measured in isolation and behave as their authors report\.

## 9Epistemic and Other Reasoning Modes

The substrate generalizes beyond what is*true*or*probable*\. This section covers three further modes that reuse the same CUDA join, circuit, and CDCL machinery \(epistemic reasoning over world views, probabilistic aggregates, and well\-founded semantics\) broadening what a neural network can be integrated with while keeping data\-plane execution GPU\-backed\.

### 9\.1Modal surface and the epistemic IR

Epistemic logic programming asks what is*known*or*possible*across the multiple stable models a program admits—the natural setting for introspection and reasoning under incomplete knowledge\. A program may use four modal literals over a predicate:know,possible,not know,not possible\. Instead of rewriting them away at parse time, the compiler preserves them in an Epistemic IR \(EIR\) between the AST and execution planning\. The high\-level dispatcher classifies modal dependencies before selecting Generate–Propagate–Test, a mode\-specific positive\-cycle fixpoint, or GPU\-backed WFS\. The accepted surface spans finite nested modal chains, epistemic integrity constraints \(which prune candidate world views on the GPU\), rules that couple several epistemic predicates, same\-name multi\-arity modal predicates, and recursive epistemic execution\.

### 9\.2World\-view semantics

A world view is a non\-empty set of stable models\.know pholds whenpappears in every model of the world view;possible pholds when it appears in at least one\. Two semantics are selectable\. Under the default FAEEL \(Founded Autoepistemic Equilibrium Logic\), a circular derivation contributes a tuple only when independent founded support exists\. A program containing onlyp :\- possible p\.therefore executes to an empty founded extension instead of failing with an unsupported\-construct diagnostic\. A Gelfond\-1991\-style compatibility mode admits that self\-supporting tuple\. Non\-epistemic programs evaluate identically under both\.

### 9\.3Epistemic execution routes

After EIR construction, acyclic modal programs follow a Generate–Propagate–Test schedule whose phases run as CUDA kernels\.*Generate*enumerates bounded candidate assumptions as device bitsets;*propagate*prunes candidates that contradict known or rejected facts;*test*validates survivors against the program’s world views, checking stable\-model tuple membership on\-device per arity\. Validating a candidate on this route reuses the on\-GPU CDCL solver already built for compilation verification \([Section5](https://arxiv.org/html/2609.27203#S5)\), the same substrate that serves satisfiability, bounded MaxSAT and assumption\-based queries, and accepted world\-view evidence feeds the existing GPU\-native exact path\.

A positive FAEEL dependency cycle reduces to ordinary rules and reaches the founded least fixpoint in the existing recursive engine\. A supported Gelfond\-1991 cycle, whose selected positivepossiblegates must use their rule heads’ own terms and stay within one recursive dependency component, instead descends to the greatest compatible set: the runtime relaxes those gates for an upper bound and then reevaluates until GPU set comparison over the intensional relations reports no further change \([Section12](https://arxiv.org/html/2609.27203#S12)\)\. Supported cycles through negation take the GPU\-backed WFS alternating fixpoint instead, and recursive negation or aggregation inside a compatibility component is rejected, because either would make the descending operator nonmonotone\.

The reduced ordinary work reuses the optimizer, WCOJ planner and helper\-splitting machinery of[Section4](https://arxiv.org/html/2609.27203#S4), and*epistemic splitting*decomposes eligible acyclic programs into independent components solved separately and recombined\. No CPU fallback is provided for the accepted data\-plane hot paths: a construct these routes do not support is rejected with a typed error; no host implementation serves it\. Transfer budgets track data movement; the host sequences Gelfond\-1991 refinement and WFS iterations, while relation evaluation, snapshot copies and convergence comparisons remain GPU\-backed\.

### 9\.4Probabilistic aggregates

Finite aggregate queries \(count,sum,min,max,logsumexp\) are supported in both exact provenance/PIR inference and Monte Carlo execution, subject to a typed exact\-domain cap that rejects domains too large for tractable enumeration\. For small finitecountdomains,*aggregate lifting*replaces naive world enumeration with exact cardinality dynamic programming over a compact state set \(collapsing, for example, a2172^\{17\}\-outcome enumeration into a few hundred lifted states with identical results\) and acceptedcountaggregates dispatch a GPU\-native exact evaluator rather than a CPU finite\-world shortcut, keeping the path device\-resident\.

### 9\.5Well\-founded semantics

Programs that violate stratification, such as the classicp :\- not q\. q :\- not p\., do not have a unique two\-valued least\-fixpoint interpretation\. For supported shapes, xlog instead assigns three\-valued truth \(true, false, undefined\) through well\-founded semantics, computing an alternating fixed point: mark the greatest unfounded set false, derive consequences true, and repeat until stable\. For probabilistic programs, true atoms receive normal probability and gradient while false and undefined atoms are assigned probability zero, matching the conservative treatment of non\-stratified programs\. Probabilistic provenance analysis and epistemic dependency dispatch select the GPU\-backed WFS route for the nonmonotone components they support; other cyclic shapes return a typed diagnostic\.

## 10Evaluation

This section reports measurements for xlog’s deterministic, probabilistic, and neural\-symbolic subsystems\. The subsystem measurements in[Sections10\.2](https://arxiv.org/html/2609.27203#S10.SS2),[10\.3](https://arxiv.org/html/2609.27203#S10.SS3)and[10\.7](https://arxiv.org/html/2609.27203#S10.SS7)are*single\-system ablations of xlog against its own baselines*: the first two on development hardware, the runtime\-optimization pair on a cloud GPU that the artifact names\.[Section10\.4](https://arxiv.org/html/2609.27203#S10.SS4)then adds controlled head\-to\-head comparisons against external engines \(Scallop, ProbLog2, Soufflé\),[Section10\.5](https://arxiv.org/html/2609.27203#S10.SS5)tabulates the Event\-Calculus rule\-induction runs of[Section7](https://arxiv.org/html/2609.27203#S7)beside the figures published for the same benchmark and states why the maritime runs of[Section8](https://arxiv.org/html/2609.27203#S8)are not tabulated beside theirs, and[Section10\.6](https://arxiv.org/html/2609.27203#S10.SS6)isolates xlog’s two design costs, verification and residency, from ordinary GPU acceleration\.[Section10\.9](https://arxiv.org/html/2609.27203#S10.SS9)describes three further runtime capabilities for which no timing is claimed\.

### 10\.1Methodology

The subsystem ablations were collected on an NVIDIA RTX PRO 3000 \(Blackwell, 12 GB VRAM, compute capability 12\.0\)\. The head\-to\-head comparisons of[Section10\.4](https://arxiv.org/html/2609.27203#S10.SS4), the overhead isolations of[Section10\.6](https://arxiv.org/html/2609.27203#S10.SS6)and the runtime\-optimization ablations of[Section10\.7](https://arxiv.org/html/2609.27203#S10.SS7)ran on cloud GPUs, as stated with each, and the neural Event\-Calculus runs of[Section10\.5](https://arxiv.org/html/2609.27203#S10.SS5)on an NVIDIA A40\. Each cloud artifact records its own device, driver and CPU quota\. For the seven head\-to\-head and overhead artifacts, a number that differs from an earlier version of the same artifact differs because of the machine: those seven were all measured on one engine build\. That does not extend to the two runtime\-optimization fixtures of[Section10\.7](https://arxiv.org/html/2609.27203#S10.SS7), whose earlier records date from the v0\.8\.6 campaign, so both the hardware and the engine version changed between them\. The relational searches of[Section10\.5](https://arxiv.org/html/2609.27203#S10.SS5)and[Section8](https://arxiv.org/html/2609.27203#S8)are deterministic CPU procedures whose results do not depend on the host; the weight trainings beside them run on CPU as well\. Rust crates are built in release mode; CUDA modules are staged cubin\-first with PTX fallback and explicit JIT warm\-up; Python components usepyxlogwith CUDA\-enabled PyTorch\. The benchmark harness uses Criterion\.rs with the settings in[Table7](https://arxiv.org/html/2609.27203#S10.T7), and GPU measurements include warm\-up to amortize kernel\-module loading and CUDA context setup\.

Per\-run measurement data is distributed with the paper for the head\-to\-head comparisons and overhead isolations, the circuit\-cache ablation, the runtime\-optimization ablations of[Section10\.7](https://arxiv.org/html/2609.27203#S10.SS7), and every rule\-induction run of[Sections7](https://arxiv.org/html/2609.27203#S7)and[8](https://arxiv.org/html/2609.27203#S8)\. Each other figure below is stated together with the fixture, protocol and aggregation that produced it\.

Table 7:Benchmark harness settings\.
### 10\.2WCOJ vs\. the binary\-join plan

This ablation asks how much the worst\-case\-optimal join path of[Section4](https://arxiv.org/html/2609.27203#S4)saves over xlog’s own binary\-join plan on the skewed cyclic query the subsystem exists for\. The query is a single three\-way triangle join, the classic worst\-case\-optimal pathology;[Table8](https://arxiv.org/html/2609.27203#S10.T8)gives the fixture and the timing protocol\.

The keys are generated by four fixture variants named for the workloads they stand in for \(call\-graph edges, Andersen points\-to\[[1](https://arxiv.org/html/2609.27203#bib.bib29)\],ddisasm\-style disassembly\[[17](https://arxiv.org/html/2609.27203#bib.bib30)\], and a neural\-symbolic mining analog\) whose size parameters coincide at this scale, so the four cells are repeats of one workload and not four distinct ones\. What the fixture does establish is skew: every join variable has a small hot domain, so the binary\-join plan materializes an intermediate far larger than the final result, which is the regime WCOJ exists to address\. WCOJ speedups depend strongly on input size and skew, and synthetic fixtures systematically overstate them, this one included, so the ratio below is the gain on the shape the subsystem targets, at this scale\.

Table 8:Triangle\-join fixture and timing protocol for the WCOJ ablation\.[Figure4](https://arxiv.org/html/2609.27203#S10.F4)reports the speedups: a27\.96×27\.96\\timesgeometric mean, with the four cells spanning26\.6×26\.6\\timesto29\.6×29\.6\\times\. Since the variants coincide at this scale, that spread measures run\-to\-run variation and not robustness across distinct workloads\.[Section10\.4](https://arxiv.org/html/2609.27203#S10.SS4)reports the external counterpart, a fused\-counting comparison against Soufflé at millions of tuples\.

Figure 4:WCOJ vs\. binary\-join speedup on the four key\-generation variants of the triangle fixture \([Table8](https://arxiv.org/html/2609.27203#S10.T8)\)\. Single\-system ablation; the dashed line is the geometric mean\.On uniform or empty inputs the adaptive classifier selects the binary\-join chain\.

### 10\.3Circuit caching and training

This ablation asks how much of neural\-symbolic training time circuit caching \([Section5](https://arxiv.org/html/2609.27203#S5)\) removes by amortizing D4 compilation across epochs\. Training is measured on MNIST single\-digit addition;[Table9](https://arxiv.org/html/2609.27203#S10.T9)carries both the full\-run timing, in which the first epoch pays cold\-start compilation and verification while warm epochs run only the cached forward/backward kernels, and the cache ablation beside it\.

The ablation is a separate experiment from the full run: its uncached arm recompiles the circuit every epoch while its cached arm compiles once, so it isolates compilation amortization, and the apparent speedup therefore grows with epoch count toward the cold/warm ratio instead of being a fixed property\. The 512\-image protocol isolates cold/warm compilation timing and is deliberately under\-trained \(near\-chance accuracy\); held\-out accuracy is measured at scale in the Scallop head\-to\-head \([Section10\.4](https://arxiv.org/html/2609.27203#S10.SS4)\), where the same pipeline reaches≈95%\{\\approx\}95\\%\.

Table 9:MNIST\-addition training summary\. The timing rows come from a 512\-image, 5\-epoch training run at batch size 64; the ablation rows come from a separate experiment \(512 images, 3 epochs, 3 seeds\), whose speedup is the mean of its three per\-seed ratios, not the ratio of its means\.
### 10\.4Head\-to\-head comparisons

[Table10](https://arxiv.org/html/2609.27203#S10.T10)reports controlled comparisons against external engines, one per reasoning mode, on cloud GPUs \(A100 80GB and L40S\), with matched programs, data and metrics\. Each artifact records the pod’s CPU quota alongside its GPU, because that quota is what the CPU baselines are given:26\.3526\.35cores for Soufflé here, against7\.657\.65in the previous measurement of the same comparison\. xlog wins where its GPU\-resident, bounded\-memory design is the point, and does not where a mature CPU compiler is already fast enough on small inputs\.

Table 10:Head\-to\-head comparisons: one external engine per reasoning mode, matched programs, data, metrics and seeds, on cloud GPU pods\. The correctness and all\-arm completeness gates pass for every comparison\.Neural\-symbolic: MNIST addition vs\. Scallop\.With identical MNISTNet, data, metric and seeds, xlog and Scallop reach comparable held\-out accuracy:0\.9561±0\.00080\.9561\\pm 0\.0008against0\.9468±0\.01040\.9468\\pm 0\.0104on the 20k protocol, and both near chance on the under\-trained 512\-image protocol\. The two systems reach that accuracy by different routes: Scallop scores each fact through a bounded set of proof clauses, while xlog evaluates the exact weighted model count of the compiled circuit on every step\.*We make no per\-epoch speed claim on this comparison\.*Scallop’s steady epoch is not monotone in the pod’s CPU quota —31\.7931\.79s at13\.613\.6cores and54\.9954\.99s at27\.227\.2on the same card, the same wheel and the same seeds — so an xlog/Scallop epoch ratio measured on any one host reports that host as much as either engine\. Establishing the ratio would take that curve measured across quotas; the accuracies above stand independently of it\.

Probabilistic: exact inference vs\. ProbLog2\.On five programs \(a conditioned Bayesian fragment and probabilistic reach chains\) xlog’s exact query probabilities match the analytic answers to zero error, identical to ProbLog2 \(correctness gate\|Δ\|<10−4\|\\Delta\|<10^\{\-4\}\)\. On timing, however, xlog is*not*competitive on these small programs\. Its per\-query time is flat, a fixed GPU launch plus a per\-call D4 compile and CDCL verify, while ProbLog2’s mature CPU compiler runs each query4545–100×100\\timesfaster\. We therefore make no exact\-inference*speed*claim; the probabilistic contribution is correctness\-equivalent inference with a CUDA\-resident circuit data plane and certification of the final smoothed circuit\. The host orchestrates the route and observes bounded solver control state, and its fixed costs amortize only at scale or under repeated evaluation\.

Deterministic: WCOJ triangle counting vs\. Soufflé\.On hub\-skewed graphs, xlog’s fused worst\-case\-optimal triangle counting, xlog’s enumerate\-then\-count diagnostic, and Soufflé produce the same per\-root triangle totals at every size\. The comparison uses the median of three full\-process executions after one\-time native builds: a standalone Soufflé executable is generated once per case with twenty\-six jobs, matching the pod’s CPU quota, and its13\.0513\.05–13\.5613\.56s compilation is recorded separately\.*The defensible claim is how the ratio moves with input size\.*Relative to fused xlog execution, compiled Soufflé is0\.88×0\.88\\times,1\.96×1\.96\\times,2\.59×2\.59\\times,3\.88×3\.88\\timesand5\.54×5\.54\\timesacross150150k to1\.21\.2M edges: on the smallest graph Soufflé is the faster of the two, and xlog only overtakes it from300300k edges on\. What holds monotonically is that the ratio grows with the input, because xlog’s execution time is nearly flat \(0\.570\.57–0\.680\.68s\) while Soufflé’s grows linearly \(0\.510\.51–3\.773\.77s\)\. That flatness needs a caveat the artifact supplies: the engine’s own counting time is2525–4343ms of it, so between9393and96%96\\%of the xlog wall time here is process start, CUDA context creation and Arrow input\. What is flat at these sizes is the fixed cost, and the engine time is small enough that this comparison does not resolve how it scales\. Fused counting never materializes the triangles and its peak device allocations are8585to1,0331\{,\}033MB, while enumerate\-then\-count peaks at3,2873\{,\}287to44,97944\{,\}979MB\. All arms complete, both cross\-system count checks pass, and the all\-arm comparison gate is therefore true\. This supports bounded intermediates on these skewed, large\-intermediate workloads, not a universal Datalog speed claim: native compilation time is excluded from the execution medians, the measurements are hardware\-specific and quota\-specific, and on moderate skew the advantage over xlog’s own binary join is2\.002\.00–4\.95×4\.95\\times— measured against a binary arm that completes at every size there, where the earlier artifact had recorded its two largest cases as skipped for blow\-up\.

### 10\.5Event\-Calculus rule induction

This subsection asks how the induced theories score against the figures other authors have published for the same benchmark, and what the runs that do not favour the system look like\.[Section7](https://arxiv.org/html/2609.27203#S7)states the induction protocol and analyses its runs, and[Table3](https://arxiv.org/html/2609.27203#S7.T3)there lists them;[Table12](https://arxiv.org/html/2609.27203#S10.T12)collects their frame\-level scores\.

Published figures for the same benchmark\.[Table11](https://arxiv.org/html/2609.27203#S10.T11)places our pre\-registered ten\-fold row beside the four published frame\-levelholdsAtF1 figures formeetingon the whole distributed CAVIAR corpus\. Our figure is*below the floor of the published span*, by0\.00210\.0021: a fully pre\-registered run lands just under the lowest published figure, which is the hand\-crafted rule set\. The second\-iteration run reaches0\.77820\.7782, which is inside the span, but it is one disclosed adaptive iteration \([Section7](https://arxiv.org/html/2609.27203#S7)\); it is not the row in this table\.

The direct\-protocol reference on the same folds\.The run that produced that row also scores a direct per\-timestep reference theory on the same ten folds, under the direct protocol’s own pre\-registered defaults: held\-out accuracy, a fixed0\.750\.75fit gate, the default tie floor\. It lands far below the Event\-Calculus row beside it \([Table12](https://arxiv.org/html/2609.27203#S10.T12)\)\. The same reference theory comes out of all three ten\-fold runs \(the pre\-registered one, the second iteration and the neural negative\), so the second iteration’s added vocabulary never reaches the direct search\. Its recall is dominated by one fold on which the direct search abstains outright, leaving 855 gold frames undetected\. The figure is what those defaults produce on this corpus; it is no ceiling for the direct protocol, whose studied settings produce the windowed\-fold results of[Section7](https://arxiv.org/html/2609.27203#S7)\.

Table 11:Frame\-levelholdsAtF1 for themeetingfluent on the distributed CAVIAR corpus, micro\-averaged over pooled counts\. Rows are ordered alphabetically by system name, not by F1: the five protocol deltas printed beneath the table do not all act in the same direction\. Dashes are figures the cited table does not report\.*Protocol deltas, which must travel with this table\.*\(i\) The published runs cross\-validate over their own windowed interpretations with subsampled negatives; ours folds over whole video segments\. \(ii\) They learn full initiation*and*termination programs; our row commits a two\-literal initiation clause and an empty termination theory\. Out of its 2,304 predicted\-positive frames, 781 of the 788 false positives fall on the folds with detected interior terminations; the other 7 are initiation\-side errors persisted by inertia on a fold whose test side detects none\. \(iii\) Their rule language admits longer bodies—bottom clauses averaging some fifteen literals against our three\-literal cap\. \(iv\) Their settings are reported as the best among several tried; ours were pre\-registered\. No number of ours is adjusted on that basis\. \(v\) All rows compute F1 onholdsAtinferred through inertia, on the same corpus, the one axis on which the protocols do match, and the reason the rows are placed side by side at all\.

The remaining runs of[Section7](https://arxiv.org/html/2609.27203#S7), including the two that do not favour the system, are scored in[Table12](https://arxiv.org/html/2609.27203#S10.T12)and diagnosed there\. One of those rows needs a disclosure that section does not carry\.

Themovingthreshold, disclosed\.The two fluents carry different canonical proximity thresholds in the published CAVIAR rule set \(meetingoverclose\_25,movingoverclose\_34\), and themovingfigure above is measured under the canonicalclose\_34\. An earlier run over the same folds measuredmovingunder themeetingthreshold of 25 and scored*higher*\([Table12](https://arxiv.org/html/2609.27203#S10.T12)\)\. The canonical threshold remains the right headline, and the higher number is not evidence against it: where the clause is selected, wideningclosefrom 25 to 34 behaves exactly as threshold semantics predict, recall up and precision down\.

The micro figure falls for a selection\-level reason instead\. On the fold carrying 1,546 of the 3,136 goldmovingframes, the wider candidate pool puts the top two candidates inside the selection tie band, at a margin of0\.00930\.0093against the0\.010\.01tie floor, and the search abstains there where the threshold\-25 run had committed\. That figure therefore leaned on a fold whose selection was tie\-fragile, which is a reason to report the lower canonical number and the disagreement together rather than either alone\.

The maritime figures are not tabulated beside the published ones\.The maritime runs of[Section8](https://arxiv.org/html/2609.27203#S8)are not placed beside the published figure for that fluent;[Section8\.4](https://arxiv.org/html/2609.27203#S8.SS4)says why\.

Table 12:Frame\-levelholdsAtscores for every rule\-induction run of[Section7](https://arxiv.org/html/2609.27203#S7), micro F1 over pooled per\-fold counts\. The distributed corpus is the dump shipped with the published Event\-Calculus learners and carries the duplication defect measured in[Section7](https://arxiv.org/html/2609.27203#S7); the clean corpus is its deduplicated, scene\-family\-grouped form\. Dashes are quantities the run does not report separately\.
### 10\.6Verification cost and residency benefit

These two isolations ask what xlog’s design costs, separated from ordinary GPU acceleration: what the equivalence proof buys with cold\-compile time, and what device residency saves in transfers\. Both run on an A100 80GB PCIe pod with a26\.3526\.35\-core CPU quota, and[Table13](https://arxiv.org/html/2609.27203#S10.T13)carries their measurements\.

Verification cost\.The cold epoch’s compilation time is dominated by the on\-GPU CDCL equivalence check rather than the D4 compile\. Split on probabilistic reachability chains, CDCL verification accounts for98\.898\.8–99\.4%99\.4\\%of the cold\-compile time and grows with circuit size, while D4 compilation stays between1\.21\.2and11\.711\.7ms and is non\-zero at every point\. The “expensive” cold epoch is thus almost entirely the price of the machine\-checked correctness certificate \([Section5](https://arxiv.org/html/2609.27203#S5)\), a cost the CPU\-symbolic and GPU\-Datalog systems surveyed in[Section11](https://arxiv.org/html/2609.27203#S11)do not pay, because they do not verify\.

Table 13:Design\-cost isolations\. Verification splits the cold compile on probabilistic reachability chains of lengthnn\. Residency forces a device→\\tohost→\\todevice round\-trip at the neural–symbolic boundary, swept over22to512512handoffs per step on the batched addition path\.Residency benefit\.To isolate the transfer\-free advantage from ordinary GPU acceleration we run the same neural–symbolic pipeline with and without a forced device→\\tohost→\\todevice round\-trip at the neural–symbolic boundary, the transfer a CPU\-reasoning hybrid pays every step, sweeping the number of neural→\\tosymbolic handoffs per step\. Below a handful of handoffs the round\-trip cost is lost in run\-to\-run variation\. From a few dozen upward it is a visible share of the step, because the batched circuit compute grows sublinearly with the batch while the transfer grows linearly with the handoff count\.

On a single query the transfer is therefore negligible \(2\.7%2\.7\\%at two handoffs\); at a realistic training batch it is a≈16%\{\\approx\}16\\%tax that xlog does not pay, distinct from and additive to the GPU\-compute and circuit\-caching advantages\. The forced per\-buffer copy is an upper bound, since a hybrid could coalesce transfers\. The larger transfer\-dominated regime, large\-state Datalog fixpoints where whole relations would cross the bus every iteration \([Section1](https://arxiv.org/html/2609.27203#S1)\), lies outside what this isolation measures \([Section12](https://arxiv.org/html/2609.27203#S12)\)\.

### 10\.7Index reuse and the chain scorer

This pair of ablations asks what two of the runtime optimizations of[Section4](https://arxiv.org/html/2609.27203#S4)save on the repeated\-session workloads they target, each against the path it replaces\. The persistent hash\-index manager retains built join indices across evaluations, keyed on relation generation, schema signature and device ordinal, under a byte\-budgeted LRU policy: a session whose relations change little between calls reuses an index instead of rebuilding it, and a generation change invalidates the entry instead of serving a stale one\. The profile\-gated shared\-memory chain scorer tiles the left relation through shared memory when scoring chain\-shaped candidate bodies during exact rule induction, and is gated on a candidate\-row threshold below which the baseline scorer runs unchanged\.

Both target the same waste, work repeated across calls that the previous call already did, and both are transparent to the program\. Common\-subexpression elimination and adaptive re\-optimization are held to output equivalence with the unoptimized plan\.

[Table14](https://arxiv.org/html/2609.27203#S10.T14)gives the medians\. Two things belong with them\. The index fixture was re\-measured in release after an earlier version of its artifact recorded a build flag the run had not used; the same pod then ran both profiles back to back, and release is the*higher*ratio,8\.33×8\.33\\timesagainst7\.72×7\.72\\timesin debug\. The reason is that the two arms sit on different sides of the bus: the index\-rebuilding arm is GPU\-bound and barely moves between profiles \(15\.8315\.83to15\.7815\.78ms\), while the cached arm is host\-side and does get faster \(2\.052\.05to1\.891\.89ms\), so optimizing the build widens the gap\. And the chain scorer’s ratio rose from5\.58×5\.58\\timesto7\.20×7\.20\\timespartly because its baseline arm got slower on this card,27\.5127\.51to52\.4252\.42ms, so that gain is not a like\-for\-like improvement over the earlier record\. The index fixture is build\-heavy by construction, so that building the index dominates the join, and neither arm records a host transfer\. The chain scorer’s two arms do not overlap on the chain\-hot fixture; on a small input below its gate threshold, where the baseline path runs instead, the two medians differ by2\.0%2\.0\\%and the arms’ ranges overlap\. Both are point medians on single synthetic fixtures, and the scorer’s coverage output is identical to the baseline’s on both\. The scorer’s artifact now also records the host\-transfer count per arm rather than asserting a fixed one: what the claim rests on is that the shared\-memory arm adds none relative to baseline, and the measured difference is zero\.

Table 14:Runtime\-optimization ablations, each a median over the timed runs of one synthetic fixture\.
### 10\.8Capability coverage across systems

[Table15](https://arxiv.org/html/2609.27203#S10.T15)positions xlog qualitatively against representative systems; each addresses a subset of the design space, and xlog’s contribution is exposing the supported routes through one typed language and provider\-owned CUDA runtime services\. This table covers capability: the quantitative head\-to\-head results against Scallop, ProbLog2 and Soufflé are in[Section10\.4](https://arxiv.org/html/2609.27203#S10.SS4)\.

The rule\-induction row covers two paths of different maturity: the trainable\-rule\-body path is carried onto an external benchmark in[Section7](https://arxiv.org/html/2609.27203#S7)and tabulated in[Section10\.5](https://arxiv.org/html/2609.27203#S10.SS5), while the differentiable\-ILP path is not exercised there at all \([Section6](https://arxiv.org/html/2609.27203#S6)\)\. The table’s “yes” claims capability, not maturity \([Section12](https://arxiv.org/html/2609.27203#S12)\)\.

Table 15:Capability comparison across neurosymbolic and GPU logic systems\.
### 10\.9Log\-evidence, rule unions, and exact constraint solving

The capabilities below round out the runtime surface\. Each is described for what it does; no timing is claimed for any of them\.

Exact log\-evidence and the CNF\-variable\-to\-fact map\.An exact evaluation now returns the log partition function of the weighted formula,log⁡Z\\log Z, alongside the per\-query probabilities, so a program’s evidence mass is read off directly instead of being reconstructed from marginals; it surfaces aslog\_z\_eon the Python result\. Paired with it,prob\_var\_map\(\)reports which probabilistic fact each CNF variable stands for \(an ordinary fact, one Bernoulli decision of an annotated disjunction’s chain, or padding\) so the per\-variable gradient buffers can be attributed back to program facts and not to opaque indices\. Its length is the encoder’s variable*capacity*, not a variable count, and it is refused with a typed error where there is no CNF encoding to report: Monte Carlo programs, and exact programs taking the GPU fast path that skips the encoding\.

Same\-head rule unions in one multiway pass\.A predicate head defined by many rules used to fold its per\-rule contributions into the head relation one union at a time, re\-sorting the growing accumulator once per rule and going quadratic in the rule count, a real cost at corpus scale where one head can carry thousands of rules\. Contributions are now merged with a single multiway union per head per iteration\. The union count therefore no longer scales with the same\-head rule count \(eight same\-head rules record one union, not eight\) while the derived rows stay byte\-identical to the unbatched result\.

An exact stage beyond enumeration capacity\.Constraint solving over several interacting constraints enumerates a component completely where it is small enough\. Long chain\-shaped components that exceed that capacity take a memoized dynamic\-programming stage on the GPU instead, which computes the same totals exactly instead of approximating them\. A component wider than the configured limit is refused with a typed error instead of served by an approximation, and the solver’s buffers reach Python through the same zero\-copy DLPack\[[14](https://arxiv.org/html/2609.27203#bib.bib15)\]views as the rest of the runtime \([Section6\.3](https://arxiv.org/html/2609.27203#S6.SS3)\)\.

## 11Related Work

xlog draws on five lines of research: neurosymbolic programming, GPU\-accelerated Datalog, probabilistic logic programming, GPU SAT, and differentiable ILP\. Its contribution is to expose those capabilities through one typed language and shared CUDA services while retaining route\-specific execution and differentiability contracts\.

### 11\.1Neurosymbolic programming

DeepProbLog\[[25](https://arxiv.org/html/2609.27203#bib.bib5)\]replaces selected probabilistic facts with neural\-network outputs, enabling end\-to\-end gradient training of neural predicates inside a probabilistic\-logic framework\. NeurASP\[[43](https://arxiv.org/html/2609.27203#bib.bib6)\]integrates network outputs as probability annotations on answer\-set programs\. Both perform symbolic inference on the CPU and shuttle gradients across the bus\. Scallop\[[24](https://arxiv.org/html/2609.27203#bib.bib32)\]provides a differentiable Datalog with provenance\-semiring reasoning\[[19](https://arxiv.org/html/2609.27203#bib.bib37)\]and a relational symbolic representation, and is the closest language\-level analogue to xlog\. Its reasoning core, however, is CPU\-based\.

Lobster\[[5](https://arxiv.org/html/2609.27203#bib.bib31)\]is the most directly comparable system: it GPU\-accelerates neurosymbolic programs in the Scallop style, and shares xlog’s premise that the symbolic data plane belongs on the GPU\. Against it, xlog is complementary along three axes\. It includes exact knowledge compilation and epistemic reasoning in addition to provenance\-based differentiable Datalog\. It certifies the final smoothed circuit’s logical equivalence to its back\-end source formula using GPU CDCL and on\-device proof checking\. And it reports route\-specific residency with byte\-level transfer accounting\. No head\-to\-head performance comparison with Lobster is drawn here \([Section12](https://arxiv.org/html/2609.27203#S12)\)\.

Differentiable\-SAT and logic\-as\-loss methods \(SATNet\[[39](https://arxiv.org/html/2609.27203#bib.bib41)\], semantic loss\[[42](https://arxiv.org/html/2609.27203#bib.bib42)\], and Logic Tensor Networks\[[4](https://arxiv.org/html/2609.27203#bib.bib43)\]\) instead couple neural models to constraints through relaxed or fuzzy surrogates\. By contrast, xlog couples through*exact*weighted model counting, trading their broader applicability for exact gradients and the on\-device verifiability of[Section5](https://arxiv.org/html/2609.27203#S5)\.

### 11\.2GPU\-accelerated Datalog and joins

GPUlog\[[36](https://arxiv.org/html/2609.27203#bib.bib1)\]ported bottom\-up fixed\-point computation to CUDA using HISA indexing, and reported up to45×45\\timesspeedups over CPU Datalog engines\. VFLog\[[34](https://arxiv.org/html/2609.27203#bib.bib2)\]advanced this with a vertically\-fused, column\-oriented kernel design that avoids intermediate materialization, reporting up to200×200\\timesover CPU column engines; mnmgDatalog\[[32](https://arxiv.org/html/2609.27203#bib.bib3)\]extends GPU Datalog to multi\-node, multi\-GPU clusters\. Most relevant to xlog’s join path, Sun et al\.\[[35](https://arxiv.org/html/2609.27203#bib.bib33)\]scale worst\-case\-optimal joins to GPUs\.

All of them target deterministic Datalog only: none supports probabilistic semantics, weighted model counting, or gradient computation over derived facts\. Like them, xlog uses a columnar, kernel\-fused execution model, and it also promotes eligible cyclic and multiway rules to a worst\-case\-optimal join path\[[27](https://arxiv.org/html/2609.27203#bib.bib26),[38](https://arxiv.org/html/2609.27203#bib.bib27),[40](https://arxiv.org/html/2609.27203#bib.bib28)\]\. But that engine is one component of a substrate that extends through circuit\-based inference to neural\-symbolic gradient propagation in a single address space\.

### 11\.3Probabilistic logic programming

ProbLog2\[[16](https://arxiv.org/html/2609.27203#bib.bib4)\]established the modern pipeline for exact probabilistic inference: ground the program, encode provenance as a propositional formula, compile to a tractable target \(d\-DNNF\[[11](https://arxiv.org/html/2609.27203#bib.bib34)\]or SDD\[[13](https://arxiv.org/html/2609.27203#bib.bib39)\]\), and evaluate weighted model counts\[[8](https://arxiv.org/html/2609.27203#bib.bib36)\]\. The compilers \(D4\[[23](https://arxiv.org/html/2609.27203#bib.bib14)\], c2d\[[12](https://arxiv.org/html/2609.27203#bib.bib17)\]\) run as host\-side subprocesses, and recent work makes such compilation*certified*\[[6](https://arxiv.org/html/2609.27203#bib.bib40)\]\. xlog adopts the same compile\-once/evaluate\-many model with CUDA\-backed data planes for provenance, Tseitin encoding, D4 compilation, equivalence verification, and forward/backward evaluation\. The host orchestrates those stages and reads bounded solver control state; device circuit and gradient buffers share an address space with the neural and deterministic data planes\.

### 11\.4GPU SAT

ParaFROST\[[28](https://arxiv.org/html/2609.27203#bib.bib7)\]parallelizes CDCL clause\-database simplification on the GPU while retaining sequential conflict\-driven search on the CPU\. FastFourierSAT\[[7](https://arxiv.org/html/2609.27203#bib.bib19)\]reformulates SAT as continuous optimization and applies GPU local search, an incomplete solver for satisfiable instances\. Both are standalone competition solvers\. In xlog the GPU CDCL module is instead a verification component inside knowledge compilation \([Section5](https://arxiv.org/html/2609.27203#S5)\), proving circuit–formula equivalence via two UNSAT proofs and providing the certificates the probabilistic and epistemic backends rely on\.

### 11\.5Differentiable ILP

Differentiable ILP\[[15](https://arxiv.org/html/2609.27203#bib.bib8)\]casts first\-order rule induction as differentiable optimization, scoring candidate rules by soft forward\-chaining\. Dense materialization over the rule space scales cubically in the number of constants, and implementations remain CPU\-based\. The dILP subsystem of xlog \([Section6](https://arxiv.org/html/2609.27203#S6)\) replaces dense materialization with sparse GPU bitmasks and on\-device scatter–gather credit assignment, avoiding the cubic blowup while preserving differentiability\.

### 11\.6Logic programming languages

xlog inherits ideas from a long line of logic languages\. Prolog\[[41](https://arxiv.org/html/2609.27203#bib.bib22)\]offers unification and metaprogramming on a CPU interpreter; Mercury\[[33](https://arxiv.org/html/2609.27203#bib.bib23)\]introduced strong typing and modes, compiling to native code\. Soufflé\[[20](https://arxiv.org/html/2609.27203#bib.bib24)\]is a typed Datalog compiling to C\+\+ for program analysis, and clingo\[[18](https://arxiv.org/html/2609.27203#bib.bib25)\]provides answer\-set semantics on CPU grounders and solvers\. From these xlog adopts the typed\-predicate discipline while unifying typed Datalog, probabilistic facts, neural predicates, and epistemic operators in one language whose supported routes use CUDA kernels and provider\-owned runtime services\.

## 12Limitations and Future Work

### 12\.1Current limitations

NVIDIA GPU required\.The execution kernels are written in CUDA C; there is no OpenCL, Metal, or ROCm backend\. The persistent\-index manager, recorded\-launch discipline, and in\-kernel hash\-consing use CUDA\-specific primitives such as cooperative groups, warp\-level operations, and unified virtual addressing\. Users without a supported NVIDIA GPU cannot run xlog\.

Device memory and fixed capacities are bounded\.Relations, indices, circuit buffers, and Monte Carlo sample arrays are allocated on\-device; there is no out\-of\-core spilling\. An allocation that exceeds the configured byte budget fails withRESOURCE\_EXHAUSTED\. A row, tuple, sample, domain, or other fixed\-count limit instead fails withCAPACITY\_EXCEEDED, naming the exhausted unit\. A bounded recursive or Monte Carlo fixpoint that reaches its iteration limit without convergence fails withCONVERGENCE\_FAILURE; partial counters do not turn it into a result\.

Maturity of the rule\-learning surfaces\.The differentiable\-ILP subsystem \([Section6](https://arxiv.org/html/2609.27203#S6)\) is beta: the search space is restricted to definite programs, convergence is sensitive to learning\-rate schedules, and its API may change\. The trainable\-rule\-body surface of[Section6\.4](https://arxiv.org/html/2609.27203#S6.SS4)\(mixed neural/symbolic bodies, existential joins, and joint multi\-rule mixtures\) is at the same maturity\. It is carried onto a public benchmark under pre\-registered gates and cross\-validation in[Section7](https://arxiv.org/html/2609.27203#S7), but how its accuracy and training cost compare with dedicated relational learners on standard benchmarks is an open question\.

Coverage of the epistemic runtime\.The epistemic runtime \([Section9](https://arxiv.org/html/2609.27203#S9)\) executes its accepted data\-plane work on the GPU, but the broader solver portfolio \(MaxSAT/portfolio services\) and the end\-to\-end probabilistic–epistemic evidence path are still being broadened\. The negated\-modal WFS route and Gelfond\-1991 compatibility refinement are GPU\-backed but host\-orchestrated\. Positive modal dependency cycles have defined execution: FAEEL computes a founded least fixpoint, including an empty extension for an unseeded cycle, and supported Gelfond\-1991 positivepossiblecycles compute the greatest compatible set of concrete tuples from an upper bound and frozen snapshots\. The shared recursion\-depth setting bounds both descending compatibility refinements and WFS iterations\.

Fail\-closed boundaries\.Raw lowering of modal literals, recursive epistemic programs that also contain modal integrity constraints, WFS shapes outside the supported negated\-modal plan, unbounded tuple\-key forms, and recursive negation or aggregation within a Gelfond\-1991 compatibility component all remain fail\-closed\. The Python batch\-query helpers are typed but do not yet accept floating\-point uploads, a convenience\-API gap and not a core execution limit\.

Partial head\-to\-head coverage\.[Section10\.4](https://arxiv.org/html/2609.27203#S10.SS4)reports controlled comparisons on identical programs and data against one external engine per reasoning mode: Scallop \(neural\-symbolic\), ProbLog2 \(probabilistic\), and Soufflé \(deterministic\)\. Coverage is still partial\. Lobster, the most directly comparable GPU\-neurosymbolic system, and the GPU Datalog engines GPUlog and VFLog are not among the baselines; DeepProbLog was not run under a matched \(non\-timeout\) protocol; and each comparison rests on a single GPU configuration rather than a cross\-hardware sweep\. That last limitation is not hypothetical: measuring the MNIST comparison on two L40S pods with the same wheel, the same seeds and different CPU quotas moved Scallop’s steady epoch from31\.7931\.79s at13\.613\.6cores to54\.9954\.99s at27\.227\.2, so the epoch ratio between the two systems changed by a factor of1\.81\.8with neither engine touched\. The pods differed in driver revision and host as well as in quota, so the quota is the candidate explanation rather than the isolated cause; the27\.227\.2\-core measurement is distributed as the companion file beside the MNIST artifact\. That is why[Section10\.4](https://arxiv.org/html/2609.27203#S10.SS4)reports accuracy for that comparison and no timing\. A per\-cell ratio measured on one host is a property of the pair*and*the host; broader multi\-system, multi\-hardware comparison remains future work\.

Rule\-induction evidence\.The evidence of[Section7](https://arxiv.org/html/2609.27203#S7)is thinnest exactly where it is leak\-free: the deduplicated, scene\-family\-grouped corpus carries too few initiation events for a cross\-validated claim\. Both routes commit a clause on most folds and that clause does not transfer, so the protocol yields nomeetingtheory and supports no conclusion about that fluent’s learnability in either direction\. The protocol\-matched numbers are computed instead on the dump distributed with the published Event\-Calculus learners, which carries a measured duplication defect; we report there because it is the regime the published figures share, and every figure computed on it inherits that caveat\. No ordering against OLED, WOLED\-ASP or the hand\-crafted rule set follows from[Table11](https://arxiv.org/html/2609.27203#S10.T11), and none is claimed: the five protocol deltas printed with that table are real, unquantified, and do not act in the same direction, while the clean protocol has too few events to settle any of them\. Learning termination programs and lifting the body\-length cap, which would remove two of those deltas, is future work\.

Two figures of different status\.The headline figure of[Section7](https://arxiv.org/html/2609.27203#S7)is fully pre\-registered: gates, seeds and folds were fixed before the run, and that run was executed once\. The second\-iteration figure differs from it in exactly one respect, its Event\-Calculus vocabulary having been chosen after the first run’s failure mode was known on the same folds, which makes it one disclosed adaptive iteration and not a pre\-registered result; it is reported only with that label and is never the row we place beside a published number\.

Maritime scope\.The maritime runs of[Section8](https://arxiv.org/html/2609.27203#S8)remove the evidence\-starvation bound, but they carry bounds of their own\. Their supervision is synthetic: the gold labels are a hand\-crafted rule’s output over the same streams the vocabulary is derived from, a regime the published maritime figures share\. Every number there is therefore a rule\-reconstruction figure under an incomplete vocabulary, not a detection figure, and none of those runs exercises the GPU substrate\. Their temporal grid is the critical\-point grid of the RTEC exports, not the dense grid of the published figure, so no maritime number of ours stands beside the published0\.980\.98and no pass time beside the published training times \([Section8\.4](https://arxiv.org/html/2609.27203#S8.SS4)\)\. And the single\-pass runs are online in the weights only, their body pool and permutation\-null gate being computed on the training side: they demonstrate single\-pass weight learning and not online structure revision, which remains future work, and the zero degradation they measure rests on a single body sitting above the decision threshold in every regime, on a0\.0070\.007margin; it is a property of this pool, corpus and threshold, not a robustness result\.

### 12\.2Future work

Out\-of\-core execution\.A streaming mode would partition relations across host and device, paging tiles through GPU memory in fixpoint\-iteration order, removing the single\-GPU\-memory ceiling at the cost of added transfers\.

Multi\-GPU partitioned evaluation\.Inspired by mnmgDatalog’s\[[32](https://arxiv.org/html/2609.27203#bib.bib3)\]radix\-hash partitioning and GPU\-aware all\-to\-all shuffle, a multi\-GPU backend would distribute relations across devices and coordinate joins over NVLink or PCIe\.

Deeper epistemic residency\.The remaining epistemic work is stronger residency and coverage: a device\-resident, no\-host\-interaction well\-founded path, broader non\-finite tuple\-key forms, and semantic forms beyond the current finite accepted surface\.

## 13Conclusion

xlog is a CUDA\-native logic programming engine with one typed language and provider\-owned runtime services for deterministic, probabilistic, epistemic, and neural\-symbolic use\. A neural network is an ordinary predicate; exact query gradients flow through the probabilistic knowledge\-compilation route, while the other routes reuse typed device\-buffer interfaces without claiming identical differentiability\. The final smoothed probabilistic circuit is certified against its back\-end source formula before it is cached or evaluated\. Solver proof traces are checked on the GPU, and the host observes bounded status and error scalars\.

Residency claims are likewise route\-specific\. Ordinary relational and exact execution are host\-orchestrated over device data planes\. Eligible recursion and resident Monte Carlo use certified cores that record zero tracked transfers and then return one authoritative terminal receipt\. Byte exhaustion, fixed\-capacity exhaustion, and nonconvergence remain separate typed outcomes\.

The measurements describe a system that pays off where the symbolic workload is large and repeated: reusing a verified circuit across training iterations, and avoiding the intermediate blowup of binary\-join plans on skewed cyclic queries\. Against external engines the picture is mixed: clear gains in bounded\-memory join evaluation and in per\-epoch neurosymbolic training, and a clear loss to a mature CPU compiler on small exact\-inference programs\.

What they do not give is a general ranking of xlog against other systems\. Each comparison covers one engine per reasoning mode on one class of program, the rule\-induction results rest on two public corpora, and the epistemic and rule\-learning surfaces are young\. The evidence supports the architecture, not a claim of universal superiority\.

The direction is the one the architecture already implies: out\-of\-core and multi\-GPU execution to lift the memory ceiling, deeper residency for the epistemic routes, and structure learning that runs on the stream rather than over it\.

## References

- \[1\]L\. O\. Andersen\(1994\)Program analysis and specialization for the C programming language\.Ph\.D\. Thesis,University of Copenhagen\.Cited by:[§10\.2](https://arxiv.org/html/2609.27203#S10.SS2.p2.1)\.
- \[2\]Apache Arrow: cross\-language development platform for in\-memory data\.Note:[https://arrow\.apache\.org](https://arrow.apache.org/)Accessed 2026Cited by:[§6\.3](https://arxiv.org/html/2609.27203#S6.SS3.p3.1)\.
- \[3\]A\. Artikis, M\. Sergot, and G\. Paliouras\(2015\)An Event Calculus for event recognition\.IEEE Transactions on Knowledge and Data Engineering27\(4\),pp\. 895–908\.External Links:[Document](https://dx.doi.org/10.1109/TKDE.2014.2356476)Cited by:[§8\.1](https://arxiv.org/html/2609.27203#S8.SS1.p1.1)\.
- \[4\]S\. Badreddine, A\. d’Avila Garcez, L\. Serafini, and M\. Spranger\(2022\)Logic tensor networks\.Artificial Intelligence303,pp\. 103649\.Cited by:[§11\.1](https://arxiv.org/html/2609.27203#S11.SS1.p3.1)\.
- \[5\]P\. Biberstein, Z\. Li, J\. Devietti, and M\. Naik\(2026\)Lobster: a GPU\-accelerated framework for neurosymbolic programming\.InArchitectural Support for Programming Languages and Operating Systems \(ASPLOS\),Note:arXiv:2503\.21937Cited by:[§11\.1](https://arxiv.org/html/2609.27203#S11.SS1.p2.1)\.
- \[6\]F\. Capelli\(2019\)Knowledge compilation languages as proof systems\.InTheory and Applications of Satisfiability Testing \(SAT\),Lecture Notes in Computer Science, Vol\.11628,pp\. 90–99\.Cited by:[§11\.3](https://arxiv.org/html/2609.27203#S11.SS3.p1.1),[§5\.2](https://arxiv.org/html/2609.27203#S5.SS2.p2.1)\.
- \[7\]Y\. Cen, Z\. Zhang, and X\. Fong\(2023\)Massively parallel continuous local search for hybrid SAT solving on GPUs\.Note:arXiv:2308\.15020Cited by:[§11\.4](https://arxiv.org/html/2609.27203#S11.SS4.p1.1)\.
- \[8\]M\. Chavira and A\. Darwiche\(2008\)On probabilistic inference by weighted model counting\.Artificial Intelligence172\(6\-7\),pp\. 772–799\.Cited by:[§11\.3](https://arxiv.org/html/2609.27203#S11.SS3.p1.1),[§5\.1](https://arxiv.org/html/2609.27203#S5.SS1.p4.1)\.
- \[9\]Cudarc: safe rust wrapper around CUDA\.Note:[https://github\.com/coreylowman/cudarc](https://github.com/coreylowman/cudarc)Accessed 2026Cited by:[§2\.3](https://arxiv.org/html/2609.27203#S2.SS3.p1.1)\.
- \[10\]A\. Darwiche and P\. Marquis\(2002\)A knowledge compilation map\.Journal of Artificial Intelligence Research17,pp\. 229–264\.Cited by:[§5\.1](https://arxiv.org/html/2609.27203#S5.SS1.p4.1)\.
- \[11\]A\. Darwiche\(2001\)Decomposable negation normal form\.Journal of the ACM48\(4\),pp\. 608–647\.Cited by:[§11\.3](https://arxiv.org/html/2609.27203#S11.SS3.p1.1),[§5\.1](https://arxiv.org/html/2609.27203#S5.SS1.p4.1)\.
- \[12\]A\. Darwiche\(2004\)New advances in compiling CNF into decomposable negation normal form\.InProceedings of the 16th European Conference on Artificial Intelligence \(ECAI\),Cited by:[§11\.3](https://arxiv.org/html/2609.27203#S11.SS3.p1.1)\.
- \[13\]A\. Darwiche\(2011\)SDD: a new canonical representation of propositional knowledge bases\.InProceedings of the Twenty\-Second International Joint Conference on Artificial Intelligence \(IJCAI\),pp\. 819–826\.Cited by:[§11\.3](https://arxiv.org/html/2609.27203#S11.SS3.p1.1)\.
- \[14\]DLPack: open in memory tensor structure\.Note:[https://github\.com/dmlc/dlpack](https://github.com/dmlc/dlpack)Accessed 2026Cited by:[§1](https://arxiv.org/html/2609.27203#S1.p3.1),[§10\.9](https://arxiv.org/html/2609.27203#S10.SS9.p4.1),[§6\.3](https://arxiv.org/html/2609.27203#S6.SS3.p2.1)\.
- \[15\]R\. Evans and E\. Grefenstette\(2018\)Learning explanatory rules from noisy data\.Journal of Artificial Intelligence Research61,pp\. 1–64\.Cited by:[§11\.5](https://arxiv.org/html/2609.27203#S11.SS5.p1.1)\.
- \[16\]D\. Fierens, G\. Van den Broeck, J\. Renkens, D\. Shterionov, B\. Gutmann, I\. Thon, G\. Janssens, and L\. De Raedt\(2015\)Inference and learning in probabilistic logic programs using weighted Boolean formulas\.Theory and Practice of Logic Programming15\(3\),pp\. 358–401\.Cited by:[§11\.3](https://arxiv.org/html/2609.27203#S11.SS3.p1.1),[§5](https://arxiv.org/html/2609.27203#S5.p1.1)\.
- \[17\]A\. Flores\-Montoya and E\. Schulte\(2020\)Datalog disassembly\.InUSENIX Security Symposium,pp\. 1075–1092\.Cited by:[§10\.2](https://arxiv.org/html/2609.27203#S10.SS2.p2.1)\.
- \[18\]M\. Gebser, R\. Kaminski, B\. Kaufmann, and T\. Schaub\(2019\)Multi\-shot ASP solving with clingo\.Theory and Practice of Logic Programming19\(1\),pp\. 27–82\.Cited by:[§11\.6](https://arxiv.org/html/2609.27203#S11.SS6.p1.1)\.
- \[19\]T\. J\. Green, G\. Karvounarakis, and V\. Tannen\(2007\)Provenance semirings\.InProceedings of the 26th ACM SIGMOD\-SIGACT\-SIGART Symposium on Principles of Database Systems \(PODS\),pp\. 31–40\.Cited by:[§11\.1](https://arxiv.org/html/2609.27203#S11.SS1.p1.1),[§5\.1](https://arxiv.org/html/2609.27203#S5.SS1.p2.1)\.
- \[20\]H\. Jordan, B\. Scholz, and P\. Subotić\(2016\)Soufflé: on synthesis of program analyzers\.InComputer Aided Verification \(CAV\),pp\. 422–430\.Cited by:[§11\.6](https://arxiv.org/html/2609.27203#S11.SS6.p1.1)\.
- \[21\]N\. Katzouris, A\. Artikis, and G\. Paliouras\(2016\)Online learning of Event Definitions\.Theory and Practice of Logic Programming\.External Links:1608\.00100Cited by:[Table 11](https://arxiv.org/html/2609.27203#S10.T11.6.2.5.1.1),[Table 11](https://arxiv.org/html/2609.27203#S10.T11.6.3.5.1.1),[§7\.2](https://arxiv.org/html/2609.27203#S7.SS2.p2.1.2)\.
- \[22\]N\. Katzouris, G\. Paliouras, and A\. Artikis\(2023\)Online learning probabilistic Event Calculus theories in Answer Set Programming\.Theory and Practice of Logic Programming23\(2\),pp\. 362–386\.External Links:[Document](https://dx.doi.org/10.1017/S1471068421000107),2104\.00158Cited by:[Table 11](https://arxiv.org/html/2609.27203#S10.T11.6.2.5.1.1),[Table 11](https://arxiv.org/html/2609.27203#S10.T11.6.4.5.1.1),[Table 11](https://arxiv.org/html/2609.27203#S10.T11.6.6.5.1.1),[§7\.2](https://arxiv.org/html/2609.27203#S7.SS2.p2.1.2),[§8\.1](https://arxiv.org/html/2609.27203#S8.SS1.p2.1),[§8\.3](https://arxiv.org/html/2609.27203#S8.SS3.p7.1),[§8\.4](https://arxiv.org/html/2609.27203#S8.SS4.p1.1)\.
- \[23\]J\. Lagniez and P\. Marquis\(2017\)An improved decision\-DNNF compiler\.InProceedings of the Twenty\-Sixth International Joint Conference on Artificial Intelligence \(IJCAI\),Cited by:[§11\.3](https://arxiv.org/html/2609.27203#S11.SS3.p1.1),[§5\.1](https://arxiv.org/html/2609.27203#S5.SS1.p4.1)\.
- \[24\]Z\. Li, J\. Huang, and M\. Naik\(2023\)Scallop: a language for neurosymbolic programming\.Proceedings of the ACM on Programming Languages \(PLDI\)7,pp\. 166:1–166:25\.Cited by:[§11\.1](https://arxiv.org/html/2609.27203#S11.SS1.p1.1)\.
- \[25\]R\. Manhaeve, S\. Dumancic, A\. Kimmig, T\. Demeester, and L\. De Raedt\(2018\)DeepProbLog: neural probabilistic logic programming\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[§1](https://arxiv.org/html/2609.27203#S1.p1.1),[§11\.1](https://arxiv.org/html/2609.27203#S11.SS1.p1.1)\.
- \[26\]M\. W\. Moskewicz, C\. F\. Madigan, Y\. Zhao, L\. Zhang, and S\. Malik\(2001\)Chaff: engineering an efficient SAT solver\.InProceedings of the 38th Design Automation Conference \(DAC\),pp\. 530–535\.Cited by:[§5\.1](https://arxiv.org/html/2609.27203#S5.SS1.p4.1)\.
- \[27\]H\. Q\. Ngo, E\. Porat, C\. Ré, and A\. Rudra\(2018\)Worst\-case optimal join algorithms\.Journal of the ACM65\(3\),pp\. 16:1–16:40\.Cited by:[§11\.2](https://arxiv.org/html/2609.27203#S11.SS2.p2.1),[§4\.4](https://arxiv.org/html/2609.27203#S4.SS4.p1.1)\.
- \[28\]M\. Osama, A\. Wijs, and A\. Biere\(2021\)SAT solving with GPU accelerated inprocessing\.InTools and Algorithms for the Construction and Analysis of Systems \(TACAS\),Lecture Notes in Computer Science, Vol\.12651,pp\. 133–151\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-72016-2%5F8)Cited by:[§1](https://arxiv.org/html/2609.27203#S1.p2.1),[§11\.4](https://arxiv.org/html/2609.27203#S11.SS4.p1.1)\.
- \[29\]M\. Pitsikalis, A\. Artikis, R\. Dréo, C\. Ray, E\. Camossi, and A\. Jousselme\(2019\)Composite event recognition for maritime monitoring\.InProceedings of the 13th ACM International Conference on Distributed and Event\-based Systems \(DEBS\),pp\. 163–174\.External Links:[Document](https://dx.doi.org/10.1145/3328905.3329762)Cited by:[§8\.1](https://arxiv.org/html/2609.27203#S8.SS1.p1.1),[§8](https://arxiv.org/html/2609.27203#S8.p1.1)\.
- \[30\]PyO3: rust bindings for Python\.Note:[https://pyo3\.rs](https://pyo3.rs/)Accessed 2026Cited by:[§2\.3](https://arxiv.org/html/2609.27203#S2.SS3.p1.1),[§6\.3](https://arxiv.org/html/2609.27203#S6.SS3.p4.1)\.
- \[31\]C\. Ray, R\. Dréo, E\. Camossi, A\. Jousselme, and C\. Iphar\(2019\)Heterogeneous integrated dataset for maritime intelligence, surveillance, and reconnaissance\.Data in Brief25,pp\. 104141\.External Links:[Document](https://dx.doi.org/10.1016/j.dib.2019.104141)Cited by:[§8](https://arxiv.org/html/2609.27203#S8.p1.1)\.
- \[32\]A\. R\. Shovon, Y\. Sun, T\. Gilray, K\. Micinski, and S\. Kumar\(2025\)Multi\-node multi\-GPU Datalog\.InProceedings of the 39th ACM International Conference on Supercomputing \(ICS\),External Links:[Document](https://dx.doi.org/10.1145/3721145.3730431)Cited by:[§11\.2](https://arxiv.org/html/2609.27203#S11.SS2.p1.1),[§12\.2](https://arxiv.org/html/2609.27203#S12.SS2.p2.1)\.
- \[33\]Z\. Somogyi, F\. Henderson, and T\. Conway\(1996\)The execution algorithm of Mercury, an efficient purely declarative logic programming language\.Journal of Logic Programming29\(1\-3\),pp\. 17–64\.Cited by:[§11\.6](https://arxiv.org/html/2609.27203#S11.SS6.p1.1)\.
- \[34\]Y\. Sun, S\. Kumar, T\. Gilray, and K\. Micinski\(2025\)Column\-oriented Datalog on the GPU\.InProceedings of the AAAI Conference on Artificial Intelligence,Vol\.39,pp\. 15177–15185\.External Links:[Document](https://dx.doi.org/10.1609/aaai.v39i14.33665)Cited by:[§1](https://arxiv.org/html/2609.27203#S1.p2.1),[§11\.2](https://arxiv.org/html/2609.27203#S11.SS2.p1.1)\.
- \[35\]Y\. Sun, K\. Qi, T\. Gilray, S\. Kumar, and K\. Micinski\(2026\)Scaling worst\-case optimal Datalog to GPUs\.Note:arXiv:2604\.20073Cited by:[§11\.2](https://arxiv.org/html/2609.27203#S11.SS2.p1.1)\.
- \[36\]Y\. Sun, A\. R\. Shovon, T\. Gilray, S\. Kumar, and K\. Micinski\(2025\)Optimizing Datalog for the GPU\.InProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems \(ASPLOS\),External Links:[Document](https://dx.doi.org/10.1145/3669940.3707274)Cited by:[§1](https://arxiv.org/html/2609.27203#S1.p2.1),[§11\.2](https://arxiv.org/html/2609.27203#S11.SS2.p1.1)\.
- \[37\]G\. S\. Tseitin\(1968\)On the complexity of derivation in propositional calculus\.Studies in Constructive Mathematics and Mathematical Logic\.Cited by:[§5\.1](https://arxiv.org/html/2609.27203#S5.SS1.p3.1)\.
- \[38\]T\. L\. Veldhuizen\(2014\)Leapfrog triejoin: a simple, worst\-case optimal join algorithm\.InInternational Conference on Database Theory \(ICDT\),pp\. 96–106\.Cited by:[§11\.2](https://arxiv.org/html/2609.27203#S11.SS2.p2.1),[§4\.4](https://arxiv.org/html/2609.27203#S4.SS4.p1.1)\.
- \[39\]P\. Wang, P\. L\. Donti, B\. Wilder, and J\. Z\. Kolter\(2019\)SATNet: bridging deep learning and logical reasoning using a differentiable satisfiability solver\.InProceedings of the 36th International Conference on Machine Learning \(ICML\),pp\. 6545–6554\.Cited by:[§11\.1](https://arxiv.org/html/2609.27203#S11.SS1.p3.1)\.
- \[40\]Y\. R\. Wang, M\. Willsey, and D\. Suciu\(2023\)Free join: unifying worst\-case optimal and traditional joins\.Proceedings of the ACM on Management of Data \(SIGMOD\)1\(2\),pp\. 150:1–150:23\.Cited by:[§11\.2](https://arxiv.org/html/2609.27203#S11.SS2.p2.1),[§4\.4](https://arxiv.org/html/2609.27203#S4.SS4.p1.1)\.
- \[41\]J\. Wielemaker, T\. Schrijvers, M\. Triska, and T\. Lager\(2012\)SWI\-Prolog\.Theory and Practice of Logic Programming12\(1\-2\),pp\. 67–96\.Cited by:[§11\.6](https://arxiv.org/html/2609.27203#S11.SS6.p1.1)\.
- \[42\]J\. Xu, Z\. Zhang, T\. Friedman, Y\. Liang, and G\. Van den Broeck\(2018\)A semantic loss function for deep learning with symbolic knowledge\.InProceedings of the 35th International Conference on Machine Learning \(ICML\),pp\. 5502–5511\.Cited by:[§11\.1](https://arxiv.org/html/2609.27203#S11.SS1.p3.1)\.
- \[43\]Z\. Yang, A\. Ishay, and J\. Lee\(2020\)NeurASP: embracing neural networks into answer set programming\.InProceedings of the Twenty\-Ninth International Joint Conference on Artificial Intelligence \(IJCAI\),Cited by:[§1](https://arxiv.org/html/2609.27203#S1.p1.1),[§11\.1](https://arxiv.org/html/2609.27203#S11.SS1.p1.1)\.