=Paper=
{{Paper
|id=Vol-3326/ARQNL2022_preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-3326/ARQNL2022_preface.pdf
|volume=Vol-3326
}}
==None==
https://ceur-ws.org/Vol-3326/ARQNL2022_preface.pdf
Christoph Benzmüller
Jens Otten (Eds.)
Automated Reasoning in
Quantified Non-Classical Logics
4th International Workshop, ARQNL 2022,
Haifa, Israel, August 11th, 2022
Proceedings
Originally published online by
CEUR Workshop Proceedings (CEUR-WS.org)
Automated Reasoning in Quantified Non-Classical Logics ARQNL 2022
Preface
This volume contains the proceedings of the Fourth International Workshop on Automated Rea-
soning in Quantified Non-Classical Logics (ARQNL 2022), held August 11th, 2022, in Haifa,
Israel. The workshop was affiliated and co-located with the International Joint Conference
on Automated Reasoning (IJCAR 2022), which was part of the Federated Logic Conference
(FLoC 2022). The aim of the ARQNL 2022 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. For many propositional
non-classical logics there exist proof calculi and ATP systems. Often proof search in these
logics is significantly more difficult than in classical logic. For first-order and higher-order
non-classical logics the mechanization and automation of proof search is even more challeng-
ing. Furthermore, extending existing non-classical propositional calculi, proof techniques and
implementations to quantified logics is often not straightforward. As a result, for most quanti-
fied non-classical logics there exist no or only few (efficient) ATP systems. 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 2022 Workshop received seven paper submissions. Each paper was reviewed
by at least three referees, and following an online discussion, six research papers were selected
to be included in the proceedings. The ARQNL 2022 Workshop included invited talks by
Tomer Libal (“Do Lawyers Use Automated Reasoning?”) and Renate Schmidt (“Advances
and Challenges in the Development and Application of Forgetting Tools”). Additionally, one
research paper was selected for presentation at the workshop.
We would like to sincerely thank the invited speakers, all authors for their contributions
and all active participants of the ARQNL 2022 workshop. We would also like to thank the
members of the Program Committee of ARQNL 2022 for their professional work in the re-
view process. Furthermore, we would like to thank the IJCAR Workshop co-chairs Shaull
Almagor and Guillermo Pérez and the local organizers of FLoC 2022. Finally, we would like
to acknowledge the support of the EasyChair conference management system.
Bamberg and Oslo Christoph Benzmüller
August 2022 Jens Otten
ii
Automated Reasoning in Quantified Non-Classical Logics ARQNL 2022
Organization
Program Committee
Carlos Areces Universidad Nacional de Córdoba, Argentina
Christoph Benzmüller University of Bamberg, Germany – co-chair
Christian Fermüller Vienna University of Technology, Austria
Didier Galmiche Université de Lorraine - LORIA, France
Marianna Girlando University of Birmingham, UK
Andreas Herzig University of Toulouse - IRIT-CNRS, France
Annika Kanckos University of Helsinki, Finland
Stephan Merz INRIA Nancy, France
Larry Moss Indiana University Bloomington, USA
Hans De Nivelle Nazarbayev University, Kazakhstan
Jens Otten University of Oslo, Norway – co-chair
Fabio Papacchini Lancaster University Leipzig, Germany
Xavier Parent Vienna University of Technology, Austria
Revantha Ramanayake University of Groningen, Netherlands
Alexander Steen University of Greifswald, Germany
Luca Viganò King’s College London, UK
Editors & Workshop Chairs
Christoph Benzmüller
University of Bamberg (and Freie Universität Berlin)
An der Weberei 5, 96047 Bamberg, Germany
E-mail: christoph.benzmueller@uni-bamberg.de
Web: http://christoph-benzmueller.de
Jens Otten
Department of Informatics
University of Oslo
Gaustadalléen 23 B, 0373 Oslo, Norway
E-mail: jeotten@ifi.uio.no
Web: http://jens-otten.de
iii
Automated Reasoning in Quantified Non-Classical Logics ARQNL 2022
Contents
Do Lawyers Use Automated Reasoning? 1–10
Tomer Libal
Advances and Challenges in the Development and Application of Forgetting Tools
(Abstract) 11–12
Renate A. Schmidt
Towards a Coq Formalization of a Quantified Modal Logic 13–27
Ana de Almeida Borges
Reasoning in Non-normal Modal Description Logics 28–45
Tiziano Dalmonte, Andrea Mazzullo and Ana Ozaki
Intuitionistic Derivability in Anderson’s Variant of the Ontological Argument 46–63
Annika Kanckos
(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems 64–80
Thomas Neele
Advancing Automated Theorem Proving for the Modal Logics D and S5 81–91
Jens Otten
Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results 92–108
Xavier Parent and Christoph Benzmüller
iv