Using Z3 to Verify Inferences in Fragments of Linear Logic

TL;DR

This paper introduces a method using the Z3 theorem prover to verify inference rules in fragments of linear logic, enhancing the reliability of logical reasoning in applications like programming and quantum physics.

Contribution

It presents a template for verifying linear logic inference rules with Z3, applied to MLL+Mix and MILL fragments, advancing automated proof validation techniques.

Findings

Successfully verified inference rules in MLL+Mix and MILL fragments.

Demonstrated the effectiveness of Z3 in linear logic inference validation.

Provided a framework for automated checking of logical inference rules.

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 [8] 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: MLL+Mix (Multiplicative Linear Logic extended with a Mix rule) and MILL (Multiplicative Intuitionistic Linear Logic).