Vampire23: Editor's Preface

This volume presents the proceedings of the 7th Vampire workshop, held on 5th July 2023 in Rome, Italy. The workshop was affiliated and co-located with the 29th Confererence on Automated Deduction (CADE). The proceedings contains invited papers, as well as selected contributed papers presented at the workshop. The included papers in the proceedings have been peer-reviewed by workshop chairs and the Vampire developer team.

The Vampire workshop series aims to address recent trends in the implementation of first-order theorem provers, and focus on new challenges and application areas. It also discusses the development and use of the first-order theorem prover Vampire, and its potential use cases and interaction with other systems.

At the 7th Vampire workshop, we were fortunate to enjoy a variety of talks on these topics. Implementation of first-order theorem provers remains an active research area, including Stephan Schulz's work on lazy and eager patterns in high-performance automated theorem proving; Robin Coutelier's approach towards engineering subsumption resolution in Vampire; and Andrei Voronkov's Spider framework for learning in the sea of options. 

However, Vampire continues into new domains including higher-order logic (presented by Ahmed Bhayat within new tends in higher-order), induction (discussed by Márton Hajdu in syntax-driven induction), and program synthesis (detailed by Petra Hozzová when integrating answer literals with AVATAR for program synthesis). Vampire also achieves new use cases in Pamina Georgiou's approach on sorting without sorts in Vampire, and begins to interact with the Dedukti verification tool in the cocntribution of Anja Petkovic Komel towards verifying Vampire proofs in \lambda\Pi-calculus modulo theories. 

Related and relevant research efforts in saturation-based theorem proving have been overviewed and discussed to the greatest detail within the excellent invited talk on Sophie Tourret, introducing The Spawns of the Saturation Framework. 

We thank all speakers and the workshop participants for their contribution towards the development of Vampire and present and future systems like it.