An incremental answer set programming based system for finite model computation
- We address the problem of Finite Model Computation (FMC) of first-order theories and show that FMC can efficiently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE's 2009 Automated Theorem Proving (ATP) competition on the respective benchmark collection.
| Verfasserangaben: | Martin GebserORCiD, Orkunt Sabuncu, Torsten H. SchaubORCiDGND |
|---|---|
| DOI: | https://doi.org/10.3233/AIC-2011-0496 |
| ISSN: | 0921-7126 |
| Titel des übergeordneten Werks (Englisch): | AI communications : AICOM ; the European journal on artificial intelligence |
| Verlag: | IOS Press |
| Verlagsort: | Amsterdam |
| Publikationstyp: | Wissenschaftlicher Artikel |
| Sprache: | Englisch |
| Jahr der Erstveröffentlichung: | 2011 |
| Erscheinungsjahr: | 2011 |
| Datum der Freischaltung: | 26.03.2017 |
| Freies Schlagwort / Tag: | Incremental answer set programming; finite model computation |
| Band: | 24 |
| Ausgabe: | 2 |
| Seitenanzahl: | 18 |
| Erste Seite: | 195 |
| Letzte Seite: | 212 |
| Fördernde Institution: | German Science Foundation (DFG) [SCHA 550/8-1/2] |
| Organisationseinheiten: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science |
| Peer Review: | Referiert |
| Name der Einrichtung zum Zeitpunkt der Publikation: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik |
