VAMPIRE 2014 PROCEEDINGS: EDITOR'S PREFACE

First-order theorem proving is currently undergoing a rapid development thanks to its successful use in program analysis and verification, semantic Web, database systems, symbolic computation, theorem proving in mathematics, and other areas.  A key feature for these recent developments is the implementation and availability of powerful theorem proving tools. 

The Vampire 2014 workshop focuses on the 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 an active dialog between:

• theoreticians and practitioners working in automated reasoning;
• tool developers and  research software engineers of existing and future theorem provers;
• users of theorem proving tools.

Vampire 2014 is the first ever Vampire Workshop and is dedicated to discussing the development and use of Vampire. The workshop addresses the newest trends in implementing first-order theorem provers, and focuses on new challenges and application areas. 

We are delighted to have one excellent invited speaker, Jasmin Christian Blanchette (Technische Universität München, Germany), addressing challenges and oppurtunities of automated and interactive theorem proving. In addition, the workshop includes one tutorial overviewing the past and present of Vampire. The 5 regular contributions presented at our workshop  shed the light  on what is essential for substantial progress in theorem proving tools; what are the best implementation principles to be used; what are the best heuristics and strategies, depending on application areas; and what are some missing features in modern theorem provers.

We would finally like to thank the VSL local organziers and EasyChair for their support and guidance.