CADE-28: THE 28TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
PROGRAM

Days: Sunday, July 11th Monday, July 12th Tuesday, July 13th Wednesday, July 14th Thursday, July 15th Friday, July 16th

Sunday, July 11th

View this program: with abstractssession overviewtalk overview

08:00-10:00 Session 2C: PDAR Workshop: Practical Experience (PDAR-21)
Location: ZoomRoom 3
08:00
The Networked Uncertainty Principle, or How I Stopped Worrying and Love Local Tracing
08:30
Demonstrating Work-stealing with Lace and its Application in Sylvan
09:00
GPU SAT Solving
09:30
Hacking Shared Memory Parallelism in Vampire
08:00-10:00 Session 2E: ThEdu Workshop: ATPs in Geometry (ThEdu'21)
Location: ZoomRoom 1
08:00
Towards Next Step Guidance in Triangle Construction Problems (abstract)
08:30
Four Geometry Problems to Introduce Automated Deduction in Secondary Schools (abstract)
PRESENTER: Pedro Quaresma
09:00
Symbolic Comparison of Geometric Quantities in GeoGebra (abstract)
PRESENTER: Zoltán Kovács
09:30
Prooftoys: a Proof Assistant for Beginners (abstract)
09:00-10:00 Session 3: PxTP Workshop: Certifying Transformations (PxTP-7)
Location: ZoomRoom 2
09:00
A Framework for Proof-Carrying Logical Transformations (abstract)
09:30
General Automation in Coq through Modular Transformations (abstract)
10:00-10:30Break
10:30-12:00 Session 4C: PDAR Workshop: New Directions (PDAR-21)
Chair:
Location: ZoomRoom 3
10:30
Parallel Probabilistic Inference
11:00
Parallel Tricks for Speedy Learned Guidance
11:30
Constraint Solving in the Serverless Cloud
10:30-11:30 Session 4D: PxTP Workshop: Invited Talk (PxTP-7)
Location: ZoomRoom 2
10:30
Reasoning in Many Logics with Vampire: Everything's CNF in the End
10:30-12:00 Session 4E: ThEdu Workshop: ATPs in Geometry; Isabelle in Education (ThEdu'21)
Location: ZoomRoom 1
10:30
Automated Discovery of Geometrical Theorems in GeoGebra (abstract)
PRESENTER: Zoltán Kovács
11:00
Teaching Intuitionistic Propositional Logic Using Isabelle (abstract)
11:30
Make Isabelle Accessible! (abstract)
PRESENTER: Walther Neuper
11:30-12:30 Session 5: PxTP Workshop: Use Cases (PxTP-7)
Location: ZoomRoom 2
11:30
Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract) (abstract)
12:00-12:30Break
12:30-14:00 Session 6C: PDAR Workshop: Discussion (PDAR-21)

This will be a structured discussion session arranged around submitted discussion  points. The structure will depend on the number of participants. A list of discussion points will be posted on the PDAR website before the session. If you have a discussion point you would like to raise then please contact the chairs.

Location: ZoomRoom 3
12:30-13:10 Session 6D: PxTP Workshop: Generating and Using Proofs (PxTP-7)
Location: ZoomRoom 2
12:30
Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract) (abstract)
12:50
Alethe: Towards a Generic SMT Proof Format (Extended Abstract) (abstract)
12:30-14:00 Session 6E: ThEdu Workshop: Automated Deduction Educational Applications (ThEdu'21)
Location: ZoomRoom 1
12:30
Learning Theorem Proving by Example - Implementing JavaRes (abstract)
PRESENTER: Adam Pease
13:00
Evolution of SASyLF 2008-2021 (abstract)
13:30
A Drag-and-Drop Proof Tactic (abstract)
PRESENTER: Pablo Donato
14:00-14:30Break
15:20-16:20 Session 9: ThEdu Workshop: Automated Deduction Educational Applications (ThEdu'21)
Location: ZoomRoom 1
15:20
Automated Grading of Automata with ACL2s (abstract)
PRESENTER: Ankit Kumar
15:50
Automated Instantiation of Control Flow Tracing Exercises (abstract)
Monday, July 12th

View this program: with abstractssession overviewtalk overview

08:00-09:00 Session 12: Invited Talk (CADE-28)
Location: ZoomRoom 1
08:00
Formal Reasoning about Decentralized Financial Applications (abstract)
09:00-10:00 Session 13: Theories (A) (CADE-28)
Location: ZoomRoom 1
09:00
The ksmt calculus is a delta-complete decision procedure for non-linear constraints (abstract)
09:30
Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning (abstract)
10:00-10:30Break
10:30-12:30 Session 14: Logical Foundations (CADE-28)
Location: ZoomRoom 1
10:30
Tableau-based decision procedure for non-Fregean logic of sentential identity (abstract)
11:00
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (abstract)
11:30
Efficient Local Reductions to Basic Modal Logic (abstract)
12:00
Isabelle's Metalogic: Formalization and Proof Checker (abstract)
12:30-13:00Break
13:00-15:00 Session 15: Intuition and Induction (CADE-28)
Location: ZoomRoom 1
13:00
Unifying Decidable Entailments in Separation Logic with Inductive Definitions (abstract)
13:30
Subformula Linking for Intuitionistic Logic and Type Theory (abstract)
14:00
Efficient SAT-based proof search in Intuitionistic Propositional Logic (abstract)
14:30
Proof Search and Certificates for Evidential Transactions (abstract)
15:00-15:30Break
15:30-16:30 Reception (CADE-28)

The CADE-28 (online) reception, a time to meet and interact with friends and foes in the automated reasoning community.  It's open bar (BYO), tasty hors d'oeuvres(BYO), and live entertainment ... there will be five "topical sessions", each led by experts in the topical areas. To start it off the experts will give 5 minute teasers for their topics. Then for the second 30 minutes there will be five breakout ZoomRooms in which the experts will lead and listen to discussion of their topics. People can join and leave the topical rooms, to enjoy some interesting interactions. Remember that the ChatRooms are available if you want head off for a private discussion.

Location: ZoomLobby
15:30-16:00 Session 16: Topical ZoomRoom Teasers (CADE-28)
Location: ZoomRoom 1
15:30
Reception Opening
15:35
Newbie's Meeting Place
PRESENTER: Ruzica Piskac
15:40
17 Ways to make an ATP System Fast
PRESENTER: Stephan Schulz
15:45
How can Anyone Trust a Theorem Prover?
15:50
Step into the Darkside - Non-classical Logics
PRESENTER: Cláudia Nalon
15:55
Law, Morality, Religion, and ATP
Tuesday, July 13th

View this program: with abstractssession overviewtalk overview

08:00-10:00 Session 19: Theory in Practice (CADE-28)
Location: ZoomRoom 1
08:00
Non-Clausal Redundancy Properties (abstract)
08:30
Multi-Dimensional Interpretation Methods for Termination of Term Rewriting (abstract)
09:00
Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (abstract)
09:30
Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes (abstract)
10:00-10:30Break
10:30-12:30 Session 21: Inference (CADE-28)
Location: ZoomRoom 1
10:30
Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance (abstract)
11:00
A Unifying Splitting Framework (abstract)
11:30
Integer Induction in Saturation (abstract)
12:00
Superposition with First-Class Booleans and Inprocessing Clausification (abstract)
12:30-13:00Break
13:00-15:00 Session 22: Implementation (CADE-28)
Location: ZoomRoom 1
13:00
Superposition for Full Higher-Order Logic (abstract)
13:30
Making Higher-Order Superposition Work (abstract)
14:00
Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver (abstract)
14:30
Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant (abstract)
15:00-15:30Break
15:30-16:30 Session 23: Invited Talk (CADE-28)
Location: ZoomRoom 1
15:30
Computational Law: Automated Reasoning in the Legal Domain
Wednesday, July 14th

View this program: with abstractssession overviewtalk overview

08:00-09:00 Session 25: Invited Talk (CADE-28)
Location: ZoomRoom 1
08:00
Non-well-founded Deduction for Induction and Coinduction (abstract)
09:00-10:00 Session 26: Theories (B) (CADE-28)
Location: ZoomRoom 1
09:00
Politeness and Stable Infiniteness: Stronger Together (abstract)
09:30
Equational Theorem Proving Modulo (abstract)
10:00-10:30Break
10:30-12:30 Session 27: Applications in Systems (CADE-28)
Location: ZoomRoom 1
10:30
An Automated Approach to the Collatz Conjecture (abstract)
11:00
Verified interactive computation of definite integrals (abstract)
11:30
A Normative Supervisor for Reinforcement Learning Agents (System Description) (abstract)
11:45
Automatically Building Diagrams for Olympiad Geometry Problems (System Description) (abstract)
12:00
The Fusemate Logic Programming System (System Description) (abstract)
12:30-13:00Break
13:00-16:10 Session 28: Awards (CADE-28)
Location: ZoomRoom 1
13:00
Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
14:15
2020 Herbrand Award
14:25
Unification, Combination, Description Logics, and All That (abstract)
15:05
Break
15:15
2021 Herbrand Award
15:25
Isabelle: Growing and Applying a Proof Assistant
Thursday, July 15th

View this program: with abstractssession overviewtalk overview

08:00-10:00 Session 30: System Descriptions and Competition Reports (CADE-28)
Location: ZoomRoom 1
08:00
Twee: an equational theorem prover (System Description) (abstract)
08:15
The Isabelle/Naproche Natural Language Proof Assistant (System Description) (abstract)
08:30
The Lean 4 Theorem Prover and Programming Language (System Description) (abstract)
08:45
Harpoon: Mechanizing Metatheory Interactively (System Description) (abstract)
09:00
The CADE-28 ATP System Competition (CASC-28) Results (abstract)
09:30
Termination and Complexity Competition Results (abstract)
10:00-10:30Break
10:30-12:00 Session 31: ATP+AI (CADE-28)
Location: ZoomRoom 1
10:30
Confidences for Commonsense Reasoning (abstract)
11:00
Neural Precedence Recommender (abstract)
PRESENTER: Filip Bártek
11:30
Improving ENIGMA-Style Clause Selection While Learning From History (abstract)
12:00-12:30Break
13:30-14:00Break
Friday, July 16th

View this program: with abstractssession overviewtalk overview

08:00-10:00 Session 35A: Theorem Proving: Theory and Practice (ARCADE 2021)
Location: ZoomRoom 1
08:00
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic (abstract)
08:30
Search Spaces for Theorem Proving Strategies (abstract)
09:00
On Evaluating Theorem Provers (abstract)
09:30
Relevance and Abstraction (abstract)
08:00-09:00 Session 35E: WST Workshop: Invited Talk (WST 2021)
Location: ZoomRoom 2
08:00
Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs (abstract)
09:00-10:00 Session 36A: LFMTP Workshop: Meta-Theory Reasoning (LFMTP 2021)
Location: ZoomRoom 3
09:00
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts (abstract)
PRESENTER: Laila El-Beheiry
09:30
Countability of Inductive Types Formalized in the Object-Logic Level (abstract)
PRESENTER: Xiwei Wu
09:00-10:00 Session 36B: WST Workshop: Classical Topics in Termination (WST 2021)
09:00
Mixed Base Rewriting for the Collatz Conjecture (abstract)
09:30
deVrijer’s Measure for SN of λ→ in Scheme (abstract)
10:00-10:30Break
10:30-11:30 Session 37A: TPTP World (ARCADE 2021)
Location: ZoomRoom 1
10:30
The Expansion, Modernisation, and Future of the TPTP World (abstract)
11:00
Management of the TPTP Problem Set (abstract)
10:30-12:00 Session 37D: LFMTP Workshop: Foundations (LFMTP 2021)
Location: ZoomRoom 3
10:30
Automating Induction by Reflection (abstract)
11:00
Interacting safely with an unsafe environment (abstract)
11:30
Foundations of the Squirrel meta-logic for reasoning over security protocols (abstract)
PRESENTER: David Baelde
10:30-12:00 Session 37E: WST Workshop: Decidability and Analysis (WST 2021)
10:30
Polynomial Loops: Termination and Beyond (abstract)
11:00
Polynomial Termination over N is Undecidable (abstract)
11:30
Modular Termination Analysis of C Programs (abstract)
12:00-12:30Break
12:30-14:00 Session 39D: WST Workshop: Runtime Complexity (WST 2021)
Location: ZoomRoom 2
12:30
Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes (abstract)
13:00
Parallel Complexity of Term Rewriting Systems (abstract)
13:30
Between Derivational and Runtime Complexity (abstract)
13:30-14:00 Session 40: Foundations: MetaCoq (LFMTP 2021)
Location: ZoomRoom 3
13:30
Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style (abstract)
PRESENTER: Navid Roux
14:00-14:30Break
14:30-16:00 Session 41C: LFMTP Workshop: Formalization (LFMTP 2021)
Location: ZoomRoom 3
14:30
Adelfa: A System for Reasoning about LF Specifications (abstract)
PRESENTER: Mary Southern
15:00
A logical framework with a graph meta-language (abstract)
PRESENTER: Bruno Cuconato
15:30
Towards a Semantic Framework for Policy Exchange in the Internet (abstract)
14:30-16:30 Session 41D: WST Workshop: Term Rewriting and Termination Arguments (WST 2021)
Location: ZoomRoom 2
14:30
Did Turing Care of the Halting Problem? (abstract)
15:00
Formalizing Higher-Order Termination in Coq (abstract)
15:30
Observing Loopingness (abstract)
16:00
Loops for which Multiphase-Linear Ranking Functions are Sufficient (abstract)