AReCCa 2023 – Automated Reasoning with Connection Calculi Jens Otten1 , Wolfgang Bibel2 1 Department of Informatics, University of Oslo, Norway 2 Technical University of Darmstadt, Germany This volume contains the proceedings of the First International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023), held 18 September 2023 in Prague, Czech Republic. The workshop was affiliated and co-located with the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023. The aim of the AReCCa 2023 Workshop has been to foster the development of connection calculi and systems based on them for automated theorem proving (ATP). It provided a forum for researchers to present and discuss recent developments in this area. Beforehand it seems worthwhile to summarize in a few sentences the area’s pertinent historical background. The formalization of human reasoning by way of a logical framework has a tradition reaching back more than two thousand years [1]. Supporting calculations by mechanical devices looks back to a similarly long tradition [2]. Applying such mechanical devices to logical reasoning, i.e. the combination of the two just mentioned traditions, has first been pioneered about 150 years ago [3, p.60], but has restarted its successful path only about 75 years ago [4]. Today, the automation of logical reasoning is a blossoming discipline, variably called Automated Deduction (AD), Automated Reasoning (AR), or Automated Theorem Proving (ATP). It is one of the subdisciplines of the science Artificial Intelligence (AI). As described in detail in [5, Sect.2], the first automated provers for first-order logic (fol), built in the 1950s, may be regarded as derivatives from Gentzen’s calculus of natural deduction (NK) [6]. Due to the relatively high number of proof rules, these provers turned out to become appallingly complicated. Given this background, the discovery of resolution as a single rule for achieving the same function [7] was hailed as a great improvement in the 1960s. Thus started the triumphant advance of resolution as the leading proof method for ATP up to this day. In the 1970s the line of research in ATP derived from NK was resumed by two researchers; they independently achieved an abstraction of the NK-calculus which simplified the resulting calculus substantially with the potential of becoming competitive with resolution, one under the term of matings [8], the other termed connection method (CM) [9]. This approach to ATP has been explored extensively in the decades thereafter, both theoretically and experimentally, leading to a wide range of promising results. Calculi based on the connection method, their development and implementations are the AReCCa 2023: Automated Reasoning with Connection Calculi, 18 September 2023, Prague, Czech Republic $ jeotten@ifi.uio.no (J. Otten); bibel@gmx.net (W. Bibel) € http://jens-otten.de/ (J. Otten)  0000-0002-4331-8698 (J. Otten); 0000-0003-3892-0171 (W. Bibel) © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) AReCCa 2023 1 CEUR-WS.org CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings topical focus in the present volume. As already mentioned, the papers collected therein are the outcome of the AReCCa 2023 Workshop. It was initiated by the first of the present authors, featured a program committee consisting of 14 leading researchers, a one day program with 9 talks, and assembled around two dozens of researchers. In detail, the volume presents the work contained in the following 9 papers. During the last decades quite a few systems implementing the CM have been built. Among those the series of systems derived from leanCoP may be regarded as representative in various respects. The paper by Jens Otten presents a comprehensive overview of this series of very successful systems consisting of just several lines of Prolog code. In these kinds of proof systems like leanCoP backtracking is an important technical ingredient. Michael Färber has developed a novel, comparatively less restricted backtracking strategy based on the notion of exclusive cuts which has been integrated in a new prover called meanCoP, leading to an amazing improvement in performance as demonstrated on several standard benchmarks. Arithmetic is one of the most important extensions for first-order logics. The paper by Leo Repp et al. presents the system nanoCoP-Omega, an extension of the non-clausal connection prover nanoCoP for classical first-order logic, that can deal with typed linear integer arithmetic. The prover thus can handle arithmetic calculations and equations. The paper by Clemens Eisenhofer et al. investigates a very general syntactic approach to searching for proofs in certain kinds of logical calculi by use of an SMT solver. Using Z3’s support for user propagation, proofs in a user-specified calculus, such as a connection calculus, can be found automatically via Z3’s internal satisfiability procedures. The work by Christoph Wernhard has recently extended the potential of CM provers in a substantial way. By an interplay of goal- and axiom-driven processing it features lemma re-use and heuristic restrictions known from saturating provers. It produces remarkably short proofs, is competitive with other leading systems on the chosen domain of condensed detachment problems, and was able to solve an ATP challenge problem fully automatically for the first time. Jens Otten et al. in their contribution propose a unified format for connection proofs. Their proposed syntax generalizes the existing leantptp syntax and is a better fit to the TPTP con- ventions. Agreement on such a common syntax for solutions significantly simplifies tool development and interoperability. Sean Holden describes the system Connect++, an automated theorem prover for first-order logic with equality, based on a clausal connection calculus. By coding it in the compiled language C++, the work aims at fast system performance. In its design the additional goal of supporting the integration of machine learning mechanisms has been taken into consideration. The paper by Fredrik Rømming et al. describes a Python framework for combining reinforce- ment learning methods with connection calculi for classical, intuitionistic, and modal logic, based on several versions of the leanCoP system. The paper summarizes the MDP (Markov Decision Process) setting, discusses its mapping to the various connection calculi, and provides a Python library implementing such MDPs. The concluding paper by Wolfgang Bibel analyses and compares on a high level of abstraction significant features of the leading proof methods resolution, tableaux, and the connection method in Automated Theorem Proving. It aims at the identification of promising areas of research in order to further advance the field. 2 We thank all authors, but also the workshop participants for their valuable contributions and for their collaboration in this project towards advancing the field by contributing to the further development of the connection method. Particularly, we also thank all members of the Program Committee for their professional work guaranteeing a high level of quality of the papers accepted for the workshop and eventually for the Proceedings. Each of the papers contained in this volume has been reviewed by three independent referees in the standard anonymous manner. Last but not least, we thank the organizing team of TABLEAUX 2023 in Prague for their perfect arrangements which made the attendance of the workshop and its surrounding events a really pleasant and memorable one. Finally, we would like to acknowledge the support of the EasyChair conference management system. Oslo and Scheidegg, December 2023 Jens Otten and Wolfgang Bibel References [1] W. Kneale, M. Kneale, The Development of Logic, Clarendon Press, Oxford, 1984. [2] H. Bruderer, Milestones in Analog and Digital Computing, volume 1 and 2, 3 ed., Springer Nature Swizzerland, Cham, 2020. [3] W. S. Jevons, The Substitution of Similars – The True Principle of Reasoning, Derived from a Modification of Aristotle’s Dictum, Macmillan, Cambridge, 1869. [4] K. Zuse, Über den Plankalkül als Mittel zur Formulierung schematisch kombinativer Aufgaben, Archiv der Mathematik 1 (1948) 441–449. [5] W. Bibel, Early history and perspectives of automated deduction, in: J. Hertzberg, M. Beetz, R. Englert (Eds.), Proceedings of the 30th Annual German Conference on Artificial Intelligence (KI-2007), volume 4667 of LNAI, Springer, Berlin, 2007, pp. 2–18. [6] G. Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39 (1935) 176–210 and 405–431. Engl. transl. in [10]. [7] J. A. Robinson, A machine-oriented logic based on the resolution principle, Journal of ACM 12 (1965) 23–41. Also contained in [11, 397–415]. [8] P. B. Andrews, Theorem proving via general matings, Journal of the ACM 28 (1981) 193–214. [9] W. Bibel, Matings in matrices, Comm. ACM 26 (1983) 844–852. [10] M. E. Szabo (Ed.), The collected papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969. [11] J. Siekmann, G. Wrightson (Eds.), Automation of Reasoning – Classical Papers on Compu- tational Logic 1957–1966, volume 1, Springer, Berlin, 1983. 3