Logic programming with function symbols: Checking termination of bottom-up evaluation

Function symbols are an important feature in logic programming, as they often make modeling easier and the resulting encodings more readable and concise. In addition, they increase the expressive power and allow us to overcome the inability of dealing with infinite domains. The main problem with the introduction of function symbols is that common inference tasks (e.g., cautious and brave reasoning) become undecidable. In order to cope with this issue, recent research has focused on identifying classes of logic programs that impose some limitations on the use of function symbols but guarantee decidability of inference tasks. This has led to several termination criteria, that is, (decidable) sufficient conditions ensuring that the bottom-up evaluation of a program terminates. This talk will survey termination criteria recently proposed in the literature. It will also discuss an orthogonal technique, based on program adornment, that can be used in conjunction with current termination criteria to make them more effective. Joint work with Marco Calautti, Sergio Greco, and Irina Trubitsyna.