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

Theory Exploration and Inductive Theorem Proving

Dan Rosén (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Göteborg : Chalmers University of Technology, 2016. - 90 s.
[Licentiatavhandling]

We have built two state-of-the-art inductive theorem provers named HipSpec and Hipster. The main issue when automating proofs by induction is to discover essential helper lemmas. Our theorem provers use the technique theory exploration, which is a method to systematically discover interesting conclusions about a mathematical theory. We use the existing theory exploration system QuickSpec which conjectures properties for a program that seem to hold based on testing. The idea is to try to prove these explored conjectures together with the user-stated goal conjecture. By using this idea and connecting it with our previous work on Hip, the Haskell Inductive Prover, we were able to take new leaps in field of inductive theorem proving. Additionally, we have developed a benchmark suite named TIP, short for Tons of Inductive Problems, with benchmark problems for inductive theorem provers, and a tool box for converting and manipulating problems expressed in the TIP format. There were two main reasons to this initiative. Firstly, the inductive theorem proving field lacked a shared benchmark suite as well as a format. Secondly, the benchmarks that have been used were outdated: all contemporary provers would solve almost every problem. We have so far added hundreds of new challenges to the TIP suite to encourage further research.



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-02-12. Senast ändrad 2016-02-15.
CPL Pubid: 231969

 

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

Informations- och kommunikationsteknik
Programvaruteknik

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:


Automating Inductive Proofs using Theory Exploration


Hipster: Integrating theory exploration in a proof assistant


TIP: Tons of Inductive Problems


Tip: Tools for inductive provers


Examination

Datum: 2016-03-08
Tid: 13:15
Lokal: ED, Rännvägen 6, Chalmers Tekniska Högskola
Opponent: Jasmin Blanchette