Workshop Description

General Information

The First International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop will take place in association with The 26th International Conference on Automated Deduction (CADE-26) on the August 6, 2017.

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 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. Roughly ten years ago SMT was one such challenge.
  • 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 (if at all)? For example, following Reiner Hahnle’s question in the AAR Newsletter, is there a place at CADE for research on usable automated reasoning (in resemblance to the flourishing topic of usable security)?
  • 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 to be published in EPiC.


Submission

Please submit your paper via this EasyChair submission page. Submissions should use the EPiC LaTeX format. We solicit non-technical extended abstracts of 2–4 pages (without firmly enforcing this length requirement). The post-proceedings version of the paper may be longer (but still of a reasonable length).


Important Dates

Submission deadline: 12 May, 2017
Author notification: 23 June, 2017
Workshop: 6 August, 2017
Post-proceedings deadline: 29 September, 2017

Program

This is the final program. We have attached preprints of the submitted position papers. These may be modified before being published in the official proceedings. Each session will consist of a number of presentations and then a discussion session covering all presentations. Each discussion session will begin with a set of starting questions from the authors. We encourage attendees to consider these questions and read the preprints to prepare for lively discussion!

08:55-09:00 Intro
09:00-10:00 Session: Bridges Between Communities
09:00-09:10 Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, and Werner M. Seiler SC-square: when Satisfiability Checking and Symbolic Computation join forcesPDFslides
09:10-09:20 Simon Cruanes Making Automatic Theorem Provers more VersatilePDFslides
09:20-09:25 Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, and Uwe Waldmann Towards Strong Higher-Order Automation for Fast Interactive VerificationPDFslides
09:25-10:00 Discussion
  • Currently we have two communities, each reinventing what the other has done: can we ``join forces'' such that we do not have to become experts in too wide an area, but effectively manage to collaborate, by splitting the work in an interesting, fruitful, and rewarding way for both?
  • Both CA Systems and SMT Systems are large systems with their own internal logics and control flows. How can these collaborate at the technical level: master/slave (which direction?), coroutines, microservices etc.?

  • How to build a system for a combination of techniques (superposition+SMT+induction+…) with manageable complexity and correctness?
  • What theoretical framework would allow to describe such combinations in a simple(r) and general way?

  • A lot of work has gone into engineering the individual proof assistants. However, maybe too little has been into developing compositional methods and tools with a broad applicability across systems?
  • Have we done enough for automated reasoning to be used as a tool, where it is needed, for real-life applications? Aren't we creating a FOL playground, whereas the world expects... HO?
10:00-10:30 Coffee Break
10:30-11:15 Session: Artificial Intelligence and Machine Learning
10:30-10:35 Maria Paola Bonacina Automated Reasoning for Explainable Artificial IntelligencePDFslides
10:35-10:40 Josef Urban AI at CADE/IJCARPDF
10:40-10:50 Stephan Schulz We know (nearly) nothing! But can we learn?PDFslides
10:50-11:15 Discussion
  • What is the relationship between automated reasoning (AR) and machine learning (ML), or, more generally, AR and artificial intelligence (AI)?
  • Can the emergence of eXplainable AI (XAI) offer a grand challenge for future research into applying AR to explain ML-based predictions?

  • How do humans gain the ability to solve problems? How do mathematicians gain the ability to prove theorems that no current ATP system can prove?
  • How many people have read Turing's 1950 paper including its last section? How many of the CADE/IJCAR PC members have read the AlphaGo and DeepStack papers? How many of those can confidently explain the main ideas and the main reasons for the superhuman performance of these systems? How many people can confidently explain the main ideas behind the current performance of image recognition and language translation systems?
  • How many people believe that we can in 100 years produce a system that will (using today's hardware) prove Fermat's Last theorem (FLT), by manually defining "theories", manually defining "classes of problems", manually "designing solvers" for them, manually defining their "strategies and calculi", and manually "combining solvers" for more and more complicated lemmas involved in the proof of FLT?

  • Should we target domain-specific or more general search control knowledge?
  • Deep learning or hand-selected features - which is better for learning search control knowledge?
  • What is a better source for learning: Meta-information (success/failure, time to success, ...), full proofs, or even full search protocols?
11:15-12:00 Session: User Interfaces and Industrial Usage
11:15-11:25 Reiner Hähnle and Marieke Huisman 24 Challenges in Deductive Software Verification PDFslides
11:25-11:35 J Moore and Marijn Heule Industrial Use of ACL2: Applications, Achievements, Challenges, and DirectionsPDFslides
11:35-12:00 Discussion
  • How to establish experimental user case studies in the automated theorem proving community?
  • How to secure long-term funding for the development and maintenance of automated deduction systems and how to enable collaboration on such systems across different research groups?

  • Do we measure the success of a theorem prover (or any tool) in an industry by how many people use it or by the value it brings to the industry? If a single person saves a company half-a-billion dollars by using an obscure tool but is the only person in the company using the tool, do we deem the tool doomed to obscurity?
  • Is anyone working on a formally defined programming language with accompanying proof engine that supports scripting and GUIs and is rugged and powerful enough to model, simulate and prove properties of large digital artifacts like the x86 or the Java Virtual Machine?
12:00-14:00 Lunch
14:00-15:00 Session: Proof Formats
14:00-14:10 Bertram Felgenhauer Beyond DRAT: Challenges in Certifying UNSATPDFslides
14:10-14:20 Marijn Heule and Benjamin Kiesl The Potential of Interference-Based Proof SystemsPDFslides
14:20-14:30 Giles Reger and Martin Suda Checkable Proofs for First-Order Theorem ProvingPDFslides
14:30-15:00 Discussion
  • Which techniques that are hard for DRAT would you like to have support for?
  • Should such extensions be handled by standalone checkers or integrated into existing DRAT checkers?

  • Almost all proof systems reason only about the presence of premises. What prevents us, in particular theoreticians, from reasoning about their absence?
  • Deletion of clauses can be a powerful technique. In SAT, clause deletion provides efficiency, while in QSAT it provides a way to prove satisfiability. What can clause deletion offer in first-order logic?

  • What are the main hurdles preventing us from having the "Checkable Proofs for First-Order Theorem Proving"?
  • What should be the next steps to see this challenge realized in the near future?
  • Is more research on the theoretical side needed, or are we simply struggling because too many people would need to agree on too many details and commit to the subsequently?
15:00-15:30 Coffee Break
15:30-16:30 Session: Provers
15:30-15:40 Gopal Gupta, Elmer Salazar, Kyle Marple, Zhuo Chen, and Farhad Shakerin A Case for Predicate Answer Set ProgrammingPDFslides
15:40-15:50 Andrew Reynolds Challenges for Fast Synthesis Procedures in SMTPDFslides
15:50-16:00 Christoph Weidenbach Do Portfolio Solvers Harm?PDFslides
16:00-16:30 Discussion
  • What are the limits of model-finding approaches based on SAT solvers?
  • Can query-driven (proof-finding) approaches to automated reasoning be as efficient as model-finding, SAT solver-based approaches?
  • Can common sense reasoning, namely, reasoning used by humans, be automated faithfully & efficiently?

  • What are the best techniques for developing instantiation-based theorem provers and synthesis solvers for quantified formulas in specific theories, notably bit-vectors?
  • How can synthesis procedures in SMT solvers be leveraged as subprocedures of higher-order theorem provers and model finders?

  • How will the next generation of automatic reasoning calculi look like?
16:30-17:00 Concluding Discussion
19:00 ARCADE Dinner at Hello Monkey (Directions)

Organisation

Organisers

Giles Reger, The University of Manchester
Dmitriy Traytel, ETH Zürich

Program Committee

Franz Baader, TU Dresden
Christoph Benzmüller, Freie Universität Berlin
Armin Biere, Johannes Kepler University Linz
Nikolaj Bjørner, Microsoft Research
Jasmin Christian Blanchette, Inria Nancy & LORIA
Maria Paola Bonacina, Università degli Studi di Verona
Pascal Fontaine, LORIA, Inria, University of Lorraine
Silvio Ghilardi, Università degli Studi di Milano
Martin Giese, University of Oslo
Jürgen Giesl, RWTH Aachen
Alberto Griggio, FBK-IRST
Reiner Hähnle,TU Darmstadt
Marijn Heule, The University of Texas at Austin
Laura Kovacs, Vienna University of Technology
Aart Middeldorp, University of Innsbruck
Neil Murray, SUNY at Albany
David Plaisted, University of North Carolina at Chapel Hill
Andrei Popescu, Middlesex University London
Renate Schmidt, The University of Manchester
Stephan Schulz, DHBW Stuttgart
Geoff Sutcliffe, University of Miami
Cesare Tinelli, The University of Iowa
Andrei Voronkov, The University of Manchester
Christoph Weidenbach, Max Planck Institute for Informatics