Seminar 17 Feb, 2012

Automated runtime complexity analysis of Prolog programs

 

For term rewrite systems (TRSs), a huge number of automated termination analysis techniques have been developed during the last decades, and by automated transformations of Prolog programs to TRSs, these techniques can also be used to prove termination of Prolog programs. Very recently, techniques for automated termination analysis of TRSs have been adapted to prove asymptotic upper bounds for the runtime complexity of TRSs automatically.  In this talk, we present ongoing work to transform Prolog programs automatically into TRSs in such a way that the resulting TRSs have at least the same asymptotic upper complexity bound. Thus, techniques for complexity analysis of TRSs can be applied to prove upper complexity bounds for Prolog programs.