Yutaka Nagashima

"Artificial Intelligence for Inductive Theorem Proving"

( MPI-SWS talk in Kooperation mit dem Fachbereich Informatik)

In this talk I present how to improve automation of Isabelle/HOL using artificial intelligence.Isabelle/HOL is a proof assistant known for its strong automation implemented as tactics.Therefore, instead of building a new automation tool from scratch, I introduce meta-tools that take advantage of existing tactics to achieve higher automation.Firstly, I present a proof method recommendation tool, which predicts what tactics to use for a given problem.For inductive problems, however, recommending induction tactics is only the beginning, but one has to identify what arguments to pass to induction tactics.Therefore, in the second part of this talk, I introduce approaches to identify good arguments for induction tactics.Our evaluations showed that our meta-tools indeed improve the proof automation of Isabelle/HOL.

Bio: Yutaka Nagashima is working at Yale-NUS college as research associate. Prior to joining Yale-NUS, he worked as junior researcher at the Czech Technical University in Prague while studying for a PhD degree at the University of Innsbruck in the area of artificial intelligence for theorem proving. Before PhD studies, He worked for Data61 and NICTA as proof engineer.
From 2013 to 2020 he mostly worked on proof automation for Isabelle/HOL, though he currently works on proof automation for SuSLik at Yale-NUS.

Termin als Datei downloaden und in den Kalender importieren.