Vampire 2014 and 2015: Editor's Preface

First-order theorem proving is one of the earliest research areas in artificial intelligence and formal methods. It is undergoing a rapid development thanks to its successful use in program analysis and verification, semantic Web, databases, symbolic computation, theorem proving in mathematics, and other related areas. Breakthrough results in all areas of theorem proving have been obtained, including improvements in theory, implementation, and powerful theorem proving tools.

The Vampire workshop series aims to support the development of theory, methods and techniques that shape the future of automated reasoning. It  pays a special attention to the use and development of the world-leading theorem prover Vampire, and aims at providing a forum for active dialog between theoreticians and practitioners working in automated reasoning, and tool developers and users of existing and future theorem provers.

This volume contains the post-proceedings of the first two editions of the Vampire workshop series. The first Vampire workshop was held as an affiliated workshop of IJCAR 2014 at  FLoC 2014, while the second Vampire workshop was held at CADE 2015. We were delighted to have excellent keynote speakers: Jasmin Blanchette (INRIA Nancy and MPI Saarbruecken) in 2014, and Leonardo de Moura (Microsoft Research) and Geoff Sutcliffe (University of Miami) in 2015. Our invited speakers master theoretical and practical aspects of theorem proving reasoning and provided insights into the challenges, opportunities and applications of automated reasoning. In addition, the Vampire 2014 workshop included one tutorial overviewing the past and present of Vampire.  The papers accompanying the invited talks of Jasmin Blanchette and Geoff Sutcliffe are included in this volume. 

The contributed talks presented at the Vampire 2014 and Vampire 2015 workshops discussed new features of theorem provers, implementation principles to be used in first-order theorem proving, best heuristics and proof search strategies depending on the application areas of theorem proving, and reported on extensive summary of experimental results. Both editions of the Vampire workshop had 5 regular contributions.  This volume includes either extended abstracts or full papers describing some of these regular talks.

We thank the FLoC 2014 and CADE 2015 local organisers for their support and guidance and acknowledge the use of EasyChair for submission, reviewing and program generation of both workshops, and creation of this volume.