=Paper=
{{Paper
|id=Vol-3875/ARQNL2024_preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-3875/ARQNL2024_preface.pdf
|volume=Vol-3875
}}
==None==
Christoph Benzmüller
Jens Otten
Revantha Ramanayake (Eds.)
Automated Reasoning in
Quantified Non-Classical Logics
5th International Workshop, ARQNL 2024,
Nancy, France, July 1st, 2024
Proceedings
Originally published online by
CEUR Workshop Proceedings (CEUR-WS.org)
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
Automated Reasoning in Quantified Non-Classical Logics ARQNL 2024
Preface
This volume contains the proceedings of the Fifth International Workshop on Automated Rea-
soning in Quantified Non-Classical Logics (ARQNL 2024), held July 1st, 2024, in Nancy,
France. The workshop was affiliated and co-located with the International Joint Conference
on Automated Reasoning (IJCAR 2024). The aim of the ARQNL 2024 Workshop has been to
foster the development of proof calculi, automated theorem proving (ATP) systems and model
finders for all sorts of quantified non-classical logics. The ARQNL workshop series provides
a forum for researchers to present and discuss recent developments in this area.
Non-classical logics — such as modal logics, conditional logics, intuitionistic logic, de-
scription logics, temporal logics, linear logic, multivalued logic, dynamic logic, deontic logic,
fuzzy logic, paraconsistent logic, relevance logic, free logic, natural logic — have many appli-
cations in Artificial Intelligence, Computer Science, Philosophy, Linguistics, and Mathematics.
Hence, the automation of proof search in these logics is a crucial task. It is in particular the aim
of the ARQNL workshop series to initiate and foster practical implementations and evaluations
of such ATP systems for non-classical logics.
The ARQNL 2024 Workshop received eight paper submissions. Each paper was reviewed
by at least three referees, and following an online discussion, all eight research papers were
selected to be included in the proceedings. The ARQNL 2024 Workshop included invited talks
by Didier Galmiche (“Separation Logics: Semantics and Proofs”) and Amir Akbar Tabatabai
(“On the Computational Content of Intuitionistic Modal Proofs”).
We would like to sincerely thank the invited speakers, all authors for their contributions and
all active participants of the ARQNL 2024 workshop. We would also like to thank the mem-
bers of the Program Committee of ARQNL 2024 for their professional work in the reviewing
process. Finally, we would like to acknowledge the support of the EasyChair conference man-
agement system.
Christoph Benzmüller
Bamberg, Oslo and Groningen
Jens Otten
July 2024
Revantha Ramanayake
ii
Automated Reasoning in Quantified Non-Classical Logics ARQNL 2024
Organization
Program Committee
Christoph Benzmüller University of Bamberg, Germany – co-chair
Ana de Almeida Borges University of Barcelona, Spain
Camillo Fiorentini University of Milano, Italy
Marianna Girlando University of Amsterdam, Netherlands
Andrzej Indrzejczak University of Lodz, Poland
Annika Kanckos University of Helsinki, Finland
Dominik Kirst Ben-Gurion University, Israel
Timo Lang University College London, UK
Tomer Libal University of Luxembourg and Enidia AI
Larry Moss Indiana University Bloomington, USA
Nicola Olivetti Aix-Marseille University, France
Jens Otten University of Oslo, Norway – co-chair
Xavier Parent Vienna University of Technology, Austria
Revantha Ramanayake University of Groningen, Netherlands – co-chair
Ramaswamy Ramanujam Institute of Mathematical Sciences, Chennai, India
Editors & Workshop Chairs
Christoph Benzmüller
University of Bamberg (and Freie Universität Berlin)
E-mail: c.benzmueller@gmail.com
Web: http://christoph-benzmueller.de
Jens Otten
University of Oslo (and Potassco Solutions)
E-mail: jeotten@jens-otten.de
Web: https://jens-otten.de
Revantha Ramanayake
University of Groningen
E-mail: d.r.s.ramanayake@rug.nl
Web: https://rug.nl/staff/d.r.s.ramanayake/
iii
Automated Reasoning in Quantified Non-Classical Logics ARQNL 2024
Contents
Separation Logics: Semantics and Proofs 1–4
Didier Galmiche
On the Computational Content of Intuitionistic Modal Proofs 5
Amir Akbar Tabatabai
A Fresh Look at Relevant Number Theory 6–13
John Slaney
Implementing Intermediate Logics 14–23
Bastiaan Haaksema, Jens Otten and Revantha Ramanayake
Automated Proof Search in Intuitionistic Sentential Logic 24–37
Didier Galmiche, Brandon Hornbeck and Daniel Méry
Implementing the Fatio Protocol for Multi-Agent Argumentation in LogiKEy 38–47
Luca Pasetto and Christoph Benzmüller
Bisequent Calculi for Neutral Free Logic with Definite Descriptions 48–61
Andrzej Indrzejczak and Yaroslav Petrukhin
When Epsilon meets Lambda: Extended Leśniewski’s Ontology 62–79
Andrzej Indrzejczak
On Regular Relations in Parametric Array Theories 80–91
Rodrigo Raya
A Proof-Theoretical Approach to Some Extensions of First Order Quantification 92–107
Loı̈c Allègre, Ophélie Lacroix and Christian Retoré
iv