Related papers: Linear Logic and the Hilbert Scheme
We prove a completeness result for Multiplicative Exponential Linear Logic (MELL): we show that the relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized…
Each Multiplicative Exponential Linear Logic (MELL) proof-net can be expanded into a differential net, which is its Taylor expansion. We prove that two different MELL proof-nets have two different Taylor expansions. As a corollary, we prove…
We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose a constraint on some paths, we can bound the size of all the nets satisfying this…
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing (and deciding in the finite case) those sets of…
The diagonal in a product of projective spaces is cut out by the ideal of 2x2-minors of a matrix of unknowns. The multigraded Hilbert scheme which classifies its degenerations has a unique Borel-fixed ideal. This Hilbert scheme is generally…
HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL)…
We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality B to capture mixed-state quantum computation. The language supports algebraic constructs such as linear combinations,…
The Hilbert scheme $S^{[n]}$ of points on an algebraic surface $S$ is a simple example of a moduli space and also a nice (crepant) resolution of singularities of the symmetric power $S^{(n)}$. For many phenomena expected for moduli spaces…
Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions frequently contain errors that cannot be automatically checked. Formal theorem proving systems such as Lean 4 offer automated…
We show that for Multiplicative Exponential Linear Logic (without weakenings) the syntactical equivalence relation on proofs induced by cut-elimination coincides with the semantic equivalence relation on proofs induced by the multiset based…
We give a new proof the arithmetic Hilbert-Samuel theorem by using classical reductions in the theory of coherent sheaves, a direct proof in the case of the projective space and the conservation of some numerical invariants, called…
Linear logic has provided new perspectives on proof-theory, denotational semantics and the study of programming languages. One of its main successes are proof-nets, canonical representations of proofs that lie at the intersection between…
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are…
A pair of disjoint lines on a smooth cubic threefold determines an irreducible component of the Hilbert scheme. We prove that this component is smooth and isomorphic to the blow-up of the symmetric product of Fano varieties of lines on the…
The article explores the arithmetic of multiplication as a model of many valued projective logic. It is demonstrated that closed numerical intervals within this framework constitute Heyting algebras. The conditions for these algebras to be…
We show that a proof in multiplicative linear logic can be represented as a decorated surface, such that two proofs are logically equivalent just when their surfaces are geometrically equivalent. This is an extended abstract for…
In this paper we investigate two logics from an algebraic point of view. The two logics are: MALL (multiplicative-additive Linear Logic) and LL (classical Linear Logic). Both logics turn out to be strongly algebraizable in the sense of Blok…
We introduce estimation and test procedures through divergence minimization for models satisfying linear constraints with unknown parameter. Several statistical examples and motivations are given. These procedures extend the empirical…
In this article, we study properties of the exponential Hilbert series of a $G$-equivariant projective variety, where $G$ is a semisimple, simply-connected complex linear algebraic group. We prove a relationship between the exponential…
We work out details of the extrinsic geometry for two Hilbert schemes of some contemporary interest: the Hilbert scheme of two points on the projective plane and the dense open set parametrizing non-planar clusters in the punctual Hilbert…