Evaluation of a new recursion induction principle for automated induction

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/250011
Download file(s):
File Description SizeFormat 
250011.pdfFulltext653.21 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Evaluation of a new recursion induction principle for automated induction
Authors: Andersson, Linnea
Wahlström, Andreas
Abstract: Structural induction is a powerful tool for proving properties of functions with recursive structure, but it is useless when the functions do not preserve the structure of the input. Many of today’s cutting-edge automated theorem provers use structural induction, which makes it impossible for them to prove properties about non-structurally recursive functions. We introduce a new induction principle, where the induction is done over a function application. This principle makes it possible to prove properties about non-structurally recursive functions automatically. We compare structural and application induction and the result indicates that application induction is the more powerful induction method, proving more properties, even though structural induction tends to be faster.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2017
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/250011
Collection:Examensarbeten för masterexamen // Master Theses

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.