Stellar Resolution: Multiplicatives

TL;DR

Stellar Resolution introduces an asynchronous computation model based on first-order unification, formalizing Girard's transcendental syntax and generalizing traditional models like logic programming and Wang tilings.

Contribution

It provides the first formalization of Stellar Resolution, connecting Girard's syntax programme to models of logic and proof-structures, and extends to semantics for Multiplicative Linear Logic.

Findings

Formal definitions and properties of Stellar Resolution established

Demonstrates how it generalizes logic programming and tilings

Provides semantics for Multiplicative Linear Logic

Abstract

We present a new asynchronous model of computation named Stellar Resolution based on first-order unification. This model of computation is obtained as a formalisation of Girard's transcendental syntax programme, sketched in a series of three articles. As such, it is the first step towards a proper formal treatment of Girard's proposal to tackle first-order logic in a proofs-as-program approach. After establishing formal definitions and basic properties of stellar resolution, we explain how it generalises traditional models of computation, such as logic programming and combinatorial models such as Wang tilings. We then explain how it can represent multiplicative proof-structures, their cut-elimination and the correctness criterion of Danos and Regnier. Further use of realisability techniques lead to dynamic semantics for Multiplicative Linear Logic, following previous Geometry of Interaction models.