Induction with Generalization in Superposition Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Johannes Schoisswohl; Andrei Voronkov (CICM, 2020)

Induction with Recursive Definitions in Superposition. - Márton Hajdú; Petra Hozzová; Laura Kovács; Andrei Voronkov (FMCAD, 2021)

Inductive Benchmarks for Automated Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Johannes Schoisswohl; Andrei Voronkov (CICM, 2021)

Getting Saturated with Induction. - Márton Hajdú; Petra Hozzová; Laura Kovács; Giles Reger; Andrei Voronkov (Principles of Systems Design, 2022)

The Vampire Approach to Induction (short paper). - Márton Hajdú; Laura Kovács; Michael Rawson 001; Andrei Voronkov (PAAR@IJCAR, 2022)

Lemma Discovery and Strategies for Automated Induction. - Sólrún Halla Einarsdóttir; Márton Hajdú; Moa Johansson; Nicholas Smallbone; Martin Suda 001 (IJCAR (1), 2024)

Reducibility Constraints in Superposition. - Márton Hajdú; Laura Kovács; Michael Rawson 001; Andrei Voronkov (IJCAR (1), 2024)

Synthesis of Recursive Programs in Saturation. - Petra Hozzová; Daneshvar Amrollahi; Márton Hajdú; Laura Kovács; Andrei Voronkov; Eva Maria Wagner (IJCAR (1), 2024)

Induction in Saturation. - Laura Kovács; Petra Hozzová; Márton Hajdú; Andrei Voronkov (IJCAR (1), 2024)

Saturating Sorting without Sorts. - Pamina Georgiou; Márton Hajdú; Laura Kovács (LPAR, 2024)

Rewriting and Inductive Reasoning. - Márton Hajdú; Laura Kovács; Michael Rawson 001 (LPAR, 2024)

Term Ordering Diagrams. - Márton Hajdú; Robin Coutelier; Laura Kovács; Andrei Voronkov (CADE, 2025)

Partial Redundancy in Saturation. - Márton Hajdú; Laura Kovács; Andrei Voronkov (CADE, 2025)

The Vampire Diary. - Filip Bártek; Ahmed Bhayat; Robin Coutelier; Márton Hajdú; Matthias Hetzenberger; Petra Hozzová; Laura Kovács; Jakob Rath; Michael Rawson 001; Giles Reger; Martin Suda 001; Johannes Schoisswohl; et al. (CAV (3), 2025)

Synthesis Benchmarks for Automated Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Andrei Voronkov; Eva Maria Wagner; Richard Steven Zilincík (CoRR, 2025)