CICM 2021 Invited Speakers

Alessandro Cimatti (Fondazione Bruno Kessler, Trento, IT)
Title: Logic at work, and some research challenges for computer mathematics
Abstract: Formal verification relies on the ability to exhaustively analyze the dynamic behaviour of complex systems. Such systems are modeled as transition systems or hybrid automata, and are represented symbolically by way of logical formulae interpreted over mathematical theories with nonlinear and transcendental operators and with differentiable functions. In this talk I will first outline the methods currenlty adopted in formal verification, ranging from Satisfiability Modulo Theories to abstraction- refinement and property-directed reachability. Then, I will overview some research challenges in computer mathematics to improve the effectiveness and efficiency of such methods.

Michael Kohlhase (FAU Erlangen-Nürnberg, Germany)
Title: Referential Semantics -- a Concept for Bridging between Representations of mathematical/technical Documents and Knowledge
Abstract:

Laura Kovacs (TU Vienna, Austria)
Title: Induction in Saturation-Based Reasoning
Abstract: We describe extensions to first-order theorem proving in support of automating inductive reasoning. We integrate induction directly into saturation-based proof search. We do so by turning applications of induction into inference rules of the saturation process and adding instances of appropriate induction schemata. Our inference rules capture the application of induction to inductive formulas to be proved. However, this is insufficient for efficient theorem proving. Modern saturation-based theorem provers are very powerful not just because of the logical calculi they are based on, such as superposition. What makes them powerful and efficient are (i) redundancy criteria and pruning search space, (ii) strategies for directing proof search, mainly by clause and inference selection, and recent results on (iii) theory-specific reasoning, for example with inductive data types. We overview our recent efforts in bringing induction in saturation, in particular in generalizing inductive formulas and handling recursive functions.

Angus Mcintyre (London/Edinburgh, UK)
Title: Doing Number Theory in Weak Systems of Arithmetic
Abstract: Although Godel's Theorem shows that even ZFC is incomplete for unsolvability of diophantine equations, nothing explicit of any real interest to number theorists has ever been shown to be unprovable. I will consider various important statements about solvability modulo all prime powers, and exhibit a wide class which get decided by PA (first order Peano Arithmetic) using serious algebraic geometry inside nonstandard models of PA. So although PA is often misrepresented as very weak, it is rather strong for basic results of 20th century number theory.