The 28th International Conference on Automated Deduction

The conference on Automated Deduction (CADE) is the major international forum at which research on all aspects of automated deduction is presented. The conference programme includes invited talks, paper presentations, workshops, tutorials, and system competitions. Furthermore, the Herbrand Award for Distinguished Contributions to Automated Deduction, the Skolem Award(s) for influential historical CADE papers, and the new Bill McCune PhD Award, are presented at the conference.

The 28th International Conference on Automated Deduction (CADE-28) will be virtual due to the COVID-19 pandemic. The virtual conference will take place from July 11 to 16, 2021 as originally planned.

Submissions to CADE-28 can be made in two categories: Regular papers (up to 15 pages in LNCS style, excluding references) and short papers (up to 10 pages in LNCS style, excluding references). More information about submission can be found in the joint Call for Papers and Workshops/Tutorials/Competitions.

The authors of a selection of the best CADE-28 papers will be invited to submit an extended version of their paper after the conference, to be published in a special issue of the Journal of Automated Reasoning.

CADE-28 is organized in cooperation with ACM SIGLOG.

Open Access Proceedings Available

The accepted papers have been published in Lecture Notes in Artificial Intelligence volume 12699 with Open Access (Springer).

CADE-28 Proceedings

All dates are Anywhere on Earth.

Events

Workshops+Tutorials: July 11 and 16, 2021
Conference: July 12 - 15, 2021

Papers

Papers must be submitted to the CADE-28 track via EasyChair.
All papers must include the ORCID ids of authors (at least the corresponding author).

Abstract deadline: February 15, 2021
Submission deadline: February 22, 2021 (AoE, no extensions)
Rebuttal phase: March 29 to March 31, 2021
Notification: April 9, 2021
Final version: April 30, 2021

Liron Cohen, Ben-Gurion University

Title: Non-well-founded deduction for induction and coinduction

Induction and coinduction are both used extensively within mathematics and computer science. Algebraic formulations of these principles make the duality between them apparent, but do not account well for the way they are commonly used in deduction. Generally, the formalization of these reasoning methods employs inference rules that express a general explicit (co)induction scheme. Non-well-founded proof theory provides an alternative, more robust approach for formalizing implicit (co)inductive reasoning. This approach has been extremely successful in recent years in supporting implicit inductive reasoning, but is not as well-developed in the context of coinductive reasoning. This talk reviews the general method of non-well-founded proofs, and puts forward a concrete natural framework for (co)inductive reasoning, based on (co)closure operators, that offers a concise framework in which inductive and coinductive reasoning are captured as we intuitively understand and use them. Through this framework we demonstrate the enormous potential of non-well-founded deduction, both in the foundational theoretical exploration of (co)inductive reasoning and in the provision of proof support for (co)inductive reasoning within (semi-)automated proof tools.

Bio: Liron Cohen is senior lecturer (assistant professor) in the Department of Computer Science at Ben-Gurion University in Israel. Previously, Liron was a Fulbright postdoctoral researcher at Cornell University working with Robert Constable. She obtained her Ph.D. in 2016 from Tel Aviv University advised by Arnon Avron. Liron's research is motivated by the desire to understand the deep connection between proofs and computation. Her research interests include computer-aided deduction and verification, type systems, logics, programming languages and computational mathematics.

Mooly Sagiv, Tel Aviv University

Title: Formal Reasoning about Decentralized Financial Applications

Financial applications such as Landing and Payment protocols, and their realization in decentralized financial (DeFi) applications in Blockchains, comprise a unique domain where bugs in the code may be exploited by anyone to steal assets. This situation provides unique opportunities for formal verification to enable “move fast and break nothing”. Formal verification can be used to detect errors early in the development process and guarantee correctness when a new version of the code is deployed.

I will describe an attempt to automatically verify DeFis and identify potential bugs. The approach is based on breaking the verification of DeFis into decidable verification tasks. Each of these tasks is solved via a decision procedure which automatically generates a formal proof or a test input showing a violation of the specification. In order to overcome undecidability, high level properties are expressed as ghost states and static analysis used to infer how low level programs update ghost states.

Bio: Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv University and a CEO and co-founder of Certora. He is a leading researcher in the area of large scale (inter-procedural) program analysis, and one of the key contributors to shape analysis. His fields of interests include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments.

Guido Governatori, CSIRO

Title: Computational Law: Automated Reasoning in the Legal Domain

Bio: Guido Governatori leads the Software Systems Research Group and research activities on legal informatics at CSIRO's Data61. He received his PhD in Legal Informatics from the University of Bologna. His research has focused on automated reasoning techniques for non-classical logic, modal logic and non-monotonic reasoning (including labelled tableaux for modal logic, rule-based systems, and defeasible logic), and their applications in the legal domain, autonomous agents and business processes.

Markus Rabe, Google

Title: Towards the Automatic Mathematician

Over the recent years deep learning has found successful applications in mathematical reasoning. Today, we can predict fine-grained proof steps, relevant premises, and even useful conjectures using neural networks. This extended abstract summarizes recent developments of machine learning in mathematical reasoning and the vision of the N2Formal group at Google Research to create an automatic mathematician. The second part discusses the key challenges on the road ahead.

Bio: Markus N. Rabe is a software engineer and researcher at Google. He explores the foundations of automated reasoning, including the use of deep learning, and is a member of the N2Formal team, which has the goal to automatically formalize mathematics. Markus has a Ph.D. from Saarland University and visited UC Berkeley as a postdoc.

Participants of CADE-28 need to register at https://www.conftool.org/cade28/index.php . Registration includes the ability to attend the workshops and tutorials. Standard registration is now open and closes on July 4, 2021. Late registration (higher fees) will start on July 5, 2021.

There are three types of participants:
- Author participants (standard $120, late $150), whose registration fee will partially cover the conference costs. For each accepted conference paper, one author needs to register as an author participant. A single author registration covers only a single conference paper. Accepted workshop papers don't require author participant registration; and
- Regular participants (standard $50, late $80); and
- Student participants (standard $20, late $30). Students of accepted papers are eligible for a Woody Bledsoe award covering the student registration fee (but not an author registration fee). Advisors can nomiante their students for a Woody Bledsoe award at registration@cade-28.info.

Alternatively, one can register only for the workshops and tutorials (standard $20, late $30) or only for CASC (standard $65, late $85).

Everything will be on Zoom: the workshops and tutorials, the paper sessions, the lobby area, etc. To make this all work everyone must have their own device (laptop/desktop/tablet/etc.) with Zoom app version 5.6 or better installed. Zoom 5.6 has been around since March 2021, but please check to be sure.

There will be two Zoom meetings, one for the workshops and tutorials on the 11th and 16th July, and one for the conference 12-15th July. Each day the main Zoom room will be the ZoomLobby. There will be breakout rooms for the various workshops, tutorials, parallel conference events, named ZoomRoomN with N in 1..5. You can move yourself freely between rooms, without approval or help from the meeting hosts. Additionally there will be rooms that participants can use for private Zoom chats, named ChatRoomN, N in 1..10.

Checklist for Everyone

• Have Zoom app version 5.6 or better installed.
• Make sure you know how to mute/unmute yourself, put a question in the chat, etc.
• Make sure you know how to move into and out of a breakout room. In the Breakout Rooms window click on the number at the right to join that room, and confirm.
• Feel free to use an empty ChatRoom anytime during the conference (a room with the number 0 next to it is empty).

Checklist for Presenters

• Make sure you know how to share and stop sharing your screen.   In particular, test it with whatever tools you plan to show during   your presentation (Powerpoint, PDFViewer, terminal window, etc.)   to make sure the font, window/fullscreen mode, etc., all work well.
• Go to the breakout room listed in the program.
• Turn on your camera (we expect to see you live!).
• Give your talk live - you may not play a recorded video (we expect to see a live talk!).
• The session chair will monitor for questions during and after the   presentation, and will unmute questioners.
• Watch the chat for time warnings.
• Unshare your screen when finished.

Checklist for Audience

• Go to the breakout room listed in the program.
• Enjoy your session.
• Raise Zoom hand to ask a question, and ask your question in Zoom.   You can also ask questions in chat.

Checklist for Session Chairs

• Go to the breakout room listed in the program.
• You will be made a co-host, which will give you certain privileges, see https://support.zoom.us/hc/en-us/articles/360040324512-Roles-in-a-meeting
• Ensure presenters are online, and can share screen to present.
• Mute all except each presenter (mute all in the Participants window).
• Monitor participants for raised hands, or in chat, with questions, tell   questioners to unmute themselves, speak chat questions, mute questioners   when done.
• Monitor the time, send a chat message to the presenter at 5min, 2min, 0min.
• If the presenter does not stop their screenshare, do it for them.

Workshops

July 11

Theorem Proving Components for Educational Software (ThEdu'21)

Workshop on Proof eXchange for Theorem Proving (PxTP)

Parallel and Distributed Automated Reasoning

July 16

17th International Workshop on Termination (WST 2021)

International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)

3rd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE)

Tutorials

July 11

Program Validation and Verification in PVS

Paolo Masci (NIA), Mariano Moscato (NIA), César Munoz (NASA), Aaron Dutle (NASA), and Tanner Slagel (NASA)

This tutorial provides a gentle introduction to PVS 7.1, recently released, through the most recent versions of NASALib and VSCode-PVS. The tutorial is structured as a hands-on activity with lectures and exercises. Attendees are encouraged to bring their own laptops (Linux or Mac OSX). Slides, exercises, and other information of the tutorial are available here: http://precisa.nianet.org/pvs-cade-2021/.

Practice of First-Order Reasoning

Stephan Schulz (DHBW), Adam Pease (Articulate Software), and Geoff Sutcliffe (University of Miami)

The tutorial will use PyRes, a simple but complete automatic theorem prover for first-order logic. PyRes has been particularly designed with a pedagogical purpose in mind. It is written in clear, extensively documented Python code. The tutorial will acquaint the participants with the architecture and implementation of a saturating first-order reasoning system. The morning sessions will comprise presentations on the most important aspects of resolution-based theorem proving and their realization in PyRes. Afternoon sessions will be supervised programming exercises by the participants, with the goal of building improved variants of the prover.
The tutorial will conclude with a small CASC-like competition where the different teams can compare the effects of their improvements. Systems that perform well will be eligible for late entry into the demonstration division of CASC.

July 16

Learning to Prove: Machine Learning for Better SAT and QSAT Solvers

Sean Holden (Univeristy of Cambridge)

Satisfiability (SAT) and quantified satisfiability (QSAT) solvers are a fundamental concern for the field of Automated Deduction. While machine learning (ML) is currently an immensely fashionable area, it might not be apparent to many that ML researchers have been applying their work to SAT and QSAT solvers since the late 1980s; and, in fact, numerous aspects of various state-of-the-art solvers employ ele- ments of ML. More recently SAT and QSAT solvers have become an application of interest within the area of deep ML, and the application of these techniques turns out to raise new issues. This tutorial aims to provide an overall introduction to how ML has been applied to date to SAT and QSAT solving, with the aim of providing interested researchers with sufficient background to help move the field forward.

Proof-Theoretical Analysis of Non-Fregean Logic

Szymon Chlebowski, Marta Gawek, Dorota Leszczyńska-Jasion, and Agata Tomczyk (Adam Mickiewicz University)

The tutorial focuses on proof-theory for non-Fregean logics. We will pay special attention to structural proof theory taking into considerations sequent systems and natural deduction systems. The issues of cut-elimination and normalization will be discussed. However, we will also present tableau systems (Rasiowa-Sikorski formalization, dual tableaux, synthetic tableaux) for non-Fregean logics. Finally, we will sketch the ideas how to use the variety of proof systems in facilitating automated proof search in propositional logics with identity.

Competitions

The CADE ATP System Competition (CASC)

Termination and Complexity Competition (termCOMP)

The CADE-28 program is available here (all times in EDT).

The CADE-28 proceedings are available here (Open Access).

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret and Petar Vukmirović. Superposition for Full Higher-Order Logic

Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin and Sophie Tourret. Making Higher-Order Superposition Work

Gabriel Ebner, Jasmin Blanchette and Sophie Tourret. A Unifying Splitting Framework

Visa Nummelin, Alexander Bentkamp, Sophie Tourret and Petar Vukmirović. Superposition with First-Class Booleans and Inprocessing Clausification

Randal Bryant and Marijn Heule. Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver

Hans-Jörg Schurr, Mathias Fleury and Martin Desharnais. Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann and Alisa Kovtunova. Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures

Camillo Fiorentini. Efficient SAT-based proof search in Intuitionistic Propositional Logic

Alessandro Cimatti, Alberto Griggio and Gianluca Redondi. Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning

Fajar Haifani, Sophie Tourret and Christoph Weidenbach. Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance

Mnacho Echenim, Radu Iosif and Nicolas Peltier. Unifying Decidable Entailments in Separation Logic with Inductive Definitions

Nicholas Smallbone. Twee: an equational theorem prover (System Description)

Kaustuv Chaudhuri. Subformula Linking for Intuitionistic Logic and Type Theory

Tobias Nipkow and Simon Roßkopf. Isabelle's Metalogic: Formalization and Proof Checker

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett and Cesare Tinelli. Politeness and Stable Infiniteness: Stronger Together

Emery Neufeld, Ezio Bartocci, Agata Ciabattoni and Guido Governatori. A Normative Supervisor for Reinforcement Learning Agents (System Description)

Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language (System Description)

Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz and Makarius Wenzel. The Isabelle/Naproche Natural Language Proof Assistant (System Description)

Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt and Clare Dixon. Efficient Local Reductions to Basic Modal Logic

Lee Barnett and Armin Biere. Non-Clausal Redundancy Properties

Ryan Krueger, Jesse Michael Han and Daniel Selsam. Automatically Building Diagrams for Olympiad Geometry Problems (System Description)

Jacob Errington, Junyoung Jang and Brigitte Pientka. Harpoon: Mechanizing Metatheory Interactively (System Description)

Franz Brauße, Konstantin Korovin, Margarita Korovina and Norbert Th. Müller. The ksmt calculus is a delta-complete decision procedure for non-linear constraints

Dohan Kim and Christopher Lynch. Equational Theorem Proving Modulo

Franz Baader, Patrick Koopmann, Francesco Kriegel and Adrian Nuradiansyah. Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes

Vivek Nigam, Giselle Reis, Samar Rahmouni and Harald Ruess. Proof Search and Certificates for Evidential Transactions

Martin Suda. New Techniques that Improve ENIGMA-style Clause Selection Guidance

Petra Hozzová, Laura Kovács and Andrei Voronkov. Integer Induction in Saturation

Emre Yolcu, Scott Aaronson and Marijn Heule. An Automated Approach to the Collatz Conjecture

Joanna Golinska-Pilarek, Michal Zawidzki and Taneli Huuskonen. Tableau-based decision procedure for non-Fregean logic of sentential identity

Tanel Tammet, Dirk Draheim and Priit Järv. Confidences for Commonsense Reasoning

Akihisa Yamada. Multi-Dimensional Interpretation Methods for Termination of Term Rewriting

Peter Baumgartner. The Fusemate Logic Programming System (System Description)

Runqing Xu, Liming Li and Bohua Zhan. Verified interactive computation of definite integrals

Christoph Wernhard and Wolfgang Bibel. Learning from Łukasiewicz and Meredith: Investigations into Proof Structures

Filip Bártek and Martin Suda. Neural Precedence Recommender

PC Chairs

André Platzer, Carnegie Mellon University
Geoff Sutcliffe, University of Miami

Conference Chair

Marijn Heule, Carnegie Mellon University

Workshop and Tutorial Chair

Alexander Steen, University of Luxembourg

Publicity Chair

Sophie Tourret, Max Planck Institute

Program Committee

Peter Baumgartner, CSIRO
Bernhard Beckert, Karlsruhe Institute of Technology
Christoph Benzmüller, Freie Universität Berlin
Armin Biere, Johannes Kepler University Linz
Nikolaj Bjorner, Microsoft
Jasmin Blanchette, Vrije Universiteit Amsterdam
Maria Paola Bonacina, Università degli Studi di Verona
Agata Ciabattoni, Vienna University of Technology
Koen Claessen, Chalmers University of Technology
Hans de Nivelle, School of Engineering and Digital Sciences Nazarbayev University
Stéphane Demri, LSV CNRS ENS Paris-Saclay
Huimin Dong, Zhejiang University
Gilles Dowek, INRIA and ENS Paris-Saclay
Mnacho Echenim, University of Grenoble
Pascal Fontaine, Université de Liège Belgium
Nathan Fulton, IBM
Silvio Ghilardi, Dipartimento di Matematica Università degli Studi di Milano
Jürgen Giesl, RWTH Aachen University
Rajeev Gore, The Australian National University
Nao Hirokawa, JAIST
Moa Johansson, Chalmers University of Technology
Dejan Jovanović, SRI International
Cezary Kaliszyk, University of Innsbruck
Laura Kovacs, Vienna University of Technology
Tomer Libal, American University of Paris
Assia Mahboubi, INRIA
Cláudia Nalon, University of Brasília
Vivek Nigam, fortiss GmbH
Tobias Nipkow, Technical University of Munich
Frank Pfenning, Carnegie Mellon University
Giles Reger, The University of Manchester
Andrew Reynolds, University of Iowa
Philipp Ruemmer, Uppsala University
Katsuhiko Sano, Faculty of Humanities and Human Sciences Hokkaido University
Renate A. Schmidt, The University of Manchester
Stephan Schulz, DHBW Stuttgart
Viorica Sofronie-Stokkermans, University Koblenz-Landau
Martin Suda, Czech Technical University in Prague
Tanel Tammet, Tallinn University of Technology
Sophie Tourret, Max Planck Institute for Informatics
Christian Urban, King's College London
Uwe Waldmann, MPI for Informatics
Yoni Zohar, Stanford University

CADE implements the ACM policy against harassment.