Vampire Home Page
Overview
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.