Author:

Abstract:

One of the main advantages of logic programs is that it allows to write declarative programs that very understandable. However, such a declarati ve program can be a very inefficient or even a non-terminating specifica tion of a problem. Therefore, one of the main concerns in program verifi cation of a logic proram, is proving that it terminates. If such a proof fails, non-termination analysis identifies the loop in the program. In this PhD, we prove non-termination based on symbolic derivation trees . These symbolic trees show (a part of) the derivations of all queries i n a certain class of queries. We implemented these symbolic trees and in troduced a new non-termination condition based on these trees. In the remainder of the PhD, these trees will be extended to use non-fai lure information. This allows to prove non-termination of more classes o f programs. Furthermore, we will investigate which non-logical features of Prolog can be incorporated in order to analyse more realistic Prolog programs.