CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Automated theory exploration for interactive theorem proving: An introduction to the hipster system

Moa Johansson (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers))
Lecture Notes in Computer Science: 8th International Conference on Interactive Theorem Proving, ITP 2017; Brasilia; Brazil; 26 September 2017 through 29 September 2017 (03029743). Vol. 10499 LNCS (2017), p. 1-11.
[Konferensbidrag, refereegranskat]

Theory exploration is a technique for automatically discovering new interesting lemmas in a mathematical theory development using testing. In this paper I will present the theory exploration system Hipster, which automatically discovers and proves lemmas about a given set of datatypes and functions in Isabelle/HOL. The development of Hipster was originally motivated by attempts to provide a higher level of automation for proofs by induction. Automating inductive proofs is tricky, not least because they often need auxiliary lemmas which themselves need to be proved by induction. We found that many such basic lemmas can be discovered automatically by theory exploration, and importantly, quickly enough for use in conjunction with an interactive theorem prover without boring the user.



Denna post skapades 2017-10-05.
CPL Pubid: 252360

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)