|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Solving HOL problems using FOL tools
If you have a question about this talk, please contact Thomas Tuerk.
HOL is seen by many as an ideal language for expressing mathematical ideas, but HOL ’s expressivity makes its automation more challenging. One frequently finds that HOL problems are “essentially first-order”—that is, they can be faithfully translated into FOL . Automated reasoning in FOL is quite mature compared to that in HOL . It has been argued that for “essentially first-order” problems it is more sensible to carry out the translation into FOL and solve using high-performance FOL tools, rather than attempt to solve the problem using a HOL prover. During this talk I will describe and compare translations from HOL to FOL .
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 listsFood Futures in the World Motivic stable homotopy theory study group Clare Hall Talks
Other talksObserving Quasars that Switch Off. And back On again: What we are learning, and still don't understand, about the active central engines. Evolutionary analysis on barcode NGS swine influenza virus data 2017 Lord Lewis Lecture (I) Sustainable plasmonics: abundant materials for modular photocatalysis Bumps and Ramps in the Glacial CO2 Record 2017 Lord Lewis Lecture (II) Plasmonics for sustainability: harvesting light energy for new solar applications "The Shaman is the White Man's Computer": The interaction of shamanism and conservation in Amazonian Guyana