skip to main content
research-article

Open answer set programming with guarded programs

Published: 29 August 2008 Publication History

Abstract

Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program's constants. We define a fixed-point logic (FPL) extension of Clark's completion such that open answer sets correspond to models of FPL formulas and identify a syntactic subclass of programs, called (loosely) guarded programs. Whereas reasoning with general programs in OASP is undecidable, the FPL translation of (loosely) guarded programs falls in the decidable (loosely) guarded fixed-point logic (μ(L)GF). Moreover, we reduce normal closed ASP to loosely guarded OASP, enabling, for the first time, a characterization of an answer set semantics by μLGF formulas.
We further extend the open answer set semantics for programs with generalized literals. Such generalized programs (gPs) have interesting properties, for example, the ability to express infinity axioms. We restrict the syntax of gPs such that both rules and generalized literals are guarded. Via a translation to guarded fixed-point logic, we deduce 2-EXPTIME-completeness of satisfiability checking in such guarded gPs (GgPs). Bound GgPs are restricted GgPs with EXPTIME-complete satisfiability checking, but still sufficiently expressive to optimally simulate computation tree logic (CTL). We translate Datalog lite programs to GgPs, establishing equivalence of GgPs under an open answer set semantics, alternation-free μGF, and Datalog LITE.

References

[1]
Abiteboul, S., Hull, R., and Vianu, V. 1995. Foundations of Databases. Addison-Wesley, Reading, MA.
[2]
Andréka, H., Németi, I., and Van Benthem, J. 1998. Modal languages and bounded fragments of predicate logic. J. Philosoph. Log. 27, 3, 217--274.
[3]
Attie, P. C. and Emerson, E. A. 2001. Synthesis of concurrent programs for an atomic read/write model of computation. ACM Trans. Program. Lang. Syst. 23, 2, 187--242.
[4]
Balduccini, M. and Gelfond, M. 2003. Diagnostic reasoning with a-prolog. Theor. Pract. Log. Program. 3, 4-5, 425--461.
[5]
Baral, C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge, U.K.
[6]
Chandra, A. K. and Harel, D. 1982. Horn clauses and the fixpoint query hierarchy. In Proceedings of PODS '82. ACM Press, New York, NY, 158--163.
[7]
Clark, K. L. 1987. Negation as failure. In Readings in Nonmonotonic Reasoning. Morgan Kaufmann, San Francisco, CA, 311--325.
[8]
Clarke, E. M., Emerson, E. A., and Sistla, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2, 244--263.
[9]
Dantsin, E., Eiter, T., Gottlob, G., and Voronkov, A. 2001. Complexity and expressive power of logic programming. ACM Comput. Surv. 33, 3, 374--425.
[10]
Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Elsevier Science Publishers B.V., Amsterdam, The Netherlands, 995--1072.
[11]
Emerson, E. A. and Clarke, E. M. 1982. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 3, 241--266.
[12]
Emerson, E. A. and Halpern, J. Y. 1982. Decision procedures and Expressiveness in the temporal logic of branching time. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing. ACM Press, New York, NY, 169--180.
[13]
Flum, J. 1999. On the (infinite) model theory of fixed-point logics. Models, Algebras, and Proofs, X. Caceido and C. Montenegro, Eds. Marcel Dekker, New York, NY, 67--75.
[14]
Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proceedings of International Conference on Logic Programming (ICLP 1988). MIT Press, Cambridge, MA, 1070--1080.
[15]
Gelfond, M. and Przymusinska, H. 1993. Reasoning in open domains. In Logic Programming and Non-Monotonic Reasoning. MIT Press, Cambridge, MA, 397--413.
[16]
Gottlob, G., Grädel, E., and Veith, H. 2002. Datalog LITE: A deductive query language with linear time model checking. ACM Trans. Computat. Log. 3, 1, 1--35.
[17]
Grädel, E. 1999. On the restraining power of guards. J. Symbol. Log. 64, 4, 1719--1742.
[18]
Grädel, E. 2002a. Guarded fixed point logic and the monadic theory of trees. Theoret. Comput. Sci. 288, 129--152.
[19]
Grädel, E. 2002b. Model checking games. In Proceedings of WOLLIC 02. Electronic Notes in Theoretical Computer Science, vol. 67. Elsevier, Amsterdam, The Netherlands.
[20]
Grädel, E., Hirsch, C., and Otto, M. 2002b. Back and forth between guarded and modal logics. ACM Trans. Computat. Log. 3, 418--463.
[21]
Grädel, E. and Walukiewicz, I. 1999. Guarded fixed point logic. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS '99). IEEE Computer Society Press, Los Alamitos, CA, 45--54.
[22]
Halevy, A., Mumick, I., Sagiv, Y., and Shmueli, O. 2001. Static analysis in Datalog extensions. J. ACM 48, 5, 971--1012.
[23]
Halpin, T. 2001. Information Modeling and Relational Databases. Morgan Kaufmann, San Francisco, CA.
[24]
Heymans, S., Van Nieuwenborgh, D., and Vermeir, D. 2005a. Guarded open answer set programming. In 8th International Conference on Logic Programming and Non Monotonic Reasoning (LPNMR 2005), C. Baral, G. Greco, N. Leone, and G. Terracina, Eds. Lecture Notes in Artificial Intelligence, vol. 3662. Springer, Berlin, Germany, 92--104.
[25]
Heymans, S., Van Nieuwenborgh, D., and Vermeir, D. 2005b. Nonmonotonic ontological and rule-based reasoning with extended conceptual logic programs. In 2nd European Semantic Web Conference (ESWC 2005), A. Goméz-Pérez and J. Euzenat, Eds. Lecture Notes in Computer Science, vol. 3532. Springer, Berlin, Germany, 392--407.
[26]
Heymans, S., Van Nieuwenborgh, D., and Vermeir, D. 2006a. Guarded open answer set programming with generalized literals. In Fourth International Symposium on Foundations of Information and Knowledge Systems (FoIKS 2006), J. Dix and S. Hegner, Eds. Lecture Notes in Computer Science, vol. 3861. Springer, Berlin, Germany, 179--200.
[27]
Heymans, S., Van Nieuwenborgh, D., and Vermeir, D. 2006b. Open answer set programming for the semantic Web. J. Appl. Log. To appear. Also available online at http://tinf2.vub.ac.be/~sheymans/tech/hvnv-jal2006.pdf.
[28]
Huth, M. R. A. and Ryan, M. 2000. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge, U.K.
[29]
Immerman, N. 1986. Relational queries computable in polynomial time. Inform. Control 68, 1-3, 86--104.
[30]
Kozen, D. 1983. Results on the Propositional μ-calculus. Theoret. Comput. Sci. 27, 333--354.
[31]
Lee, J. and Lifschitz, V. 2003. Loop formulas for disjunctive logic programs. In Proceedings of ICLP 2003. Lecture Notes in Computer Science, vol. 2916. Springer, Berlin, Germany, 451--465.
[32]
Leone, N. and Perri, S. 2003. Parametric connectives in disjunctive logic programming. In Answer Set Programming. CEUR Workshop Proceedings, vol. 78. Available online at http://sunsite.informatile.rwth-aachen.de/Publications/CEUR-WS/.
[33]
Lifschitz, V., Pearce, D., and Valverde, A. 2001a. Strongly Equivalent Logic Programs. ACM Trans. Computat. Log. 2, 4, 526--541.
[34]
Lifschitz, V., Pearce, D., and Valverde, A. 2001b. Strongly equivalent logic programs. ACM Trans. Computat. Log. 2, 4, 526--541.
[35]
Lifschitz, V., Tang, L. R., and Turner, H. 1999. Nested expressions in logic programs. Ann. Math. Artific. Intell. 25, 3-4, 369--389.
[36]
Lin, F. and Zhao, Y. 2002. ASSAT: Computing answer sets of a logic program by SAT solvers. In Proceedings of the 18th National Conference on Artificial Intelligence. 112--117.
[37]
Lloyd, J. and Topor, R. 1984. Making Prolog more expressive. J. Log. Program. 1, 3, 225--240.
[38]
Manna, Z. and Wolper, P. 1984. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6, 1, 68--93.
[39]
Moschovakis, Y. 1974. Elementary Induction on Abstract Structures. North Holland, Amsterdam, The Netherlands.
[40]
Osorio, M., Navarro, J. A., and Arrazola, J. 2004. Applications of intuitionistic logic in answer set programming. Theor. Pract. Log. Program. 4, 3, 325--354.
[41]
Osorio, M. and Ortiz, M. 2004. Embedded implications and minimality in asp. In Proceedings of the 15th International Conference on Applications of Declarative Programming and Knowledge Management and 18th Workshop on Logic Programming. 241--254.
[42]
Papadimitriou, C. H. 1994. Computational Complexity. Addison Wesley, Reading, MA.
[43]
Schlipf, J. 1993. Some Remarks on Computability and Open Domain Semantics. In Proceedings of the Workshop on Structural Complexity and Recursion-Theoretic Methods in Logic Programming.
[44]
Schlipf, J. 1995. Complexity and undecidability results for logic programming. Ann. Math. Artific. Intell. 15, 3-4, 257--288.
[45]
Sistla, A. P. and Clarke, E. M. 1985. The complexity of propositional linear temporal logics. J. ACM 32, 3, 733--749.
[46]
Syrjänen, T. 2004. Cardinality constraint programs. In Proceedings of JELIA'04. Springer, Berlin, Germany, 187--200.
[47]
Tarski, A. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285--309.
[48]
Tobies, S. 2001. Complexity results and practical algorithms for logics in knowledge representation. Ph.D. dissertation, LuFG Theoretical Computer Science, RWTH-Aachen, Germany.
[49]
Van Benthem, J. 1997. Dynamic bits and pieces. In ILLC Research Report. University of Amsterdam, Amsterdam, The Netherlands.
[50]
van Emden, M. H. and Kowalski, R. A. 1976. The semantics of predicate logic as a programming language. J. ACM 23, 4, 733--742.

Cited By

View all
  • (2015)Reasoning with Forest Logic Programs Using Fully Enriched AutomataLogic Programming and Nonmonotonic Reasoning10.1007/978-3-319-23264-5_29(346-353)Online publication date: 15-Sep-2015
  • (2014)hex-Programs with Existential QuantificationDeclarative Programming and Knowledge Management10.1007/978-3-319-08909-6_7(99-117)Online publication date: 12-Jul-2014
  • (2012)Worst-case optimal reasoning with forest logic programsProceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning10.5555/3031843.3031920(608-612)Online publication date: 10-Jun-2012
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic
ACM Transactions on Computational Logic  Volume 9, Issue 4
August 2008
244 pages
ISSN:1529-3785
EISSN:1557-945X
DOI:10.1145/1380572
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 August 2008
Accepted: 01 September 2006
Received: 01 March 2006
Published in TOCL Volume 9, Issue 4

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Answer set programming
  2. fixed-point logic
  3. open domains

Qualifiers

  • Research-article
  • Research
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 16 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2015)Reasoning with Forest Logic Programs Using Fully Enriched AutomataLogic Programming and Nonmonotonic Reasoning10.1007/978-3-319-23264-5_29(346-353)Online publication date: 15-Sep-2015
  • (2014)hex-Programs with Existential QuantificationDeclarative Programming and Knowledge Management10.1007/978-3-319-08909-6_7(99-117)Online publication date: 12-Jul-2014
  • (2012)Worst-case optimal reasoning with forest logic programsProceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning10.5555/3031843.3031920(608-612)Online publication date: 10-Jun-2012
  • (2012)Synonymous theories and knowledge representations in answer set programmingJournal of Computer and System Sciences10.1016/j.jcss.2011.02.01378:1(86-104)Online publication date: 1-Jan-2012
  • (2011)Answer set programming's contributions to classical logicLogic programming, knowledge representation, and nonmonotonic reasoning10.5555/2001078.2001080(12-32)Online publication date: 1-Jan-2011
  • (2011)A hybrid system combining intuitionistic fuzzy description logics with intuitionistic fuzzy logic programs2011 Eighth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD)10.1109/FSKD.2011.6019517(60-64)Online publication date: Jul-2011
  • (2011)Reasoning with Forest Logic Programs and f-hybrid knowledge basesTheory and Practice of Logic Programming10.1017/S147106841100059713:03(395-463)Online publication date: 30-Dec-2011
  • (2011)Answer Set Programming’s Contributions to Classical LogicLogic Programming, Knowledge Representation, and Nonmonotonic Reasoning10.1007/978-3-642-20832-4_2(12-32)Online publication date: 2011
  • (2010)FO(ID) as an extension of DL with rulesAnnals of Mathematics and Artificial Intelligence10.5555/1873322.187334858:1-2(85-115)Online publication date: 1-Feb-2010
  • (2010)Tractable Reasoning with DL-Programs over Datalog-rewritable Description LogicsProceedings of the 2010 conference on ECAI 2010: 19th European Conference on Artificial Intelligence10.5555/1860967.1860976(35-40)Online publication date: 4-Aug-2010
  • Show More Cited By

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media