Abstract
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 Automated Theorem Proving (ATP) competition.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Kluwer Academic, Dordrecht (2004)
Bibel, W.: Automated Theorem Proving. Vieweg (1987)
Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University, Cambridge (2003)
Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Thiele, S.: Engineering an incremental ASP solver. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 190–205. Springer, Heidelberg (2008)
Zhang, J., Huang, Z.: Reducing symmetries to generate easier SAT instances. Electronic Notes in Theoretical Computer Science 125(3), 149–164 (2005)
Tammet, T.: Finite model building: Improvements and comparisons. In: Baumgartner, P., Fermüller, C. (eds.) Proceedings of the Workshop on Model Computation — Principles, Algorithms, Applications, MODEL 2003 (2003)
McCune, W.: A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical Report ANL/MCS-TM-194, Argonne National Laboratory (1994)
Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model finding. In: Baumgartner, P., Fermüller, C. (eds.) Proceedings of the Workshop on Model Computation — Principles, Algorithms, Applications, MODEL 2003 (2003)
Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability. IOS (2009)
Zhang, J., Zhang, H.: SEM: A system for enumerating models. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI 1995), pp. 298–303. Morgan Kaufmann, San Francisco (1995)
Zhang, J.: Constructing finite algebras with FALCON. Journal of Automated Reasoning 17(1), 1–22 (1996)
Syrjänen, T.: Lparse 1.0 user’s manual, http://www.tcs.hut.fi/Software/smodels/lparse.ps.gz
Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Thiele, S.: A user’s guide to gringo, clasp, clingo, and iclingo, http://potassco.sourceforge.net
Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artificial Intelligence 138(1-2), 181–234 (2002)
Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. Journal of Applied Logic 7(1), 58–74 (2009)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Sabuncu, O., Alpaslan, F.: Computing answer sets using model generation theorem provers. In: Costantini, S., Watson, R. (eds.) Proceedings of the 4th International Workshop on Answer Set Programming (ASP 2007), pp. 225–240 (2007)
Lierler, Y., Lifschitz, V.: Logic programs vs. first-order formulas in textual inference, http://z.cs.utexas.edu/users/ai-lab/publications_recent.php
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gebser, M., Sabuncu, O., Schaub, T. (2010). An Incremental Answer Set Programming Based System for Finite ModelComputation. In: Janhunen, T., Niemelä, I. (eds) Logics in Artificial Intelligence. JELIA 2010. Lecture Notes in Computer Science(), vol 6341. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15675-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-15675-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15674-8
Online ISBN: 978-3-642-15675-5
eBook Packages: Computer ScienceComputer Science (R0)