On November 2, 2023 at 14:00 EET, Mihai Prunescu (University of Bucharest) will give a talk in the Logic Seminar.
Title: Using Z3 to Verify Inferences in Fragments of Linear Logic
Abstract:
Linear logic is a substructural logic proposed as a refinement of classical and intuitionistic logics, with applications in programming languages, game semantics, and quantum physics. We present a template for Gentzen-style linear logic sequents that supports verification of logic inference rules using automatic theorem proving. Specifically, we use the Z3 Theorem Prover to check targeted inference rules based on a set of inference rules that are presumed to be valid. To demonstrate the approach, we apply it to validate several derived inference rules for two different fragments of linear logic: \(\mathsf{MLL+Mix}\) (Multiplicative Linear Logic extended with a Mix rule) and \(\mathsf{MILL}\) (Multiplicative Intuitionistic Linear Logic).
The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.