Recent years, program verification has become a more and more key problem in computer science. Solving recurrences, as a vital part of program verification system, has also attracted much more interests from outside. Although there exist some well-known systems like Sympy and Mathematica which help computing closed-form solutions for recurrences, these tools have limited functions and sometimes don’t work. Especially, those existing systems in literature have no ability of finding solutions to recurrences with conditions. In this thesis, a system of finding closed form solutions to recurrences using machine theorem discovery is presented. Our proposed method can successfully address not only lots of common recurrences without conditions, but also multiple kinds of conditional...[ Read more ]

Recent years, program verification has become a more and more key problem in computer science. Solving recurrences, as a vital part of program verification system, has also attracted much more interests from outside. Although there exist some well-known systems like Sympy and Mathematica which help computing closed-form solutions for recurrences, these tools have limited functions and sometimes don’t work. Especially, those existing systems in literature have no ability of finding solutions to recurrences with conditions. In this thesis, a system of finding closed form solutions to recurrences using machine theorem discovery is presented. Our proposed method can successfully address not only lots of common recurrences without conditions, but also multiple kinds of conditional recurrences with a single condition and nested conditional recurrences with more than one conditions, demonstrated by a systematic experimental evaluation. Of course, to find closed form solutions to recurrences with conditions is the most significant contribution of this work.