Seminar: Mercury Talk. Recent Developments in Automated Higher-Order Theorem Proving
| Dates: | 18 March 2020 |
|---|
| Times: | 14:00 - 15:00 |
|---|
| What is it: | Seminar |
|---|
| Organiser: | Department of Computer Science |
|---|
| Who is it for: | University staff, Adults, Current University students |
|---|
| Speaker: | Ahmed Bhayat |
|---|
|
Please join us for the next Mercury talk with speaker Ahmed Bhayat on Wednesday 18 March 2020 at 2pm in Kilburn L.T 1.5
Higher-order logic is the natural language for many areas of mathematics. As such, it would be useful to have strong automation for higher-order reasoning. Unfortunately, automation for higher-order logic has lagged behind that for first-order logic. The Vampire theorem prover, developed in Manchester, along with other leading first-order theorem provers are based on the superposition calculus. Superposition is essentially a brute force search through the set of all conclusions from given axioms. However, it adds powerful simplification techniques that allow the the deletion of redundant conclusion thus keeping the search space manageable. For many years it was an open question whether superposition could be extended to higher-order logic. In this presentation, I provide details on recent research extending superposition to higher-order logic. This has been done in two ways, one of which has been implemented in Vampire.
Speaker
Ahmed Bhayat
Role: PGR student
Organisation: University of Manchester
Travel and Contact Information
Find event
L.T 1.5
Kilburn Building
Manchester
