Berlin, Germany, August 2, 2015
The second Vampire workshop will be held at CADE-25 - the 25th International Conference on Automated Deduction in Berlin, Germany.
The workshop aims at discussing the development and use of the first-order theorem prover Vampire. The workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas.
Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The users can learn more about Vampire and its recent developments. The developers 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.