Anders Schlichtkrull: The purpose of the project is to use proof assistants to prove that algorithms and logical inference systems work correctly, i.e. as intended. For instance, a proof assistant could be used to prove that an aircraft alerting algorithm indeed does alert aircrafts if they get too close.
To prove something, means to argue rigorously that it is true. Proof assistants are computer programs that can read such proofs, and check that they are correct. The proofs for proof assistants have to be written in special proof languages which are similar to programming languages, and the proof assistant ensures that all the arguments used in the proofs are valid. The proof assistant can also conduct parts of the proofs automatically.
Proof assistants can be applied to verify algorithms and logical inference systems, and this is especially advantageous since it has real world implications on our society that they work correctly. They are used in computer programs, mobile apps, web applications, etc. For instance, logical inference systems are used in description logic which has applications in medical science, software engineering, and the semantic web. Algorithms are used for instance to sort rows in a spreadsheet computer program or perform a search on the internet.
Proof assistants have already been used to prove correct an operating system which can be used in smartphones, the division algorithm of the AMD5K86 microprocessor, and an aircraft alerting algorithm.
Supervisors: Jørgen Villadsen, Thomas Bolander
Algorithms, Logic and Graphs section
Published as PhD report: Formalization of Logic in the Isabelle Proof Assistant