Proofs and algorithms seminar: Miki Hermann on Wednesday 27 March 2024 at 14h00 ===== Seminar of the proofs and algorithms pole ===== Hello everybody, For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Miki Hermann (LIX), invited by the PARTOUT team. ***** Wednesday 27 March 2024 at 14h00, room Grace Hopper ***** Miki Hermann -- Primal Grammars Driven Automated Induction Automated induction is important for many computer sciences and artificial intelligence applications. However, proof by induction is undecidable and diverges even for small examples, leading to failures in the proving experience. Many techniques have proposed ad-hoc heuristics to speculate on additional lemmas that hopefully stop the divergence. Although these methods have succeeded in proving interesting theorems, they have significant limitations: in particular, they often fail to find appropriate lemmas, and the provided lemmas may not be valid. We present a new technique that allows us to perform inductive proofs in conditional theories by automatically detecting the divergence of proof traces and deriving a primal grammar as well as new lemmas that schematize the divergent sequences and, thus, allow breaking the divergence and ending the proof. Our new technique is presented as a set of inference rules whose soundness and refutational completeness have been formally proved. Refutational completeness is particularly useful for detecting flaws in critical systems. Moreover, unlike related work, our new technique has no risk of over-generalization. If the initial conjectures are valid, then the lemmas generated by our technique subsume the divergent sequence and are also valid. The cornerstone of our method is the use of primal grammars, which are based on primitive recursive functions and represent the most general decidable schematization, with respect to description power, among all known schematizations. Our technique always succeeds in building a primal grammar when the divergence follows a primitive recursive pattern; this allows us to cover a large class of problems. Our new technique has been implemented in C++ and successfully proved several dozens of complex examples that fail with well-known theorem provers such as ACL2, Isabelle, LEAN, PVS, RRL, SPIKE, and related techniques for capturing and schematizing divergence for proof by induction. The following seminar will be on Thursday 14 March 2024 at 15h00 by Inigo Incer: Towards Provably Safe and Secure Systems with Contract-Based Design. The list of upcoming seminars can be found at: https://www.lix.polytechnique.fr/proofs-algorithms/seminar/ The calendar of seminars can be found at: https://www.lix.polytechnique.fr/proofs-algorithms/seminar/calendar.ics