DC FieldValueLanguage
dc.contributor.advisorKovacs, Laura-
dc.contributor.authorHajdu, Marton-
dc.date.accessioned2021-03-18T14:36:41Z-
dc.date.issued2021-
dc.date.submitted2021-03-
dc.identifier.urihttps://doi.org/10.34726/hss.2021.84140-
dc.identifier.urihttp://hdl.handle.net/20.500.12708/17065-
dc.descriptionArbeit an der Bibliothek noch nicht eingelangt - Daten nicht geprüft-
dc.descriptionAbweichender Titel nach Übersetzung der Verfasserin/des Verfassers-
dc.description.abstractFormally ensuring software reliability is challenging due to the growing complexity of software in terms of its size, used unbounded and inductive data types and supported workflow. As manual code analysis is not a viable solution, automated reasoning approaches are needed for proving software correct. There are several prominent methods addressing this challenge by (i) translating parts of a system to a logic-based formalism and (ii) using automated theorem proving to validate certain safety and liveness program properties.In this context a vital ingredient in automated reasoning is inductive reasoning, which can/must be used whenever repetition is present in a software component, e.g. loops or recursive data structures in computer programs or feedback loops in electric circuits. The two main branches in the literature are explicit and implicit induction. In this thesis focus on the former approach which is based broadly on the Noetherian well-founded induction principle. There is a plethora of research already done in this area with several automated theorem provers as well as proof assistants are equipped with inductive reasoning techniques. Some of the earliest ones are Nqthm/ACL2, Inka and Oyster/CLAM. Recently, modern automated theorem provers, such as ZipperPosition, CVC4 and Vampire, started to incorporate inductive types and reasoning.The aim of the proposed thesis is to advance the state-of-the art in inductive reasoning within first-order logic theorem proving, by using automating reasoning with recursive function definitions over inductive data types.en
dc.format101 Seiten-
dc.languageEnglish-
dc.language.isoen-
dc.subjectformal methodsen
dc.subjectinductive reasoningen
dc.subjectfirst-order theorem provingen
dc.subjectinductionen
dc.titleAutomating inductive reasoning with recursive functionsen
dc.typeThesisen
dc.typeHochschulschriftde
dc.identifier.doi10.34726/hss.2021.84140-
dc.publisher.placeWien-
tuw.thesisinformationTechnische Universität Wien-
tuw.publication.orgunitE192 - Institut für Logic and Computation-
dc.type.qualificationlevelDiploma-
dc.identifier.libraryidAC16168885-
dc.description.numberOfPages101-
dc.thesistypeDiplomarbeitde
dc.thesistypeDiploma Thesisen
item.openairetypeThesis-
item.openairetypeHochschulschrift-
item.openaccessfulltextOpen Access-
item.languageiso639-1en-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.grantfulltextopen-
item.fulltextwith Fulltext-
item.cerifentitytypePublications-
item.cerifentitytypePublications-
Appears in Collections:Thesis

Files in this item:


Page view(s)

27
checked on Jul 16, 2021

Download(s)

32
checked on Jul 16, 2021

Google ScholarTM

Check


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