Automated Reasoning with Vampire
by Laura Kovacs, Vienna University of Technology, Vienna, Austria
Automated reasoning, and in particular first-order theorem proving, is one of the earliest research areas within artificial intelligence. It is undergoing a rapid development thanks to its successful use in program analysis and verification, security analysis, 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 the development of powerful theorem proving tools. However, recent developments are not always easily accessible to non-specialists. This short tutorial aims to address this by introducing the audience to first-order theorem proving. The workhorse used for a demonstration of concepts discussed at the tutorial will be our award-winning theorem prover Vampire.
The tutorial will be split in two parts. The first part immediately helps the audience place the work in context by introducing them to an application of theorem proving in Vampire for validating mathematical theorems. The second part introduces the core concepts of automating first-order theorem proving
Laura Kovacs is full professor at Technical University of Vienna, and head of the Formal Methods in Systems Engineering group which is concerned with the development of new methods and tools for the design and analysis of computer systems, including software, hardware and distributed systems. Her research areas are verification, invariants, theorem proving, and symbolic computation.