Title: Superposition for Higher-Order Logic

Speaker: Alexander Bentkamp

Time: 4月8日（周五）3:00 PM

Venue: ZOOM线上

https://zoom.us/j/87423566413?pwd=ck9FUlpDb3F1dGU3RWUybzczelFrQT09

Meeting ID: 874 2356 6413

Passcode: 780571

Abstract: In this talk, I will give a gentle introduction to my PhD thesis. Superposition provers automatically find proofs in first-order logic. One of their biggest success stories is their use within proof assistants. However, proof assistants are often based on higher-order logic and need to use clumsy encodings to invoke superposition provers. I will explain how my colleagues and I have extended the superposition calculus to operate directly on higher-order logic, how this improves automation in the proof assistant Isabelle/HOL, and how we won the higher-order division of the prover competition CASC.

Bio: I am a postdoctoral researcher in the embedded systems group of the Key State Laboratory of Computer Science. My main research interests are interactive and automated theorem proving. I have a PhD in computer science from the Vrije Universiteit Amsterdam. Before my PhD, I studied mathematics and computational linguistics.