An Incremental Answer Set Programming Based System for Finite Model Computation
View/ Open
Author(s)
Gebser, Martin
Schaub, Torsten
Sabuncu, Orkunt
Griffith University Author(s)
Year published
2010
Metadata
Show full item recordAbstract
We address the problem of Finite Model Computation (FMC) of firstorder 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 ...
View more >We address the problem of Finite Model Computation (FMC) of firstorder 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 Automated Theorem Proving (ATP) competition.
View less >
View more >We address the problem of Finite Model Computation (FMC) of firstorder 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 Automated Theorem Proving (ATP) competition.
View less >
Conference Title
12th European Conference on Logics in Artificial Intelligence Proceedings
Copyright Statement
© 2010 Springer Berlin / Heidelberg. This is the author-manuscript version of this paper. Reproduced in accordance with the copyright policy of the publisher. The original publication is available at www.springerlink.com