Using linear constraints for logic program termination analysis
From MaRDI portal
Publication:4593032
DOI10.1017/S1471068416000077zbMATH Open1379.68050arXiv1512.04097OpenAlexW3104721040MaRDI QIDQ4593032FDOQ4593032
Authors: Marco Calautti, Sergio Greco, Cristian Molinaro, Irina Trubitsyna 
Publication date: 9 November 2017
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Abstract: It is widely acknowledged that function symbols are an important feature in answer set programming, as they make modeling easier, increase the expressive power, and allow us to deal with infinite domains. The main issue with their introduction is that the evaluation of a program might not terminate and checking whether it terminates or not is undecidable. To cope with this problem, several classes of logic programs have been proposed where the use of function symbols is restricted but the program evaluation termination is guaranteed. Despite the significant body of work in this area, current approaches do not include many simple practical programs whose evaluation terminates. In this paper, we present the novel classes of rule-bounded and cycle-bounded programs, which overcome different limitations of current approaches by performing a more global analysis of how terms are propagated from the body to the head of rules. Results on the correctness, the complexity, and the expressivity of the proposed approach are provided.
Full work available at URL: https://arxiv.org/abs/1512.04097
Recommendations
- On the termination of logic programs with function symbols
- Checking termination of bottom-up evaluation of logic programs with function symbols
- Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
- Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols
- scientific article; zbMATH DE number 1088021
answer set programmingfunction symbolsstable modelsbottom-up evaluationprogram evaluation termination
Cites Work
- Well–definedness and efficient inference for probabilistic logic programming under the distribution semantics
- \(\mathcal {NPD}\)atalog: A logic language for expressing \(\mathcal {NP}\) search and optimization problems
- Title not available (Why is that?)
- Title not available (Why is that?)
- One More Decidable Class of Finitely Ground Programs
- On the termination of logic programs with function symbols
- Computable Functions in ASP: Theory and Implementation
- Reasoning with infinite stable models
- Termination of term rewriting using dependency pairs
- Terminating evaluation of logic programs with finite three-valued models
- On the complexity of integer programming
- Matrix interpretations for proving termination of term rewriting
- Termination of logic programs: Transformational methods revisited
- Automated termination analysis for logic programs with cut
- Title not available (Why is that?)
- Termination of logic programs: the never-ending story
- Complexity of the unification algorithm for first-order expressions
- Termination of narrowing via termination of rewriting
- On termination of meta-programs
- Logic Programming
- Termination proofs for logic programs with tabling
- Testing logic programs for local stratification
- Total termination of term rewriting
- Checking termination of bottom-up evaluation of logic programs with function symbols
- Automated termination proofs for logic programs by term rewriting
- Incomplete data and data dependencies in relational databases
- Fast offline partial evaluation of logic programs
- Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
- Non-termination analysis of logic programs with integer arithmetics
- Disjunctive ASP with functions: decidable queries and effective computation
- On finitely recursive programs
- Termination Analysis of Logic Programs Based on Dependency Graphs
- Root-Labeling
Cited In (4)
Uses Software
This page was built for publication: Using linear constraints for logic program termination analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4593032)
