View Proposal

Proposer
Lilia Georgieva
Title
Experiments with theorem provers
Goal
Study and experiment with theorem provers
Description
Principal goal of the project: SPASS, Vampire, and Otter are contemporary resolution-based theorem provers implementing sophisticated reasoning techniques and decision procedures for classes of first-order formulae and formulae in modal and description logics. For certain classes of formulae more than one refinement of resolution leads to a decision procedure. The aim of this project is to use theorem provers to test the potential and limitations of the systems when applied to such classes. The project would involve studying the properties of classes of formulae, their translation into the input language of the theorem provers, running the theorem provers, and evaluating the results. Prerequisites: Knowledge of first-order logic, interest in theorem proving; References: See http://spass.mpi-sb.mpg.de/spass http://www.cs.man.ac.uk/~riazanoa/Vampire
Resources
Background
Url
Difficulty Level
Moderate
Ethical Approval
None
Number Of Students
1
Supervisor
Lilia Georgieva
Keywords
Degrees
Back to List