17 October 2016: Yaqing Jiang Title: Machine learning for interactive theorem proving Abstract: Machine learning for interactive theorem proving Abstract: In recent years, automated theorem provers (ATPs) have been used to find proofs for problems in interactive theorem provers. Tools like Sledgehammer have been developed. One of the key problems for such tools is to filter lemmas that are useful to the goal we want to prove. Our research aims to improve the lemma selection with machine learning methods, and measure the difficulty of goals that can be proved by tools like Sledgehammer. Oct 17 2016 14.00 - 15.00 17 October 2016: Yaqing Jiang Machine learning for interactive theorem proving IF 4.31/4.33
17 October 2016: Yaqing Jiang Title: Machine learning for interactive theorem proving Abstract: Machine learning for interactive theorem proving Abstract: In recent years, automated theorem provers (ATPs) have been used to find proofs for problems in interactive theorem provers. Tools like Sledgehammer have been developed. One of the key problems for such tools is to filter lemmas that are useful to the goal we want to prove. Our research aims to improve the lemma selection with machine learning methods, and measure the difficulty of goals that can be proved by tools like Sledgehammer. Oct 17 2016 14.00 - 15.00 17 October 2016: Yaqing Jiang Machine learning for interactive theorem proving IF 4.31/4.33
Oct 17 2016 14.00 - 15.00 17 October 2016: Yaqing Jiang Machine learning for interactive theorem proving
