University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Solving HOL problems using FOL tools

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Solving HOL problems using FOL tools

Download to your calendar using vCal

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 lists

LT2, University of Cambridge Judge Business School Keynes Hall, King’s College. Cambridge Room GS4, Donald McIntyre Building, Faculty of Education, 184 Hills Road, Cambridge, CB2 8PQ.

Other talks

Harnessing Radical Reactivity for Molecular Innovation CONFERENCE: Chemical and material sciences enabled by AI and automation Morning Tea and Coffee How Far Can Good Go Without God? The Limits of a Naturalistic Ethic Talk title TBC Mergers all the way down: simulating the origin of globular clusters in a galactic context
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity