20Feb 2020

Department of Mathematics and Computer Science, Spiegelgasse 5, Basel, 5th floor, seminar room 05.002

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