Skolemisation of Intuitionistic Linear Logic

Alessandro  Bruni; Eike Ritter; Carsten Schürmann

doi:10.1007/978-3-031-63501-4_4

Skolemisation of Intuitionistic Linear Logic

Alessandro Bruni, Eike Ritter^*, Carsten Schürmann

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

3 Downloads (Pure)

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.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part II
Editors	Christoph Benzmüller, Marijn J.H. Heule, Renate A. Schmidt
Publisher	Springer
Pages	61-77
Number of pages	17
Edition	1
ISBN (Electronic)	9783031635014
ISBN (Print)	9783031635007
DOIs	https://doi.org/10.1007/978-3-031-63501-4_4
Publication status	E-pub ahead of print - 1 Jul 2024
Event	12th International Joint Conference on Automated Reasoning, IJCAR 2024 - Inria Nancy Research Center and LORIA, Nancy, France Duration: 1 Jul 2024 → 6 Jul 2024

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	14740
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th International Joint Conference on Automated Reasoning, IJCAR 2024
Abbreviated title	IJCAR 2024
Country/Territory	France
City	Nancy
Period	1/07/24 → 6/07/24

Keywords

Skolemisation
Linear logic

ASJC Scopus subject areas

Computational Theory and Mathematics

Access to Document

10.1007/978-3-031-63501-4_4Licence: Creative Commons: Attribution (CC BY)

BruniA2024SkolemisationFinal published version, 468 KBLicence: Creative Commons: Attribution (CC BY)

Cite this

Bruni, A., Ritter, E., & Schürmann, C. (2024). Skolemisation of Intuitionistic Linear Logic. In C. Benzmüller, M. J. H. Heule, & R. A. Schmidt (Eds.), Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part II (1 ed., pp. 61-77). (Lecture Notes in Computer Science; Vol. 14740). Springer. Advance online publication. https://doi.org/10.1007/978-3-031-63501-4_4

Bruni, Alessandro ; Ritter, Eike ; Schürmann, Carsten. / Skolemisation of Intuitionistic Linear Logic. Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part II. editor / Christoph Benzmüller ; Marijn J.H. Heule ; Renate A. Schmidt. 1. ed. Springer, 2024. pp. 61-77 (Lecture Notes in Computer Science).

@inproceedings{745be73207934151a40e56e405c17b3f,

title = "Skolemisation of Intuitionistic 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.",

keywords = "Skolemisation, Linear logic",

author = "Alessandro Bruni and Eike Ritter and Carsten Sch{\"u}rmann",

year = "2024",

month = jul,

day = "1",

doi = "10.1007/978-3-031-63501-4_4",

language = "English",

isbn = "9783031635007",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "61--77",

editor = "Christoph Benzm{\"u}ller and Heule, {Marijn J.H.} and Schmidt, {Renate A.}",

booktitle = "Automated Reasoning",

edition = "1",

note = "12th International Joint Conference on Automated Reasoning, IJCAR 2024, IJCAR 2024 ; Conference date: 01-07-2024 Through 06-07-2024",

}

Bruni, A, Ritter, E & Schürmann, C 2024, Skolemisation of Intuitionistic Linear Logic. in C Benzmüller, MJH Heule & RA Schmidt (eds), Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part II. 1 edn, Lecture Notes in Computer Science, vol. 14740, Springer, pp. 61-77, 12th International Joint Conference on Automated Reasoning, IJCAR 2024, Nancy, France, 1/07/24. https://doi.org/10.1007/978-3-031-63501-4_4

Skolemisation of Intuitionistic Linear Logic. / Bruni, Alessandro ; Ritter, Eike; Schürmann, Carsten.
Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part II. ed. / Christoph Benzmüller; Marijn J.H. Heule; Renate A. Schmidt. 1. ed. Springer, 2024. p. 61-77 (Lecture Notes in Computer Science; Vol. 14740).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Skolemisation of Intuitionistic Linear Logic

AU - Bruni, Alessandro

AU - Ritter, Eike

AU - Schürmann, Carsten

PY - 2024/7/1

Y1 - 2024/7/1

N2 - 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.

AB - 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.

KW - Skolemisation

KW - Linear logic

UR - https://merz.gitlabpages.inria.fr/2024-ijcar/

UR - https://merz.gitlabpages.inria.fr/2024-ijcar/post/call-for-papers/

U2 - 10.1007/978-3-031-63501-4_4

DO - 10.1007/978-3-031-63501-4_4

M3 - Conference contribution

SN - 9783031635007

T3 - Lecture Notes in Computer Science

SP - 61

EP - 77

BT - Automated Reasoning

A2 - Benzmüller, Christoph

A2 - Heule, Marijn J.H.

A2 - Schmidt, Renate A.

PB - Springer

T2 - 12th International Joint Conference on Automated Reasoning, IJCAR 2024

Y2 - 1 July 2024 through 6 July 2024

ER -

Bruni A, Ritter E, Schürmann C. Skolemisation of Intuitionistic Linear Logic. In Benzmüller C, Heule MJH, Schmidt RA, editors, Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part II. 1 ed. Springer. 2024. p. 61-77. (Lecture Notes in Computer Science). Epub 2024 Jul 1. doi: 10.1007/978-3-031-63501-4_4

Skolemisation of Intuitionistic Linear Logic

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this