Skolemisation for Intuitionistic Linear Logic

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer 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.
OriginalsprogEngelsk
TitelInternational Joint Conference on Automated Reasoning
ForlagSpringer Nature
Publikationsdato2024
DOI
StatusUdgivet - 2024

Fingeraftryk

Dyk ned i forskningsemnerne om 'Skolemisation for Intuitionistic Linear Logic'. Sammen danner de et unikt fingeraftryk.

Citationsformater