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