9 October 2017: Yaqing Jiang Title: Machine learning for inductive theorem proving. Abstract: Although proof by induction is very common in theorem proving, it is notoriously difficult to automate. Our research aims to use modern techniques and methods including machine learning to tackle major challenges in automated inductive theorem proving, such as lemma speculation and variable selection. We build our work on top of the Boyer-Moore waterfall model, which provides a core skeleton for inductive proof automation in the proof assistant HOL Light. We also incorporate powerful off-the-shelf automated theorem provers and introduce novel concurrent proof strategies. We evaluate this work using existing theorem libraries within HOL Light. Oct 09 2017 14.00 - 15.00 9 October 2017: Yaqing Jiang Machine learning for inductive theorem proving. IF 4.31/4.33
9 October 2017: Yaqing Jiang Title: Machine learning for inductive theorem proving. Abstract: Although proof by induction is very common in theorem proving, it is notoriously difficult to automate. Our research aims to use modern techniques and methods including machine learning to tackle major challenges in automated inductive theorem proving, such as lemma speculation and variable selection. We build our work on top of the Boyer-Moore waterfall model, which provides a core skeleton for inductive proof automation in the proof assistant HOL Light. We also incorporate powerful off-the-shelf automated theorem provers and introduce novel concurrent proof strategies. We evaluate this work using existing theorem libraries within HOL Light. Oct 09 2017 14.00 - 15.00 9 October 2017: Yaqing Jiang Machine learning for inductive theorem proving. IF 4.31/4.33
Oct 09 2017 14.00 - 15.00 9 October 2017: Yaqing Jiang Machine learning for inductive theorem proving.
