Grounds of Stellar Resolution (Transcendental Syntax) Transcendental Syntax is a program proposed and started by Girard aiming for logic (linear logic, in particular) reconstruction. The idea is to go the "opposite way", forget all the logic rules, connectives etc. and to build it (logic) from computational terms. Later, there were 4 papers published by Girard expanding his ideas (called "Transcendental Syntax I-IV:...").
Moreover, recently B. Eng and T. Seiller started the formalization of those ideas using the newly proposed model of computation, called "Stellar Resolution" (SR). As name proposes, the model heavily utilizes the notion of Robinson's first-order resolution.
Assuming someone is familiar with these works, the questions are the following:

*

*As even noted in the paper Stellar Resolution: Multiplicatives the model is quite similar but differs from it in several way: firstly, the Robinson's resolution has a reference to logic and aims reaching the empty clause and, secondly, it computes differently. If one changes the goal of reaching the empty clause to the one in SR (i.e. "reaching atoms that we can infer") will it become much closer to Robinson's resolution (or even identical)? And in what sense does SR computes differently?


*In the paper A gentle introduction to Girard’s Transcendental Syntax for the linear logician it is mentioned in the beginning that the other model could have been chosen. What does it actually mean and how one should have gone with the other one? I.e. is it really necessary to choose the model which is close to resolution method, or one may even choose the lambda calculus, extend its syntax (to have some similar notions) and reach the same goal?
The goal is merely to deeply understand the ideas behind SR model.
 A: (I'll just answer question 2.) For context you should know that Girard has been trying to "reconstruct logic from computation/interaction" for a long time. Some old programmatic papers where you can find that ambition stated are:

*

*Towards a geometry of interaction (1989)

*On the meaning of logical rules I : syntax vs. semantics (1999)

The research outlined in the first paper led to various "geometry of interaction" (GoI) models of linear logic while the second led to ludics. The computational objects in GoI are some kind linear operators from functional analysis, and the construction was later generalized in various ways to quite different settings (see Haghverdi and Scott's tutorial for a general category-theoretic recipe). Ludics "reconstructs logic" (technically: gives a fully complete semantics for (polarized Multiplicative-Additive) Linear Logic) using artifacts that look like infinitary sequent calculus proofs or game-semantical strategies, depending on your point of view.
So you can see that there is a variety of choices for the untyped computational universe that you can start from. The advantage of using first-order terms is that they are finite objects, which allows for concrete/effective manipulation, something that Girard has come to consider philosophically important according to his transcendental syntax manifesto (in French).
Aside from the finiteness/effectivity requirement, I don't see any deep reason to use something specifically based on unification/resolution, rather than some other combinatorial device. I guess it's just that Girard is a fan of Herbrand's work? (Also, there is a GoI model based on a "resolution semiring" in Marc Bagnol's PhD thesis supervised by Girard, which is a bit different from the stars and constellations in transcendental syntax. I believe the idea goes back to the GoI3 paper where an operator algebra is built from resolution.)
