• search hit 1 of 6
Back to Result List

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.

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Author:Martin GebserORCiD, Orkunt Sabuncu, Torsten SchaubORCiDGND
ISSN:0921-7126 (print)
Parent Title (English):AI communications : AICOM ; the European journal on artificial intelligence
Publisher:IOS Press
Place of publication:Amsterdam
Document Type:Article
Year of first Publication:2011
Year of Completion:2011
Release Date:2017/03/26
Tag:Incremental answer set programming; finite model computation
First Page:195
Last Page:212
Funder:German Science Foundation (DFG) [SCHA 550/8-1/2]
Organizational units:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science
Peer Review:Referiert
Institution name at the time of publication:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik