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 answer set programs that include function symbols, recent work has identified classes for which grounding routines can terminate either on the entire program [Calimeri et al. 2008] or on suitable queries [Baselice et al. 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 paper we provide a formal definition of tabling with subgoal abstraction resulting in the SLG SA algorithm. Moreover, we discuss a declarative characterization of the queries and programs for which SLG SA terminates. We call this class strongly bounded term-size programs and show its equivalence to programs with finite wellfounded models. For normal programs strongly bounded term-size programs strictly includes the finitely ground programs of [Calimeri et al. 2008]. SLG SA has an asymptotic complexity on strongly bounded termsize 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.

Terminating Evaluation of Logic Programs with Finite Three-Valued Models

RIGUZZI, Fabrizio;
2014

Abstract

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 answer set programs that include function symbols, recent work has identified classes for which grounding routines can terminate either on the entire program [Calimeri et al. 2008] or on suitable queries [Baselice et al. 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 paper we provide a formal definition of tabling with subgoal abstraction resulting in the SLG SA algorithm. Moreover, we discuss a declarative characterization of the queries and programs for which SLG SA terminates. We call this class strongly bounded term-size programs and show its equivalence to programs with finite wellfounded models. For normal programs strongly bounded term-size programs strictly includes the finitely ground programs of [Calimeri et al. 2008]. SLG SA has an asymptotic complexity on strongly bounded termsize 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.
2014
Riguzzi, Fabrizio; Swift, T.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11392/2204212
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 2
social impact