Dinner

Monday 19:30 at the Camaroes Potiguar

Workshop Description

General Information

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

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 2017 in Gothenburg, Sweden.

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.

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:	2 June 2019 23 June 2019
Author notification:	30 June 2019 7 July 2019
Workshop:	26 August 2019
Post-proceedings deadline:	29 September 2019

Topics

To collect the most relevant and timely topics from various subcommunities, we asked the program committee for input. The following list summarizing the gathered questions is in no way meant to be exhaustive; rather, it collects example questions revolving around current challenges, applications, and directions.

Historically, a lot of research on automated reasoning was motivated by applications in mathematics and logic, verification, or artificial intelligence. Paragraphs (1)–(3) collect questions from these domains. Naturally, we are also most interested in contributions on challenges and difficulties at the very core of theorem proving and proofs (4). Finally, we also encourage discussion of non-technical issues about the future of our community (5).

(1) Automated Reasoning and Artificial Intelligence

• What is the role of automated reasoning (AR) in artificial intelligence (AI)?
• How can we use machine learning (ML) to build better provers, and how come it had so little impact in AR so far? Is AR not suited to ML?
• Conversely, can we use AR to better understand the results of machine learning techniques and thus help to provide explainable AI?

(2) Automated Reasoning and Verification

• The currently most widely used provers are for relatively “low-level” or even decidable logics such as SAT, SMT, and description logic. What are the practical prospects for provers for full first-order logic and beyond?
• What is the role of AR in program verification? What can AR offer to the program verification community, and which challenges need to be tackled to analyze real-world programs?
• What is the relationship between automated theorem provers and interactive proof assistant, beyond hammers?

(3) Automated Reasoning for Logic and Mathematics

• How to develop suitable standards, techniques and approaches for non- classical logics, in particular modal logic?
• What is the relationship between AR and symbolic computation?

(4) In the Guts of Theorem Proving and Proofs

• How to identify relevant facts from large knowledge bases?
• How can provers exploit semantic knowledge, or benefit from case analysis?
• How can we understand proofs of automatic theorem provers?
• How can we ensure reliability of formal verification tools? Should they be held to the same high standards that our community often applies to other pieces of software, i.e., should they be verified?

(5) Non-Technical Challenges

• Confluence of techniques and languages from fields such as propositional logic, SMT, classical first-order reasoning, and higher-order logic.
• How can we document, maintain, and transfer the vast amount of knowledge of our community that is encapsulated in software?
• How can we attract young people to our field?

Program

Our preliminary schedule assuming presentations of roughly 10 minutes comprises six topic blocks distributed over three sessions, as listed below. Every topic block is concluded by a discussion of 15-25 minutes.

8:30-10:00	Semantic and syntactic inference
	Christoph Weidenbach: The Challenge of Unifying Semantic and Syntactic Inference Restrictions
	John Hester: Automated Axiom Schemas with E
	Questions: Why bother with attempting proofs in ZFC, rather than sticking with NBG? Are these axiom schema instances actually necessary, and are they used?
	Machine learning in theorem proving
	Claudia Schon, Frieder Stolzenburg and Sophie Siebert: Using ConceptNet to Teach Common Sense to an Automated Theorem Prover
	Georg Moser and Sarah Winkler: Smarter Features, Simpler Learning
	Questions: Wouldn't it be better to use abduction instead of deduction for causal commonsense reasoning problems? Can first-order logic knowledge bases compete with knowledge graphs as a source of background knowledge? Considering machine learning of strategies applied to a given problem: can we preprocess characteristics from theorem proving problems which serve as useful features for learning? how could such features look like?
10:30-12:30	Automating higher order reasoning
	Jasmin Blanchette, Pascal Fontaine, Stephan Schulz, Sophie Tourret and Uwe Waldmann: Stronger Higher-Order Automation: A Report on the Ongoing Matryoshka Project
	Questions: How much higher-orderness do we really need in practice? Which parts of AR would you like to see being formally verified? Do you know of such ongoing efforts?
	Ethical aspects
	Christoph Benzmüller and Geoff Sutcliffe: Explicit Normative Reasoning and Machine Ethics
	Naveen Sundar Govindarajulu and Selmer Bringsjord: On Theorem Proving for Quantified Modal Logics: With Applications in Modeling Ethical Principles
	Making sure our tools are really useful
	Martin Riener: How can we improve theorem provers for tool chains?
	Giles Reger: Boldly Going Where No Prover Has Gone Before
14:00-15:30	New application areas
	Pedro Quaresma, Intelligent Geometry Community, and James H. Davenport: Intelligent Geometry Tools
	Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali and Andrey Rivkin: Verification of Data-Aware Processes: Challenges and Opportunities for Automated Reasoning
	General discussion

Organisation

Organisers

Martin Suda, Czech Technical University
Sarah Winkler, University of Innsbruck

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
Jürgen Giesl, RWTH Aachen
Alberto Griggio, FBK-IRST
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
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
Josef Urban, Czech Technical University
Christoph Weidenbach, Max Planck Institute for Informatics