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

Towards Higher-order OWL. - Martin Homola; Ján Kluka; Petra Hozzová; Vojtech Svátek; Miroslav Vacura (Künstliche Intell., 2020)

Integer Induction in Saturation. - Petra Hozzová; Laura Kovács; Andrei Voronkov (CADE, 2021)

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)

Automated Generation of Exam Sheets for Automated Deduction. - Petra Hozzová; Laura Kovács; Jakob Rath (CICM, 2021)

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

Reuse of Introduced Symbols in Automatic Theorem Provers (short paper). - Michael Rawson 001; Martin Suda 001; Petra Hozzová; Giles Reger (PAAR@IJCAR, 2022)

Program Synthesis in Saturation. - Petra Hozzová; Laura Kovács; Chase Norman; Andrei Voronkov (CADE, 2023)

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification. - Petra Hozzová; Jaroslav Bendík; Alexander Nutz; Yoav Rodeh (LPAR, 2023)

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)

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)

Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols. - Petra Hozzová; Nikolaj Bjørner (CoRR, 2025)

From MBQI to Enumerative Instantiation and Back. - Marek Danco; Petra Hozzová; Mikolás Janota (CoRR, 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)