Colloquium: Mohammad Abdulaziz (Technical University of Munich)

Computer-based formal proof in computer science and mathematics

A formal proof is a proof within an axiomatic system, where proof steps are either applications of axioms or applications of formally proven statements. Formal proofs have a long history within mathematics, starting with Euclid's element's which had an axiomatic system for geometrical reasoning. The main motivation of constructing a formal proof is obtaining unambiguous detailed proofs that can be mechanically checked. The advent of computer-based tools for formal proof, such as automatic and interactive theorem provers, made it feasible to produce formal versions of proofs that would otherwise be impossible. In this talk I will give an overview of the state-of-the-art as well as my work on the applications of computer-based formal proofs to computer science and mathematics, with a special emphasis on their use to construct trustworthy algorithms and software systems.

Export event as iCal