BEGIN:VCALENDAR
PRODID:-//Columba Systems Ltd//NONSGML CPNG/SpringViewer/ICal Output/3.3-
M3//EN
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VEVENT
DTSTAMP:20200309T152039Z
DTSTART:20200318T140000Z
DTEND:20200318T150000Z
SUMMARY:Seminar: Mercury Talk. Recent Developments in Automated Higher-Or
der Theorem Proving
UID:{http://www.columbasystems.com/customers/uom/gpp/eventid/}mq3-k7g9vvs
m-w4j2gm
DESCRIPTION:Please join us for the next Mercury talk with speaker Ahmed B
hayat on Wednesday 18 March 2020 at 2pm in Kilburn L.T 1.5\n\n\nHigher-o
rder logic is the natural language for many areas of mathematics. As suc
h\, it would be useful to have strong automation for higher-order reason
ing. Unfortunately\, automation for higher-order logic has lagged behind
that for first-order logic. The Vampire theorem prover\, developed in M
anchester\, along with other leading first-order theorem provers are bas
ed on the superposition calculus. Superposition is essentially a brute f
orce search through the set of all conclusions from given axioms. Howev
er\, it adds powerful simplification techniques that allow the the delet
ion of redundant conclusion thus keeping the search space manageable. Fo
r many years it was an open question whether superposition could be exte
nded 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.
STATUS:TENTATIVE
TRANSP:TRANSPARENT
CLASS:PUBLIC
LOCATION:L.T 1.5\, Kilburn Building\, Manchester
END:VEVENT
END:VCALENDAR