VAMPIRE17: VAMPIRE 2017
The Fourth Vampire Workshop

August 7, 2017, Gothenburg, Sweden

The fourth Vampire workshop will be held at CADE-26, in Gothenburg, Sweden.

The workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas. The workshop will also discuss the development and use of the first-order theorem prover Vampire.

Workshop participants will include both Vampire developers and users, with discussions between tool developers and users. The users can learn more about Vampire and its recent developments. The users can learn more about the use of Vampire, its efficiency in various application areas and needs of the users.

The workshop is going to to shed the light on on problems such as

  • 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;
  • both successful and unsuccessful case studies;
  • missing features in modern theorem provers.

The workshop will also overview the most recent advances made in Vampire.