  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.
