=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== https://ceur-ws.org/Vol-3875/ARQNL2024_preface.pdf
                                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