Checking termination of bottom-up evaluation of logic programs with function symbols
From MaRDI portal
Publication:4593017
Abstract: Recently, there has been an increasing interest in the bottom-up evaluation of the semantics of logic programs with complex terms. The presence of function symbols in the program may render the ground instantiation infinite, and finiteness of models and termination of the evaluation procedure, in the general case, are not guaranteed anymore. Since the program termination problem is undecidable in the general case, several decidable criteria (called program termination criteria) have been recently proposed. However, current conditions are not able to identify even simple programs, whose bottom-up execution always terminates. The paper introduces new decidable criteria for checking termination of logic programs with function symbols under bottom-up evaluation, by deeply analyzing the program structure. First, we analyze the propagation of complex terms among arguments by means of the extended version of the argument graph called propagation graph. The resulting criterion, called Gamma-acyclicity, generalizes most of the decidable criteria proposed so far. Next, we study how rules may activate each other and define a more powerful criterion, called safety. This criterion uses the so-called safety function able to analyze how rules may activate each other and how the presence of some arguments in a rule limits its activation. We also study the application of the proposed criteria to bound queries and show that the safety criterion is well-suited to identify relevant classes of programs and bound queries. Finally, we propose a hierarchy of classes of terminating programs, called k-safety, where the k-safe class strictly includes the (k-1)-safe class. Note: To appear in Theory and Practice of Logic Programming (TPLP).
Recommendations
- On the termination of logic programs with function symbols
- Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols
- Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
- Using linear constraints for logic program termination analysis
- Depth-bounded bottom-up evaluation of logic programs
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?)
- A framework for testing safety and effective computability
- A practical analysis of non-termination in large logic programs
- Algebraic methodology and software technology. 5th international conference, AMAST '96, Munich, Germany, July 1-5, 1996. Proceedings
- Automated termination analysis for logic programs with cut
- Automated termination proofs for logic programs by term rewriting
- Complexity of the unification algorithm for first-order expressions
- Computable Functions in ASP: Theory and Implementation
- Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
- Data exchange: semantics and query answering
- Dependency triples for improving termination analysis of logic programs with cut
- Disjunctive ASP with functions: decidable queries and effective computation
- Extending and implementing the stable model semantics
- Logic Programming
- Logic programming and nonmonotonic reasoning. 9th international conference, LPNMR 2007, Tempe, AZ, USA, May 15--17, 2007. Proceedings
- Logics in artificial intelligence. 8th European conference, JELIA 2002, Cosenza, Italy, September 23--26, 2002. Proceedings
- Matrix interpretations for proving termination of term rewriting
- Non-termination Analysis of Logic Programs Using Types
- On finitely recursive programs
- On termination of meta-programs
- On the power of magic
- On the termination of logic programs with function symbols
- One More Decidable Class of Finitely Ground Programs
- Optimization of bound disjunctive queries with constraints
- Reasoning with infinite stable models
- Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15--17, 2008. Proceedings
- 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
- The dependency triple framework for termination of logic programs
- Total termination of term rewriting
Cited in
(6)- Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols
- On the termination of logic programs with function symbols
- Index sets for finite normal predicate logic programs with function symbols
- Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
- What is answer set programming to propositional satisfiability
- Using linear constraints for logic program termination analysis
This page was built for publication: Checking termination of bottom-up evaluation of logic programs with function symbols
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4593017)
