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.
Similar concepts of term size'' have been considered to check termination of logic programs evaluated in a top-down fashion @cite_23 , to check local stratification of logic programs @cite_47 , in the context of partial evaluation to provide conditions for strong termination and quasi-termination @cite_32 @cite_2 , and in the context of tabled resolution @cite_24 @cite_36 . These approaches are geared to work under top-down evaluation, looking at how terms are propagated from the head to the body, while our approach is developed to work under bottom-up evaluation, looking at how terms are propagated from the body to the head. This gives rise to significant differences in how the program analysis is carried out, making one approach not applicable in the setting of the other. As a simple example, the rule @math leads to a non-terminating top-down evaluation, while it is completely harmless under bottom-up evaluation.
@cite_36 @cite_32 @cite_24 @cite_23 @cite_2 @cite_47
2108205915 2034471164 2963676309 1586790674 2044152416 2078854256
As evaluation methods for logic programs have become more sophisticated, the classes of programs for which termination can be guaranteed have expanded. From the perspective of ar set programs that include function symbols, recent work has identified classes for which grounding routines can terminate either on the entire program [ 2008] or on suitable queries [ 2009]. From the perspective of tabling, it has long been known that a tabling technique called subgoal abstraction provides good termination properties for definite programs [Tamaki and Sato 1986], and this result was recently extended to stratified programs via the class of bounded term-size programs [Riguzzi and Swift 2013]. In this article, we provide a formal definition of tabling with subgoal abstraction resulting in the SLGSA algorithm. Moreover, we discuss a declarative characterization of the queries and programs for which SLGSA terminates. We call this class strongly bounded term-size programs and show its equivalence to programs with finite well-founded models. For normal programs, strongly bounded term-size programs strictly includes the finitely ground programs of [2008]. SLGSA has an asymptotic complexity on strongly bounded term-size programs equal to the best known and produces a residual program that can be sent to an answer set programming system. Finally, we describe the implementation of subgoal abstraction within the SLG-WAM of XSB and provide performance results. One of the most important challenges in partial evaluation is the design of automatic methods for ensuring the termination of specialisation. It is well known that the termination of partial evaluation can be ensured when the considered computations are quasiterminating, i.e., when only finitely many different calls occur. In this work, we adapt the use of the so called size-change graphs to logic programming and introduce new sufficient conditions for strong (i.e., w.r.t. any computation rule) termination and quasi-termination. To the best of our knowledge, this is the first sufficient condition for the strong quasi-termination of logic programs. The class of strongly quasi-terminating logic programs, however, is too restrictive. Therefore, we also introduce an annotation procedure that combines the information from size-change graphs and the output of a traditional binding-time analysis. Annotated programs can then be used to guarantee termination of partial evaluation. We finally illustrate the usefulness of our approach by designing a simple partial evaluator in which termination is always ensured offline (i.e., statically). The distribution semantics is one of the most prominent approaches for the combination of logic programming and probability theory. Many languages follow this semantics, such as Independent Choice Logic, PRISM, pD, Logic Programs with Annotated Disjunctions (LPADs) and ProbLog. When a program contains functions symbols, the distribution semantics is well-defined only if the set of explanations for a query is finite and so is each explanation. Welldefinedness is usually either explicitly imposed or is achieved by severely limiting the class of allowed programs. In this paper we identify a larger class of programs for which the semantics is well-defined together with an efficient procedure for computing the probability of queries. Since LPADs offer the most general syntax, we present our results for them, but our results are applicable to all languages under the distribution semantics. We present the algorithm “Probabilistic Inference with Tabling and Answer subsumption” (PITA) that computes the probability of queries by transforming a probabilistic program into a normal program and then applying SLG resolution with answer subsumption. PITA has been implemented in XSB and tested on six domains: two with function symbols and four without. The execution times are compared with those of ProbLog, cplint and CVE. PITA was almost always able to solve larger problems in a shorter time, on domains with and without function symbols. One of the most important challenges in partial evaluation is the design of automatic methods for ensuring the termination of the process. In this work, we introduce sufficient conditions for the strong (i.e., independent of a computation rule) termination and quasi-termination of logic programs which rely on the construction of size-change graphs. We then present a fast binding-time analysis that takes the output of the termination analysis and annotates logic programs so that partial evaluation terminates. In contrast to previous approaches, the new binding-time analysis is conceptually simpler and considerably faster, scaling to medium-sized or even large examples. Abstract Locally stratified programs are a significant class of logic programs with negation for which both declarative and fixpoint semantics are well defined. Unfortunately in most cases recognizing local stratification is so hard a task that it has been conjectured that the problem is undecidable. Indeed, in this paper a formal proof of this undecidability is presented and rather general sufficient conditions for local stratification are introduced.