Connection calculi offer one of the most established bases for automating formal reasoning in classical and non-classical logics. Guiding the proof search by connections permits a systematic, goal-oriented and, hence, more efficient proof search. Due to their close relationship to sequent calculi and natural deduction, proofs in connection calculi can be presented directly in a more readable form.

In recent years, significant progress has been made in developing and implementing efficient connection calculi for classical and several non-classical first-order logics, such as intuitionistic and modal logics. The development of non-clausal connection calculi and the integration of machine learning into connection calculi have lead to more efficient calculi and implementations.

Aims and Scope

The main goal of the AReCCa workshop is to foster the development of efficient connection calculi and connection provers for classical and non-classical logics. To this end, the AReCCa workshop provides a forum to bring together researchers that are interested in automated reasoning with connection calculi, in order to present, discuss and publish recent developments in this research area.

The topics of the AReCCa workshop cover all theoretical and practical aspects related to the mechanization and automation of reasoning with connection calculi, including but not limited to:

  • proof search in connection calculi, including connection methods, connection tableau calculus, matings methods, model elimination
  • connection calculi for classical and non-classical logics, such as intuitionistic logic, modal logic, description logic, linear logic
  • propositional logic, first-order logic, higher-order logic
  • clausal and non-clausal connection calculi
  • optimization techniques, strategies and heuristics
  • machine learning for connection calculi
  • equality and arithmetic in connection calculi
  • decision procedures and counter example generation
  • implementations, experiments and tests
  • compact and lean implementations of connection calculi
  • user interfaces and proof presentation
  • applications and use cases for all sorts of domains

The AReCCa 2023 workshop is associated with TABLEAUX 2023, the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods in Prague, Czech Republic.