Vampire17: Editor's Preface

This volume contains the post-proceedings of the 4th Vampire Workshop (Vampire 2017), held on August 7, 2017 in Gothenburg, Sweden. The workshop was held as an affiliated event of the 26th International Conference on Automated Deduction (CADE-26).

Vampire 2017 was organized to discuss recent developments in implementing, applying, benchmarking and comparing first-order theorem provers and their combinations with other systems. Papers included in this volume were presented as talks at the workshop. Vampire 2017 also featured an invited talk of Dejan Jovanovic (SRI). Participants of our workshop included users and developers of automated reasoning engines (SAT/SMT solvers and first- and higher-order theorem provers) and resulted in many interesting discussions between tool developers and users. 

The authors were invited to submit their papers in the post-proceedings of our workshop. After peer reviewing, we accepted 5 submissions as regular papers. In addition, we were also lucky to receive two invited papers written by leading experts in automated reasoning: by Nikolaj Bjorner and Lev Nachmanson and by Stephan Schulz. 

We would like to thank all authors who submitted papers to our post-proceedings and to all participants of Vampire 2017. We also thank the EasyChair team for their help in publishing these post-proceedings.