Formal and Informal Proofs

Sara Kalvala

Date: July 17th (Wednesday)
Time: 14:25-14:50
Abstract
One difficulty in the use of formal proof systems for applications such as Computer Algebra is the different levels of abstraction. Proof systems attempt proof by rigorous logical inferences, while proofs in algebra are presented in a more informal fashion. I will present a method for integrating these levels of abstraction using so-called annotations, which capture domain-specific explanations and hints and integrate them within the Isabelle theorem prover, providing the user with an abstract level in close connection with the underlying rigorous proof.

______________
__________________________________________

Previous page RISC SWP Linz Austria