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