Termination Criteria for Datalog with Function Symbols.
Marco Calautti, Cristian Molinaro, Chiara Pulice, Irina Trubitsyna · Edinburgh Research Explorer (University of Edinburgh) · 2014
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.