..., u_n)\}$, we infer $\theta(\Gamma \cup \Delta)$ where $\theta = \unifalgo{\{t_i \doteq u_i\}_{1 \leq i \leq n}}$.

The actualisation of a diagram corresponds to several applications of the resolution rule. In particular, a saturated diagram is a full computation (instead of a partial/unfinished computation). The unification graph we use is reminiscent of dependency graphs [@nguyen2007termination; @dimopoulos1996graph] and the normalisation of the computation of answer sets [@gelfond2008answer; @eiter2009answer]. Although not described here, it may also be possible to simulate goal-directed inferences (such as SLD [@kowalski1974predicate] or SLO [@lobo1991semantics] resolution) by using unpolarised rays.

Another close model is the model of flows [@girard1995geometry; @bagnol2014resolution] made of couples of terms $t \leftharpoonup u$ where $t$ and $u$ have exactly the same variables.

Let $f = t \leftharpoonup u$ be a flow. We define its encoding as $f^\bigstar = \gstar{+t, -u}$. A wiring $F = f_1+...+f_n$ is a set of flows and it is encoded into $F^\bigstar = f_1^\bigstar + ... + f_n^\bigstar$.

A wiring will describe a graph where flows represent edges. Matching (definition \[def:matching\]) decides which vertices the edges connect. The execution of a wiring $\exec(F)$ computing maximal paths in corresponding graph corresponds to $\exec(F^\bigstar)$.

### Wang tiles and abstract tile assembly 