|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Rough-and-ready proof reconstruction
If you have a question about this talk, please contact William Denman.
This talk addresses the following question: “if we have a proof in one system, how do we check it using a different system?” . The motivations for asking this question are twofold: one might wish to move proofs of propositions between different systems; one might also wish to use a ‘safer’ system to check a proof, in the spirit of de Bruijn. During the talk I will describe an approach to proof reconstruction which relies on the existing internal automation of Isabelle/HOL to check proofs produced by Leo-II. This is made possible by Isabelle/HOL’s good level of automation. I will discuss some experimental results which suggest a measure of the strength of Isabelle/HOL’s internal automation relative to Leo-II.
This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsCambridge Medieval Art Seminar Series Talk by Bashir Saoudi Pathways to Manufacturing
Other talksTurbulent transport and mixing of oceanic sea salt aerosol over the Indian sub-continent: Cloud microphysical and geo-engineering implications Surface subgroups of graphs of free groups (part 2 of 2) The use of model based adaptive dose response in choosing doses in a lean clinical development plan From Asymmetric stem cell division to tissue engineering. Spin pumping and inverse spin hall effect in organic materials Talk by Managing Director of Abellio Greater Anglia