Evaluation of a new recursion induction principle for automated induction

Visa enkel post
dc.contributor.authorAndersson, Linnea
dc.contributor.authorWahlström, Andreas
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)sv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineering (Chalmers)en
dc.date.accessioned2019-07-03T14:28:25Z
dc.date.available2019-07-03T14:28:25Z
dc.date.issued2017
dc.description.abstractStructural 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.
dc.identifier.urihttps://hdl.handle.net/20.500.12380/250011
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectData- och informationsvetenskap
dc.subjectComputer and Information Science
dc.titleEvaluation of a new recursion induction principle for automated induction
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
dc.type.uppsokH
local.programmeComputer science – algorithms, languages and logic (MPALG), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
250011.pdf
Storlek:
653.21 KB
Format:
Adobe Portable Document Format
Beskrivning:
Fulltext
Ladda ner
Samling
Examensarbeten för masterexamen