claim great improvements, proposing in particular a Curry-Howard interpretation of first-order logic [@girard2016transcendental3]. However, these articles are too inexact in form to serve satisfactorily as the basis of a mathematical theory[^2]. The current work is the first step towards a proper formal account of the model, with underlying motivation the representation of first-order logic and its possible applications in relation with descriptive complexity results [@immerman2012descriptive], such as the Immerman-Vardi theorem [@vardi1982complexity; @immermann1986relational].

**Contributions.** We formally describe a model of computation named stellar resolution, which extends the model of computation vaguely described by Girard. We prove the main properties of the model. In particular, while Girard claimed the failure of the Church-Rosser property, we are able to prove it holds for stellar resolution (Theorem \[thm:associativity\]). We also relate it to standard models of computation such as Wang tilings [@wang1961proving] and abstract tiles assembly models [@winfree1998algorithmic; @patitz2014introduction], which have applications in bio-computing [@seeman1982nucleic; @woods2019diverse]. We then explain how this model captures the dynamics of cut-elimination for MLL, the multiplicative fragment of linear logic (Theorem \[def:dynamics\]), and the correctness criterion for proof-structures – a syntax for MLL (Theorem \[thm:correctness2\]). Lastly, we explain how realisability techniques similar to those used in $\lambda$-calculus can be 