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

Conditional Lemma Discovery and Recursion Induction in Hipster.

Moa Johansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Irene Lobo Valbuena (Institutionen för data- och informationsteknik (Chalmers))
Proceedings of the International Workshop on Automated Verification of Critical Systems (AVoCS). Electronic Communications of the EASST. Vol. 72 (2015),
[Konferensbidrag, refereegranskat]

Hipster is a theory exploration tool for the proof assistant Isabelle/HOL. It automatically discovers lemmas about given recursive functions and datatypes and proves them by induction. Previously, only equational properties could be discovered. Conditional lemmas, for example required when reasoning about sorting, has been beyond the scope of theory exploration. In this paper we describe an extension to Hipster to also support discovery and proof of conditional lemmas. We also present a new automated tactic, which uses recursion induction. Recursion induction follows the recursive structure of a function definition through its termina- tion order, as opposed to structural induction, which follows that of the datatype. We find that the addition of recursion induction increases the number of proofs completed automatically, both for conditional and equational statements.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-12-15.
CPL Pubid: 246146