Termination Criteria for Datalog with Function Symbols

Enriching Datalog with function symbols makes modeling easier, increases the expressive power, and allows us to deal with infinite domains. However, this comes at a cost: common inference tasks become undecidable. To cope with this issue, recent research has focused on finding trade-offs between expressivity and decidability by identifying classes of Datalog programs allowing only a limited use of function symbols but guaranteeing decidability of common inference tasks.
In this paper, we provide a survey of current termination criteria, which define conditions guaranteeing that a Datalog program (possibly with function symbols) has a finite number of stable models, each of them is of finite size and can be computed. We also present a technique which can be used in conjunction with current termination criteria to improve them.