• Yutaka Nagashima – Towards Smart Proof Search for Isabelle (7 June, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation.
    In this talk, I present a proof strategy language for Isabelle and a proof method recommendation tool we are developing at Data61.
    Then, I sketch a smart proof search tool based on these two predecessors to drastically improve proof automation for Isabelle,
    while identifying major challenges we have to address for this objective.