Jens Otten Wolfgang Bibel (Eds.) Automated Reasoning with Connection Calculi 1st International Workshop, AReCCa 2023, Prague, Czech Republic, September 18th, 2023 Proceedings Originally published online by CEUR Workshop Proceedings (CEUR-WS.org) CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings Automated Reasoning with Connection Calculi AReCCa 2023 Organization Program Committee Christoph Benzmüller University of Bamberg, Germany Wolfgang Bibel Technical University of Darmstadt, Germany – co-chair Chad Brown Czech Technical University in Prague, Czech Republic David Cerna Czech Academy of Sciences, Czech Republic Michael Färber University of Innsbruck, Austria Didier Galmiche LORIA - Université de Lorraine, France Sean Holden University of Cambridge, UK Cezary Kaliszyk University of Innsbruck, Austria Jens Otten University of Oslo, Norway – co-chair Michael Rawson TU Wien, Austria Stephan Schulz DHBW Stuttgart, Germany Josef Urban Czech Technical University in Prague, Czech Republic Christoph Wernhard University of Potsdam, Germany Zsolt Zombori Hungarian Academy of Sciences, Hungary Editors & Workshop Chairs 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 Wolfgang Bibel Technical University of Darmstadt Wiesenrain 20, 88175 Scheidegg, Germany E-mail: bibel@gmx.net Web: http://intellektik.de/index/WolfgangBibel.htm ii Automated Reasoning with Connection Calculi AReCCa 2023 Contents AReCCa 2023 – Automated Reasoning with Connection Calculi 1–3 Jens Otten and Wolfgang Bibel 20 Years of leanCoP - An Overview of the Provers 4–22 Jens Otten A Curiously Effective Backtracking Strategy for Connection Tableaux 23–40 Michael Färber nanoCoP-Omega: A Non-Clausal Connection Prover with Arithmetic 41–53 Leo Repp and Mario Frank Embedding the Connection Calculus in Satisfiability Modulo Theories 54–63 Clemens Eisenhofer, Laura Kovács and Michael Rawson Structure-Generating First-Order Theorem Proving 64–83 Christoph Wernhard A Syntax for Connection Proofs 84–94 Jens Otten and Sean B. Holden Connect++: A New Automated Theorem Prover Based on the Connection Calculus 95–106 Sean B. Holden Connections: Markov Decision Processes for Classical, Intuitionistic and Modal Connection Calculi 107–118 Fredrik Rømming, Jens Otten and Sean B. Holden Comparison of Proof Methods 119–132 Wolfgang Bibel iii