Recorded 17 February 2023. Petra Hozzova of Technische Universität Wien, Institute of Logic and Computation, presents "Automation of Induction in Saturation" at IPAM's Machine Assisted Proofs Workshop. Abstract: Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this talk, I describe our recent results on integrating induction directly into saturation. We do so by turning applications of induction into inference rules of the saturation process and adding instances of appropriate induction schemata. We propose additional reasoning methods for strengthening inductive reasoning, as well as for handling recursive function definitions. Our work is implemented within the Vampire prover and our experimental results demonstrate the practical impact of our work. The work described in this talk is based on joint work with Marton Hajdu (TU Wien), Petra Hozzova (TU Wien), Giles Reger (Amazon), and Andrei Voronkov (U. Manchester, EasyChair, and TU Wien). Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/