CICM 2022 Invited Speakers

• Erika Ábrahám (RWTH Aachen University)
  
  Title: SMT solving for Arithmetic Theories
  Abstract: Propositional satisfiability is the problem of determining, for a formula of propositional logic, whether there is an assignment of truth values to its variables for which that formula evaluates to true. In the 90's, a technology called SAT solving has become impressively powerful, being able to check the satisfiability of huge real-world propositional logic problems with millions of clauses.
  Based on this success, the question raised whether these technologies could be somehow extended to check also quantifier-free first-order logic formulas over different theories for satisfiability. This would be very helpful as a lot of real-world problems cannot be conveniently encoded in propositional logic. This was the motivation for the development of so-called Satisfiability Modulo Theories (SMT) solvers.
  In this talk we review the algorithmic background of these developments for arithmetic theories, present our own SMT solver SMT-RAT and discuss interesting future research directions.
  
  
• Deyan Ginev (FAU Erlangen-Nürnberg and NIST)
  
  Title: Welcome to ar5iv! Wrestling with the open problems of scholarly writing
  Abstract: The ar5iv Lab was introduced this February. It is an official, web-native preview of arXiv's corpus of scholarly preprints. In 2022, we can showcase a level of coverage and fidelity in converting LaTeX to HTML5 so as to receive wide community approval and initiate a new partnership under the arXiv Labs umbrella. This feat took us 15 years since the project was first presented to the CICM community. In this talk, I will outline the history and strategic decisions that helped us get here. I will also explore some of the open problems that keep us at 75% success rate in conversion. The core task at hand continues to be one of rescuing documents written for the requirements of a printed page into a web-native future.
  
  
• Sébastien Gouëzel (IRMAR, Université de Rennes 1)
  
  Title: Formalizing the change of variables formula for integrals in mathlib
  Abstract: We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on developments in linear algebra, analysis, measure theory and descriptive set theory. This is made possible by the highly integrated development model of mathlib.