[04-08] Superposition for Higher-Order Logic
Title: Superposition for Higher-Order Logic
Speaker: Alexander Bentkamp
Time: 4月8日（周五）3:00 PM
Meeting ID: 874 2356 6413
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.