Research School Irregular

Our PGRs are doing interesting work that we might all be able to build on in the future.  The Mercury Seminar Series invites final year PGRs to discuss and disseminate their work in just the same way as the Departmental Atlas Seminars. This is your opportunity to understand the breadth of work undertaken in the Department and discuss ideas with our early career researchers. This first session of zoom seminars will occur every other week until the beginning of August.

Wed 10th June - 2pm - Ahmed Bhayat - Title: Recent Developments in automated Theorem proving in Higher-Order Logic

Zoom Meeting ID:970 6036 3613

Abstract: 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 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.

As we are increasingly moving to the new normal, even though it looks like it will be some time yet until we physically get back to the Kilburn we will be moving to a PGR Hangout / Chat / Drop-in / Clinic every two weeks to coincide with the new Mercury Seminar and will run after the seminar on the same zoom call.

The Call-ID is 97060363613 and you will soon be getting some updated calendar invites to reflect this.