Hopster: Automated discovery of mathematical properties in HOL

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

Citation

Arkitekt (konstruktör)

Geografisk plats

Byggnad (typ)

Byggår

Modelltyp

Skala

Teknik / material

Index

item.page.endorsement

item.page.review

item.page.supplemented

item.page.referenced