Skolemisation for Intuitionistic Linear Logic

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

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 backtracking 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.
Original languageEnglish
Title of host publicationInternational Joint Conference on Automated Reasoning
PublisherSpringer Nature
Publication date2024
DOIs
Publication statusPublished - 2024

Fingerprint

Dive into the research topics of 'Skolemisation for Intuitionistic Linear Logic'. Together they form a unique fingerprint.

Cite this