## 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 language | English (US) |
---|---|

Title of host publication | CEUR Workshop Proceedings |

Pages | 1-12 |

Number of pages | 12 |

Volume | 265 |

State | Published - 2007 |

Event | 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 Duration: May 14 2007 → May 14 2007 |

### Other

Other | Workshop on Correspondence and Equivalence for Nonmonotonic Theories, CENT 2007, Colocated with 9th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2007 |
---|---|

Country/Territory | United States |

City | Tempe, AZ |

Period | 5/14/07 → 5/14/07 |

## ASJC Scopus subject areas

- Computer Science(all)