=Paper= {{Paper |id=Vol-3613/AReCCa2023_preface |storemode=property |title=AReCCa 2023 - Automated Reasoning with Connection Calculi |pdfUrl=https://ceur-ws.org/Vol-3613/AReCCa2023_preface.pdf |volume=Vol-3613 |authors=Jens Otten,Wolfgang Bibel |dblpUrl=https://dblp.org/rec/conf/arecca/X23 }} ==AReCCa 2023 - Automated Reasoning with Connection Calculi== https://ceur-ws.org/Vol-3613/AReCCa2023_preface.pdf
                                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