|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 listsSCAMPS 09 - One day Symposium Royal Aeronautical Society (RAeS) Cambridge Branch Type the title of a new list here
Other talksWriting Sound : Designing Notation : Carolingian Musical Techne Decompressive Craniectomy following Traumatic Brain Injury Brauer Relations and Mackey Functors 'It's not my story to tell': ownership, legitimacy, and the politics of history in Mocimboa da Praia, Mozambique Highlights from the “Deciphering the Mechanisms of Developmental Disorders (DMDD) consortium” – novel insights into gene function during embryogenesis Can neurocognitive findings inform our understanding of disruptive behavior and what to do with it?