Terminating evaluation of logic programs with finite three-valued models

Fabrizio Riguzzi, Terrance Swift

Research output: Contribution to journalArticle

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 ar 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 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 Calimeri et al. [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.

Original languageEnglish (US)
Article number32
JournalACM Transactions on Computational Logic
Volume15
Issue number4
DOIs
StatePublished - Sep 16 2014
Externally publishedYes

Fingerprint

Computer systems programming
Electric grounding
Logic Programs
Evaluation
Model
Terminate
Term
Termination
Query
Answer Set Programming
Evaluation Method

Keywords

  • Tabled logic programming
  • Termination

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science
  • Computational Mathematics
  • Logic

Cite this

Terminating evaluation of logic programs with finite three-valued models. / Riguzzi, Fabrizio; Swift, Terrance.

In: ACM Transactions on Computational Logic, Vol. 15, No. 4, 32, 16.09.2014.

Research output: Contribution to journalArticle

@article{57a1580adc8944b2a2732e7b6d5d173f,
title = "Terminating evaluation of logic programs with finite three-valued models",
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 ar 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 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 Calimeri et al. [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.",
keywords = "Tabled logic programming, Termination",
author = "Fabrizio Riguzzi and Terrance Swift",
year = "2014",
month = "9",
day = "16",
doi = "10.1145/2629337",
language = "English (US)",
volume = "15",
journal = "ACM Transactions on Computational Logic",
issn = "1529-3785",
publisher = "Association for Computing Machinery (ACM)",
number = "4",

}

TY - JOUR

T1 - Terminating evaluation of logic programs with finite three-valued models

AU - Riguzzi, Fabrizio

AU - Swift, Terrance

PY - 2014/9/16

Y1 - 2014/9/16

N2 - 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 [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 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 Calimeri et al. [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.

AB - 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 [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 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 Calimeri et al. [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.

KW - Tabled logic programming

KW - Termination

UR - http://www.scopus.com/inward/record.url?scp=84905261374&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84905261374&partnerID=8YFLogxK

U2 - 10.1145/2629337

DO - 10.1145/2629337

M3 - Article

VL - 15

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 4

M1 - 32

ER -