|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 listsMuseum of Zoology Associative experiment Visual Rhetoric and modern South Asian history (2014)
Other talksRetrospective evaluation of masitinib and prednisolone compared to masitinib alone in canine mast cell tumours. MRI-THE WONDER MACHINE: FROM BLUE SKIES TO EVERY DAY USAGE Film screenting - Quarter 4/11 Native speaker and learner language data in Applied Linguistics: what's next? Mind Network Spring 2016 Generative learning in the human brain