General Information

The Third International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop will take place in association with The 28th International Conference on Automated Deduction (CADE-28) on July 16, 2021. Just like CADE, ARCADE 2021 will be virtual due to the COVID-19 pandemic.


Program

Our schedule assigns a slot of 30 minutes to each presentation, with lots of room for discussion. All times are in EDT.
8:00-8:30 Erika Abraham, James H. Davenport, Matthew England and Gereon Kremer: Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
8:30-9:00 David Plaisted: Search Spaces for Theorem Proving Strategies
9:00-9:30 Michael Rawson and Giles Reger On Evaluating Theorem Provers
9:30-10:00 David Plaisted: Relevance and Abstraction
10:30-11:00 Geoff Sutcliffe: The Expansion, Modernisation, and Future of the TPTP World
11:00-11:30 Geoff Sutcliffe and David Plaisted: Management of the TPTP Problem Set
See also the CADE program on July 16.

Workshop Description

Scope

The main goal of this workshop is to bring together key people from various sub-communities of automated reasoning—such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving—to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community.

The first ARCADE was held in conjunction with CADE-26 in Gothenburg, Sweden. The second ARCADE was collocated with CADE-27 in Natal, Brazil.

The structure of the workshop will be informal. We invite extended abstracts in the form of non-technical position statements aimed at prompting lively discussion. The title of the workshop is indicative of the kind of discussions we would like to encourage:

  • Challenges: What are the next grand challenges for research on automated reasoning? Thereby, we refer to problems, solving which would imply a significant impact (e.g., shift of focus) on the CADE community and beyond?
  • Applications: Is automated reasoning applicable in real-world (industrial) scenarios? Should reports on such applications be encouraged at a venue like CADE, perhaps by means of a special case study paper category?
  • Directions: Based on the grand challenges and requirements from real- world applications, what are the research directions the community should promote? What bridges between the different sub-communities of CADE need to be strengthened? What new communities should be included?
  • Exemplary Achievements: What are the landmark achievements of automated reasoning whose influence reached far beyond the CADE community itself? What can we learn from those successes when shaping our future research?

Contributions will be grouped into similar themes and authors will be invited to make their case within discussion panels. Authors will then be invited to extend their abstracts for inclusion in post-proceedings.


Organisation

Organisers

Martin Suda, Czech Technical University
Sarah Winkler, Free University of Bolzano

Program Committee

Franz Baader, TU Dresden
Alexander Bentkamp, Vrije Universiteit Amsterdam
Christoph Benzmüller, Freie Universität Berlin
Armin Biere, Johannes Kepler University Linz
Nikolaj Bjørner, Microsoft Research
Maria Paola Bonacina, Università degli Studi di Verona
Pascal Fontaine, LORIA, Inria, University of Lorraine
Silvio Ghilardi, Università degli Studi di Milano
Jürgen Giesl, RWTH Aachen
Reiner Hähnle,TU Darmstadt
Marijn Heule, The University of Texas at Austin
Cezary Kaliszyk, University of Innsbruck
Laura Kovacs, Vienna University of Technology
Aart Middeldorp, University of Innsbruck
Stefan Mitsch, Carnegie Mellon University
Neil Murray, SUNY at Albany
David Plaisted, University of North Carolina at Chapel Hill
Andrei Popescu, Middlesex University London
Andrew Reynolds, University of Iowa
Philipp Rümmer, Uppsala University
Renate Schmidt, The University of Manchester
Stephan Schulz, DHBW Stuttgart
Geoff Sutcliffe, University of Miami
Josef Urban, Czech Technical University
Christoph Weidenbach, Max Planck Institute for Informatics