Various Projects to improve the Vampire Theorem Prover

Primary supervisor

Additional supervisors

  • Andrei Voronkov

Additional information

Contact admissions office

Other projects with the same supervisor

Funding

  • Competition Funded Project (Students Worldwide)
This research project is one of a number of projects at this institution. It is in competition for funding with one or more of these projects. Usually the project which receives the best applicant will be awarded the funding. Applications for this project are welcome from suitably qualified candidates worldwide. Funding may only be available to a limited set of nationalities and you should read the full department and project details for further information.

Project description

Vampire is an award-winning automated theorem prover for first-order logic and there are various projects available to work with Vampire.

Automated theorem proving is applicable to many areas within Computer Science including hardware and software verification, security analysis, automated planning, ontology reasoning, or proving mathematical theorems. Vampire targets first-order logic, which is expressive and very useful for encoding problems in various domains, but is undecidable in general. Due to this undecidability, proof search in first-order logic is highly complex and necessarily controlled by a large number of heuristics. Being successful in this space requires a strong theoretical basis and strong engineering. To be efficient Vampire relies on advanced preprocessing and term indexing techniques. Vampire has won the main division of the CASC competition since 2002 and has enjoyed recent success in theory reasoning and satisfiability.

Available projects would fall into two broad areas:

Extend Vampire to do new things. Vampire is most well-known for its highly efficient reasoning for first-order logic, which has recently been extended to reasoning with theories such as arithmetic. It also incorporates effective techniques for symbol elimination and interpolation. There are possible projects involving extending Vampire to new logics, e.g. higher-order logic, or new applications.

Improve what Vampire already does: Such a project would make theoretical and practical improvements to existing techniques. Two example areas would be term indexing and proof construction. Whilst Vampire already makes effective use of term indexing there is much more that could be done to improve these methods by specialising them for specific tasks. Improvements to term indexing would lead to significant performance improvements. Vampire already produces readable and usable proofs but there is much more that could be done in this area to effectively communicate how the proof was reached and to communicate proof search steps even when no proof is found. Improvements in this area would improve the usability of Vampire.

Please contact Dr Giles Reger directly to discuss the specific projects we are particularly interested in or to propose your own.

▲ Up to the top