Yet another proof of the strong equivalence between propositional theories and logic programs

Joohyung Lee, Ravi Palla

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

Abstract

Recently, the stable model semantics was extended to the syntax of arbitrary propositional formulas, which are beyond the traditional rule form. Cabalar and Ferraris, as well as Cabalar, Pearce, and Valverde, showed that any propositional theory under the stable model semantics can be turned into a logic program. In this note, we present yet another proof of this result. Unlike the other approaches that are based on the logic of here-and-there, our proof uses familiar properties of classical logic. Based on this idea, we present a prototype implementation for computing stable models of propositional theories using the answer set solver DLV. We also note that every first-order formula under the stable model semantics is strongly equivalent to a prenex normal form whose matrix has the form of a logic program.

Original languageEnglish (US)
Title of host publicationCEUR Workshop Proceedings
Pages1-12
Number of pages12
Volume265
StatePublished - 2007
EventWorkshop on Correspondence and Equivalence for Nonmonotonic Theories, CENT 2007, Colocated with 9th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2007 - Tempe, AZ, United States
Duration: May 14 2007May 14 2007

Other

OtherWorkshop on Correspondence and Equivalence for Nonmonotonic Theories, CENT 2007, Colocated with 9th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2007
CountryUnited States
CityTempe, AZ
Period5/14/075/14/07

Fingerprint

Semantics

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Lee, J., & Palla, R. (2007). Yet another proof of the strong equivalence between propositional theories and logic programs. In CEUR Workshop Proceedings (Vol. 265, pp. 1-12)

Yet another proof of the strong equivalence between propositional theories and logic programs. / Lee, Joohyung; Palla, Ravi.

CEUR Workshop Proceedings. Vol. 265 2007. p. 1-12.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Lee, J & Palla, R 2007, Yet another proof of the strong equivalence between propositional theories and logic programs. in CEUR Workshop Proceedings. vol. 265, pp. 1-12, Workshop on Correspondence and Equivalence for Nonmonotonic Theories, CENT 2007, Colocated with 9th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2007, Tempe, AZ, United States, 5/14/07.
Lee J, Palla R. Yet another proof of the strong equivalence between propositional theories and logic programs. In CEUR Workshop Proceedings. Vol. 265. 2007. p. 1-12
@inproceedings{964ee553704a4f2a8e0e8f5e3f45f615,
title = "Yet another proof of the strong equivalence between propositional theories and logic programs",
abstract = "Recently, the stable model semantics was extended to the syntax of arbitrary propositional formulas, which are beyond the traditional rule form. Cabalar and Ferraris, as well as Cabalar, Pearce, and Valverde, showed that any propositional theory under the stable model semantics can be turned into a logic program. In this note, we present yet another proof of this result. Unlike the other approaches that are based on the logic of here-and-there, our proof uses familiar properties of classical logic. Based on this idea, we present a prototype implementation for computing stable models of propositional theories using the answer set solver DLV. We also note that every first-order formula under the stable model semantics is strongly equivalent to a prenex normal form whose matrix has the form of a logic program.",
author = "Joohyung Lee and Ravi Palla",
year = "2007",
language = "English (US)",
volume = "265",
pages = "1--12",
booktitle = "CEUR Workshop Proceedings",

}

TY - GEN

T1 - Yet another proof of the strong equivalence between propositional theories and logic programs

AU - Lee, Joohyung

AU - Palla, Ravi

PY - 2007

Y1 - 2007

N2 - Recently, the stable model semantics was extended to the syntax of arbitrary propositional formulas, which are beyond the traditional rule form. Cabalar and Ferraris, as well as Cabalar, Pearce, and Valverde, showed that any propositional theory under the stable model semantics can be turned into a logic program. In this note, we present yet another proof of this result. Unlike the other approaches that are based on the logic of here-and-there, our proof uses familiar properties of classical logic. Based on this idea, we present a prototype implementation for computing stable models of propositional theories using the answer set solver DLV. We also note that every first-order formula under the stable model semantics is strongly equivalent to a prenex normal form whose matrix has the form of a logic program.

AB - Recently, the stable model semantics was extended to the syntax of arbitrary propositional formulas, which are beyond the traditional rule form. Cabalar and Ferraris, as well as Cabalar, Pearce, and Valverde, showed that any propositional theory under the stable model semantics can be turned into a logic program. In this note, we present yet another proof of this result. Unlike the other approaches that are based on the logic of here-and-there, our proof uses familiar properties of classical logic. Based on this idea, we present a prototype implementation for computing stable models of propositional theories using the answer set solver DLV. We also note that every first-order formula under the stable model semantics is strongly equivalent to a prenex normal form whose matrix has the form of a logic program.

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

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

M3 - Conference contribution

AN - SCOPUS:84886614917

VL - 265

SP - 1

EP - 12

BT - CEUR Workshop Proceedings

ER -