Using linear constraints for logic program termination analysis
From MaRDI portal
Publication:4593032
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.
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
Cites work
- scientific article; zbMATH DE number 25190 (Why is no real title available?)
- scientific article; zbMATH DE number 1884395 (Why is no real title available?)
- scientific article; zbMATH DE number 794240 (Why is no real title available?)
- Automated termination analysis for logic programs with cut
- Automated termination proofs for logic programs by term rewriting
- Checking termination of bottom-up evaluation of logic programs with function symbols
- Complexity of the unification algorithm for first-order expressions
- Computable Functions in ASP: Theory and Implementation
- Disjunctive ASP with functions: decidable queries and effective computation
- Fast offline partial evaluation of logic programs
- Incomplete data and data dependencies in relational databases
- Logic Programming
- Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
- Matrix interpretations for proving termination of term rewriting
- Non-termination analysis of logic programs with integer arithmetics
- On finitely recursive programs
- On termination of meta-programs
- On the complexity of integer programming
- On the termination of logic programs with function symbols
- One More Decidable Class of Finitely Ground Programs
- Reasoning with infinite stable models
- Root-Labeling
- Terminating evaluation of logic programs with finite three-valued models
- Termination Analysis of Logic Programs Based on Dependency Graphs
- Termination of logic programs: Transformational methods revisited
- Termination of logic programs: the never-ending story
- Termination of narrowing via termination of rewriting
- Termination of term rewriting using dependency pairs
- Termination proofs for logic programs with tabling
- Testing logic programs for local stratification
- Total termination of term rewriting
- 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
Cited in
(4)
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)
