constellation $\bar{G}$ defined as the multiset $\alpha: E\rightarrow \bar{e}$.

One can check that this encoding has the property that diagrams $\rho: T\rightarrow U(\bar{G})$ in which $T$ is a *linear graph* (i.e. a graph $\bullet \rightarrow \bullet\rightarrow \dots\rightarrow\bullet$) are in bijection with walks in $G$; moreover the diagram is saturated if and only if the walk is *maximal*.

### Logic programming

The stellar resolution is very close to concepts coming from logic programming since they all use first-order terms to do computations. The main difference is that logic programming has practical motivations and enjoy logical interpretations through model theory while our approach is purely computational and doesn’t obey logic. We choose to encode first-order disjunctive clauses [@robinson1965machine].

We have the following encoding for first-order atoms: $P(t_1, ..., t_n)^\bigstar = +P(t_1, ..., t_n)$, as well as $(\lnot P(t_1, ..., t_n))^\bigstar = -P(t_1, ..., t_n)$ where $P$ is a colour. A clause is encoded as $\{A_1, ..., A_n\}^\bigstar = \gstar{A_1^\bigstar, ..., A_n^\bigstar}$ where $A_1, ..., An$ are first-order atoms. A set of clauses is translated into $\{C_1, ..., C_n\}^\bigstar = C_1^\bigstar + ... + C_n^\bigstar$. Clauses are connected through the resolution rule: from $\Gamma \cup \{P(t_1, ..., t_n)\}$ and $\Delta \cup \{\lnot P(u_1, 