Static Termination Analysis for Prolog Using Term Rewriting and SAT Solving

摘要

The dissertation "Static Termination Analysis for Prolog using Term Rewriting and SAT Solving" (Schneider-Kamp in Dissertation, RWTH Aachen University, 2008) presents a fresh approach to automated termination analysis of Prolog programs. This approach is based on the following three main concepts: the use of program transformations to obtain simpler termination problems, a framework for modular termination analysis, and the encoding of search problems into satisfiability of propositional logic (SAT) for efficient generation of ranking functions.