Skolemisation for Intuitionistic Linear Logic
<|reference_start|>Skolemisation for Intuitionistic Linear Logic: 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.<|reference_end|>
@article{bruni2024skolemisation,
    title={Skolemisation for Intuitionistic Linear Logic},
    author={Alessandro Bruni and Eike Ritter and Carsten Sch"urmann},
    journal={arXiv preprint arXiv:2405.01375},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.01375},
    primaryClass={cs.LO}
}