Checking termination of bottom-up evaluation of logic programs with function symbols
From MaRDI portal
Publication:4593017
DOI10.1017/S1471068414000623zbMATH Open1379.68051arXiv1407.2106OpenAlexW2135520900MaRDI QIDQ4593017FDOQ4593017
Authors: Marco Calautti, Sergio Greco, Francesca Spezzano, Irina Trubitsyna 
Publication date: 9 November 2017
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
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).
Full work available at URL: https://arxiv.org/abs/1407.2106
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
- Extending and implementing the stable model semantics
- A framework for testing safety and effective computability
- 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
- Data exchange: semantics and query answering
- Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
- On the power of magic
- 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
- Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15--17, 2008. Proceedings
- Termination of narrowing via termination of rewriting
- On termination of meta-programs
- Optimization of bound disjunctive queries with constraints
- 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
- Non-termination Analysis of Logic Programs Using Types
- Logic Programming
- Total termination of term rewriting
- Algebraic methodology and software technology. 5th international conference, AMAST '96, Munich, Germany, July 1-5, 1996. Proceedings
- Automated termination proofs for logic programs by term rewriting
- Dependency triples for improving termination analysis of logic programs with cut
- Disjunctive ASP with functions: decidable queries and effective computation
- On finitely recursive programs
- A practical analysis of non-termination in large logic programs
- Termination Analysis of Logic Programs Based on Dependency Graphs
- The dependency triple framework for termination of logic programs
Cited In (6)
- Index sets for finite normal predicate logic programs with function symbols
- On the termination of 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
- What is answer set programming to propositional satisfiability
- Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols
Uses Software
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)
