Hopster: Automated discovery of mathematical properties in HOL
Ladda ner
Publicerad
Författare
Typ
Examensarbete för masterexamen
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
A new tactic for HOL is proposed that is suitable for proving equational properties
of functional programs. HOL has numerous tactics that automate the process of
proving a logical statement. Yet none incorporate the discovery of useful lemmas in
their process, an essential activity when performing a manual proof.
The Hopster tactic is able to discover new lemmas via a technique known as theory
exploration, implemented in a tool called QuickSpec. So far, theory exploration has
been applied with increasing success for generating many useful properties when
given a theory of considerable size. A dual to this scenario occurs when the theory
is fairly well-developed and the user is interested in proving a specific new property.
This work pays particular attention to the second scenario, when the user wishes
to prove a specific goal using theory exploration. The tactic has been designed
to support this case by automating the selection of which functions to explore.
The design and testing of this selection process are the principal contributions of
this work. The effectiveness and efficiency of the implementation are measured on
a set of test cases to identify where the tactic performs well and where further
improvements remain. It is hoped that Hopster serves as a useful tool that supports
the development of verified functional programs.
Beskrivning
Ämne/nyckelord
theory exploration, automated theorem proving, hopster, hol, quickspec