Termination Analysis of Logic Programs – Tutorial at IJCAI 2015

Sergio Greco and I will give a tutorial at IJCAI 2015 on Termination Analysis of Logic Programs.
A preliminary version of the tutorial slides is available here.

There are several domains where ensuring termination of the evaluation of logic programs is a central problem. In answer set programming, when the language is enriched with function symbols common inference tasks become undecidable. Guaranteeing that a program evaluation terminates is crucial for the implementation of answer set solvers. Techniques developed in this setting can be directly applied to Datalog and thus turn out to be profitable to define decidable query languages. In ontology-based data access, knowledge bases can include existentially quantified rules and their enforcement is not guaranteed to terminate—determining if their application ends is a central issue for ontological query answering.
Unfortunately, checking if a program evaluation terminates is in general undecidable. One way of dealing with this issue is to define (sufficient) conditions that ensure termination. Recent years have witnessed a great deal of interest in the problem of identifying restricted classes of logic programs whose evaluation is guaranteed to terminate. The tutorial presents and compares the main approaches in this area by highlighting the different perspectives they adopt in logic program analysis and their applications to different settings.