Abstract
Answer set programming (ASP) has been a focus as a new declarative programming paradigm. The basic algorithm to compute answer sets based on a model generation theorem proving scheme has been proposed by Inoue [7]. The implementation of the basic algorithm, however, generates enormous redundant combinations of hypotheses. In this paper, we propose a new implementation method based on a minimal model generator MM-MGTP [5], including a new data structure called modal disjunction buffer and some extended operations to avoid redundancy. Some experimental results are shown for comparison with the naive implementation and other systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bennett, F.: Quasigroup Identities and Mendelsohn Designs. Canadian Journal of Mathematics 41, 341–368 (1989)
Eiter, T., Faber, W., Koch, C., Leone, N., Pfeifer, G.: Dlv - a system for declarative problem solving. In: Proc. of the 8th Int. Workshop on Non-Monotonic Reasoning, NMR 2000 (2000)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Proc. Fifth Int. Conf. and Symp. of Logic Programming, Seattle, WA, pp. 1070–1080 (1988)
Hähnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, The MIT Press, Cambridge (2002)
Hasegawa, R., Fujita, H., Koshimura, M.: Efficient Minimal Model Generation Using Branching Lemmas. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 184–199. Springer, Heidelberg (2000)
Hasegawa, R., Fujita, H., Koshimura, M., Shirai, Y.: A Model Generation Theorem Prover MGTP for First-Order Logic. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2408, pp. 178–213. Springer, Heidelberg (2002)
Inoue, K., Koshimura, M., Hasegawa, R.: Embedding Negation as Failure into a Model Generation Theorem Prover. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 400–415. Springer, Heidelberg (1992)
Inoue, K., Sakama, C.: A Fixpoint Characterization of Abductive Logic Programs. Journal of Logic Programming 27(2), 107–136 (1996)
Lin, F., Zhao, Y.: ASSAT: Computing Answer Sets of A Logic Program By SAT Solvers. In: Proc. of 18th AAAI, pp. 112–118. AAAI Press, Menlo Park (2002)
Niemelä, I., Simons, P.: Efficient Implementation of theWell-founded and Stable Model Semantics. Research report 7-96, University of Koblenz-Landau (1996)
Shirai, Y., Hasegawa, R.: Two Approaches for Finite-Domain Constraint Satisfaction Problem - CP and MGTP. In: Sterling, L. (ed.) Proc. 12th Int. Conf. on Logic Programming, pp. 249–263. MIT Press, Cambridge (1995)
Shimajiri, Y., Seki, H., Itoh, H.: Incorporating a Pruning Strategy into the Computation of Stable Models. Journal of the Japanese Society for Artificial Intelligence 12(5) (1997) (in Japanese)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shirai, Y., Hasegawa, R. (2004). Answer Set Computation Based on a Minimal Model Generation Theorem Prover. In: Zhang, C., W. Guesgen, H., Yeap, WK. (eds) PRICAI 2004: Trends in Artificial Intelligence. PRICAI 2004. Lecture Notes in Computer Science(), vol 3157. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28633-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-28633-2_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22817-2
Online ISBN: 978-3-540-28633-2
eBook Packages: Springer Book Archive