### Skapa referens, olika format (klipp och klistra)

**Harvard**

Lindhé, V. och Logren, N. (2016) *Proof output and machine learning for inductive theorem provers*. Göteborg : Chalmers University of Technology

** BibTeX **

@mastersthesis{

Lindhé2016,

author={Lindhé, Victor and Logren, Niklas},

title={Proof output and machine learning for inductive theorem provers},

abstract={Automatic theorem provers have lately seen significant performance improvements by utilising knowledge from previously proven theorems using machine learning. HipSpec is an inductive theorem prover that has not yet explored this area, which is the primary motivation for this work. <br><br>
We lay a foundation for supporting machine learning implementations within HipSpec. Firstly, a format for representing inductive proofs of theorems is designed. Secondly, a persistent library is implemented, which allows HipSpec to remember already-proven theorems in between executions. These extensions are vital for allowing machine learning, since they provide the machine learning algorithms with the necessary data. <br><br>
This foundation is used to perform machine learning experiments on theorems from the TIP library, which is a collection of benchmarks for inductive theorem provers. We define several different feature extraction schemes for theorems, and test these using both supervised learning and
unsupervised learning algorithms. <br><br>
The results show that although no correlation between induction variables and term structure can be found, it is possible to utilise clustering algorithms in order to identify some theorems about tail-recursive functions.},

publisher={Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola},

place={Göteborg},

year={2016},

keywords={automated theorem proving, automated reasoning, theory exploration, machine learning},

note={65},

}

** RefWorks **

RT Generic

SR Electronic

ID 238593

A1 Lindhé, Victor

A1 Logren, Niklas

T1 Proof output and machine learning for inductive theorem provers

YR 2016

AB Automatic theorem provers have lately seen significant performance improvements by utilising knowledge from previously proven theorems using machine learning. HipSpec is an inductive theorem prover that has not yet explored this area, which is the primary motivation for this work. <br><br>
We lay a foundation for supporting machine learning implementations within HipSpec. Firstly, a format for representing inductive proofs of theorems is designed. Secondly, a persistent library is implemented, which allows HipSpec to remember already-proven theorems in between executions. These extensions are vital for allowing machine learning, since they provide the machine learning algorithms with the necessary data. <br><br>
This foundation is used to perform machine learning experiments on theorems from the TIP library, which is a collection of benchmarks for inductive theorem provers. We define several different feature extraction schemes for theorems, and test these using both supervised learning and
unsupervised learning algorithms. <br><br>
The results show that although no correlation between induction variables and term structure can be found, it is possible to utilise clustering algorithms in order to identify some theorems about tail-recursive functions.

PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,

LA eng

LK http://publications.lib.chalmers.se/records/fulltext/238593/238593.pdf

OL 30