Formal and Informal Proofs
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.
