Abstract
We extend the open answer set semantics for programs with generalized literals. Such extended programs (EPs) have interesting properties, e.g. the ability to express infinity axioms – EPs that have but infinite answer sets. However, reasoning under the open answer set semantics, in particular satisfiability checking of a predicate w.r.t. a program, is already undecidable for programs without generalized literals. In order to regain decidability, we restrict the syntax of EPs such that both rules and generalized literals are guarded. Via a translation to guarded fixed point logic (μGF), in which satisfiability checking is 2-EXPTIME-complete, we deduce 2-EXPTIME-completeness of satisfiability checking in such guarded EPs (GEPs). Bound GEPs are restricted GEPs with EXPTIME-complete satisfiability checking, but still sufficiently expressive to optimally simulate computation tree logic (CTL). We translate Datalog LITE programs to GEPs, establishing equivalence of GEPs under an open answer set semantics, alternation-free μGF, and Datalog LITE. Finally, we discuss ω-restricted logic programs under an open answer set semantics.
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
Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Reading (1995)
Van Benthem, J.: Dynamic Bits and Pieces. In: ILLC research report. University of Amsterdam (1997)
Chandra, A.K., Harel, D.: Horn Clauses and the Fixpoint Query Hierarchy. In: Proc. of PODS 1982, pp. 158–163. ACM Press, New York (1982)
Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 995–1072. Elsevier Science Publishers B.V., Amsterdam (1990)
Emerson, E.A., Clarke, E.M.: Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Sciene of Computer Programming 2(3), 241–266 (1982)
Gelfond, M., Lifschitz, V.: The Stable Model Semantics for Logic Programming. In: Proc. of ICLP 1988, pp. 1070–1080. MIT Press, Cambridge (1988)
Gelfond, M., Przymusinska, H.: Reasoning in Open Domains. In: Logic Programming and Non-Monotonic Reasoning, pp. 397–413. MIT Press, Cambridge (1993)
Gottlob, G., Grädel, E., Veith, H.: Datalog LITE: A deductive query language with linear time model checking. ACM Transactions on Computational Logic 3(1), 1–35 (2002)
Grädel, E.: Guarded Fixed Point Logic and the Monadic Theory of Trees. Theoretical Computer Science 288, 129–152 (2002)
Grädel, E.: Model Checking Games. In: Proceedings of WOLLIC 2002. Electronic Notes in Theoretical Computer Science, vol. 67. Elsevier, Amsterdam (2002)
Grädel, E., Walukiewicz, I.: Guarded Fixed Point Logic. In: Proc. of LICS 1999, pp. 45–54. IEEE Computer Society, Los Alamitos (1999)
Halevy, A., Mumick, I., Sagiv, Y., Shmueli, O.: Static Analysis in Datalog Extensions. Journal of the ACM 48(5), 971–1012 (2001)
Heymans, S., Van Nieuwenborgh, D., Vermeir, D.: Nonmonotonic Ontological and Rule-Based Reasoning with Extended Conceptual Logic Programs. In: Gómez-Pérez, A., Euzenat, J. (eds.) ESWC 2005. LNCS, vol. 3532, pp. 392–407. Springer, Heidelberg (2005)
Heymans, S., Van Nieuwenborgh, D., Vermeir, D.: Guarded Open Answer Set Programming. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 92–104. Springer, Heidelberg (2005)
Huth, M.R.A., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2000)
Lifschitz, V., Pearce, D., Valverde, A.: Strongly Equivalent Logic Programs. ACM Transactions on Computational Logic 2(4), 526–541 (2001)
Lloyd, J., Topor, R.: Making Prolog More Expressive. J. Log. Program. 1(3), 225–240 (1984)
Simons, P.: smodels homepage, http://www.tcs.hut.fi/Software/smodels/
Syrjänen, T.: Omega-restricted Logic Programs. In: Eiter, T., Faber, W., Truszczyński, M. (eds.) LPNMR 2001. LNCS (LNAI), vol. 2173, pp. 267–279. Springer, Heidelberg (2001)
Syrjänen, T.: Cardinality Constraint Programs. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 187–199. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heymans, S., Van Nieuwenborgh, D., Vermeir, D. (2006). Guarded Open Answer Set Programming with Generalized Literals. In: Dix, J., Hegner, S.J. (eds) Foundations of Information and Knowledge Systems. FoIKS 2006. Lecture Notes in Computer Science, vol 3861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11663881_11
Download citation
DOI: https://doi.org/10.1007/11663881_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31782-1
Online ISBN: 978-3-540-31784-5
eBook Packages: Computer ScienceComputer Science (R0)