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

Hipster: Integrating theory exploration in a proof assistant

Moa Johansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Dan Rosén (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Nicholas Smallbone (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science (0302-9743). Vol. 8543 (2014), p. 108-122.
[Konferensbidrag, refereegranskat]

This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new interesting lemmas in a given theory development. Hipster can be used in two main modes. The first is exploratory mode, used for automatically generating basic lemmas about a given set of datatypes and functions in a new theory development. The second is proof mode, used in a particular proof attempt, trying to discover the missing lemmas which would allow the current goal to be proved. Hipster's proof mode complements and boosts existing proof automation techniques that rely on automatically selecting existing lemmas, by inventing new lemmas that need induction to be proved. We show example uses of both modes.



Denna post skapades 2015-05-06. Senast ändrad 2016-06-27.
CPL Pubid: 216678

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

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


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Datavetenskap (datalogi)

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:


Theory Exploration and Inductive Theorem Proving