PROGRAM
Days: Monday, September 19th Tuesday, September 20th Wednesday, September 21st Thursday, September 22nd Friday, September 23rd
Monday, September 19th
View this program: with abstractssession overviewtalk overview
14:00-15:30 Session 1: CICM Invited talk, SMT solving
Chair:
Location: Room 107, TSU Academic Building 1
| 14:00 | SMT solving for Arithmetic Theories (abstract) |
| 15:00 | Targeted Configuration of SMT Solver (Online Talk) (abstract) PRESENTER: Jan Jakubův |
15:30-16:00Coffee Break
16:00-17:30 Session 2: Theorem proving and formalization
Chair:
Location: Room 107, TSU Academic Building 1
| 16:00 | Decomposition Rules: Dynamic, Schematic, Novel Axioms (Online Talk) (abstract) PRESENTER: Alan Bundy |
| 16:30 | Lemmaless Induction in Trace Logic (Online Talk) (abstract) PRESENTER: Ahmed Bhayat |
| 17:00 | Formalising the Kruskal-Katona theorem in Lean (Online talk) (abstract) |
Tuesday, September 20th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 3: CICM Invited talk, expression transformation
Chair:
Location: Room 107, TSU Academic Building 1
| 09:00 | Formalizing the change of variables formula for integrals in mathlib (Online Talk) (abstract) |
| 10:00 | Working with Families of Inverse Functions (abstract) PRESENTER: David Jeffrey |
10:30-11:00Coffee Break
11:00-12:30 Session 4: Digital libraries and mathematical knowledge management
Chair:
Location: Room 107, TSU Academic Building 1
| 11:00 | An Integrated Web Platform for the Mizar Mathematical Library (Online Talk) (abstract) PRESENTER: Hideharu Furushima |
| 11:30 | System Description sTeX3 – A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents (abstract) PRESENTER: Michael Kohlhase |
| 12:00 | Injecting Formal Mathematics Into LaTeX (abstract) PRESENTER: Dennis Müller |
13:00-14:00Lunch Break
14:00-15:30 Session 6: Formalization
Chair:
Location: Room 107, TSU Academic Building 1
| 14:00 | Formalising Basic Topology for Computational Logic in Simple Type Theory (Online Talk) (abstract) PRESENTER: David Fuenmayor |
| 14:30 | On the Formalization of the Heat Conduction Problem in HOL (abstract) PRESENTER: Elif Deniz |
| 15:00 | Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis (abstract) |
15:30-16:00Coffee Break
16:00-17:30 Session 7: Theorem proving and satisfiability
Chair:
Location: Room 107, TSU Academic Building 1
| 16:00 | OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas (Online Talk) (abstract) PRESENTER: Ankit Shukla |
| 16:30 | Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk) (abstract) PRESENTER: David Narváez |
| 17:00 | Hall's Theorem for Enumerable Families of Finite Sets (Online Talk) (abstract) PRESENTER: Mauricio Ayala-Rincón |
Wednesday, September 21st
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 8: Work-in-progress papers and system entries
Chair:
Location: Room 107, TSU Academic Building 1
| 09:00 | A Parallel Corpus for Natural Language Machine Translation to Isabelle (abstract) PRESENTER: Yiannos Stathopoulos |
| 09:20 | OEIS Semantified -- A Tetrapodal Data Set (abstract) PRESENTER: Michael Kohlhase |
| 09:40 | Setting up Set-theoretical Foundations in Naproche (abstract) PRESENTER: Peter Koepke |
| 10:00 | Web-Naproche (abstract) PRESENTER: Peter Koepke |
| 10:15 | Python client for Isabelle server (System Entry) (abstract) |
Thursday, September 22nd
View this program: with abstractssession overviewtalk overview
09:30-10:30 Session 9: Datasets and formalization
Chair:
Location: Room 107, TSU Academic Building 1
| 09:30 | Making the Census of Cubic Vertex Transitive Graphs searchable and FAIR (Online Talk) (abstract) PRESENTER: Filip Koprivec |
| 10:00 | Graded rings in Lean's Dependent type theory (Online Talk) (abstract) PRESENTER: Eric Wieser |
10:30-11:00Coffee Break
11:00-12:30 Session 10: Logic and education
Chair:
Location: Room 107, TSU Academic Building 1
| 11:00 | Learning to Reason Assisted by Automated Reasoning (Online Talk) (abstract) |
| 11:30 | Experiments with Automated Reasoning in the Class (abstract) PRESENTER: Isabela Dramnesc |
| 12:00 | Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories (abstract) PRESENTER: Ciaran Dunne |
12:30-14:00Lunch Break
14:00-15:30 Session 11: Digital libraries and mathematical knowledge management
Chair:
Location: Room 107, TSU Academic Building 1
| 14:00 | Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs (abstract) |
| 14:30 | Re-imagining the Isabelle Archive of Formal Proofs (Online Talk) (abstract) PRESENTER: Carlin MacKenzie |
| 15:00 | An evaluation of NLP methods to extract mathematical token descriptors (Online Talk) (abstract) PRESENTER: Emma Hamel |
15:30-16:00Coffee Break
16:00-17:00 Session 12: CICM Invited talk
Chair:
Location: Room 107, TSU Academic Building 1
| 16:00 | Welcome to ar5iv! Wrestling with the Open Problems of Scholarly Writing (Online Talk) (abstract) |
Friday, September 23rd
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 14: CLAS invited talk
Chair:
Location: Room 107, TSU Academic Building 1
| 09:00 | Hierarchical Higher-Order Port-graph Rewriting as a Modelling Tool (abstract) |
10:05-10:30 Session 15: Doctoral program
Chair:
Location: Room 107, TSU Academic Building 1
| 10:05 | Formalizing Algorithms for Real Quantifier Elimination (Online Talk) (abstract) |
10:30-11:00Coffee Break
11:00-12:40 Session 16: Doctoral program
Chair:
Location: Room 107, TSU Academic Building 1
| 11:00 | Formalization of Partial Differential Equations in HOL (abstract) |
| 11:25 | Understanding Trust Assumptions for Attestation in Confidential Computing (Online talk) (abstract) |
| 11:50 | Verified Convex Optimization for Hybrid Systems (abstract) |
| 12:15 | Formalising Nominal AC-Unification (Online talk) (abstract) |
12:40-14:00Lunch Break
14:00-15:40 Session 17: Work-in-progress papers
Chair:
Location: Room 107, TSU Academic Building 1
| 14:00 | Case Studies on Realms (Online talk) (abstract) PRESENTER: Franziska Weber |
| 14:20 | Sophize Mathematics Library (Online talk) (abstract) |
| 14:40 | Formalising the Krull Topology in Lean (Online talk) (abstract) |
| 15:00 | LOL: A library of lemmas for data-driven conjecturing (Online talk) (abstract) PRESENTER: Sólrún Halla Einarsdóttir |
| 15:20 | PISE (Proofscape Integrated Study Environment) (Online talk) (abstract) |
15:40-16:00Coffee Break