Skolemisation for Intuitionistic Linear Logic

TL;DR

This paper introduces a focused variant of first-order intuitionistic linear logic and presents a sound and complete skolemisation procedure to improve proof search efficiency.

Contribution

It develops a novel focused version of first-order intuitionistic linear logic and provides the first practical skolemisation method for it.

Findings

Sound and complete skolemisation procedure for focused intuitionistic linear logic

Enhanced proof search efficiency through skolemisation

Formal framework for skolemisation in linear logic

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.