Skolemisation for Intuitionistic Linear Logic

TL;DR

The paper tackles backtracking caused by first-order quantifier instantiations in focused, polarised intuitionistic linear logic ($LJF$). It introduces $SLJF$, a quantifier-free skolemised variant that encodes quantifier dependencies via explicit substitutions and enforces admissibility through unification at axioms. A constructive skolemisation procedure maps $LJF$ proofs to $SLJF$ proofs and is proven sound and complete, ensuring provability is preserved while reducing quantifier-order backtracking. This advances proof search in first-order linear logic and offers practical benefits for theorem provers like Imogen.

Abstract

Focusing is a known technique for reducing the number of proofs while preserving derivability. Skolemisation is another technique designed to improve proof search, which reduces the number of back-tracking steps by representing dependencies on the term level and instantiate witness terms during unification at the axioms or fail with an occurs-check otherwise. Skolemisation for classical logic is well understood, but a practical skolemisation procedure for focused intuitionistic linear logic has been elusive so far. In this paper we present a focused variant of first-order intuitionistic linear logic together with a sound and complete skolemisation procedure.

Figures (7)

• Figure 1: Focused intuitionistic linear logic (LJF)
• Figure 2: Example \ref{['ex:a']}, unique and complete proof
• Figure 3: Typing rules for substitutions
• Figure 4: Skolemised intuitionistic linear logic
• Figure 5: Example \ref{['ex:e']}, unique complete proof

Theorems & Definitions (25)

• theorem 1: Focusing
• definition 1: Free Variables
• definition 2: Admissibility
• definition 3: Proof Theory
• lemma 1: Weakening
• proof
• lemma 2: Admissibility of $\mathbin{\otimes}$R
• proof
• lemma 3: Admissibility of $\hbox{$-\!\circ$}$L
• proof