|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Interfacing two similar HOLs
If you have a question about this talk, please contact Thomas Tuerk.
In this talk I will describe ongoing work to interface the theorem-provers Isabelle/HOL and LEO -II. Both systems accept encodings in similar dialects of classical higher-order logic but offer contrasting levels of support in terms of ease-of-encoding and automation: Isabelle/HOL offers a comfortable setup of definitional extensions, but offers moderate automation; whereas LEO -II is definitionally spartan but promises a high degree of automation. The integration of these two tools is desirable since it would yield a composite which enjoys the good qualities of both tools.
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 listsBioenergy Initiative Rewriting the Code of Life: The science and ethics behind genome editing Graduate Development Lecture Series
Other talksPlasma Protein Purification System - plasma fractionation by affinity chromatography Inside the Macclesfield Psalter The Intriguing World of Clay-Inorganic Nanoparticle Suspensions: Practical Opportunities and Theoretical Challenges Dr David Bending: A novel tool to visualize and manipulate the dynamics of T cell regulation in vivo Lipid Metabolism in apicomplexan parasites: Routes for drug therapy Learning to know: the educations of Richard Hakluyt and Thomas Harriot