Abstract: Disjunctive finitary programs are a class of logic programs admitting function symbols and hence infinite domains. They have very good computational properties, for example ground queries are decidable while in the general case the stable model semantics is Pi^1_1-hard. In this paper we prove that a larger class of programs, called finitely recursive programs, preserves most of the good properties of finitary programs under the stable model semantics, namely: (i) finitely recursive programs enjoy a compactness property; (ii) inconsistency checking and skeptical reasoning are semidecidable; (iii) skeptical resolution is complete for normal finitely recursive programs. Moreover, we show how to check inconsistency and answer skeptical queries using finite subsets of the ground program instantiation. We achieve this by extending the splitting sequence theorem by Lifschitz and Turner: We prove that if the input program P is finitely recursive, then the partial stable models determined by any smooth splitting omega-sequence converge to a stable model of P.

On finitely recursive programs / Baselice, Sabrina; Bonatti, PIERO ANDREA; Criscuolo, Giovanni. - In: THEORY AND PRACTICE OF LOGIC PROGRAMMING. - ISSN 1471-0684. - STAMPA. - 9:2(2009), pp. 213-238.

On finitely recursive programs

BASELICE, SABRINA;BONATTI, PIERO ANDREA;CRISCUOLO, GIOVANNI
2009

Abstract

Abstract: Disjunctive finitary programs are a class of logic programs admitting function symbols and hence infinite domains. They have very good computational properties, for example ground queries are decidable while in the general case the stable model semantics is Pi^1_1-hard. In this paper we prove that a larger class of programs, called finitely recursive programs, preserves most of the good properties of finitary programs under the stable model semantics, namely: (i) finitely recursive programs enjoy a compactness property; (ii) inconsistency checking and skeptical reasoning are semidecidable; (iii) skeptical resolution is complete for normal finitely recursive programs. Moreover, we show how to check inconsistency and answer skeptical queries using finite subsets of the ground program instantiation. We achieve this by extending the splitting sequence theorem by Lifschitz and Turner: We prove that if the input program P is finitely recursive, then the partial stable models determined by any smooth splitting omega-sequence converge to a stable model of P.
2009
On finitely recursive programs / Baselice, Sabrina; Bonatti, PIERO ANDREA; Criscuolo, Giovanni. - In: THEORY AND PRACTICE OF LOGIC PROGRAMMING. - ISSN 1471-0684. - STAMPA. - 9:2(2009), pp. 213-238.
File in questo prodotto:
File Dimensione Formato  
345468.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: Accesso privato/ristretto
Dimensione 248.16 kB
Formato Adobe PDF
248.16 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS 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/11588/345468
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact