COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Rough-and-ready proof reconstruction

## Rough-and-ready proof reconstructionAdd to your list(s) Download to your calendar using vCal - Nik Sultana
- Tuesday 01 March 2011, 13:15-14:15
- Computer Laboratory, William Gates Building, Room SS03.
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:- All Talks (aka the CURE list)
- Computer Laboratory Automated Reasoning Group Lunches
- Computer Laboratory talks
- Computer Laboratory, William Gates Building, Room SS03
- School of Technology
Note that ex-directory lists are not shown. |
## Other listsTheoretical Chemistry TCM Blackboard Series Disability## Other talksEnzyme Activation through Ligand Binding Aspects of non-standard cosmology: galactic satellites Topfitter Edge-exchangeable graphs, sparsity, and power laws Innate Immunity: The first line of defence Prof Massimo Piepoli: TBC |