On Dual Programs in Co-Logic Programming

  • Hirohisa SekiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9527)


Co-logic programming is an extension of the conventional logic programming language, by allowing each predicate to be annotated as either inductive or coinductive. To define its procedural semantics as well as an alternating fixpoint semantics, the stratification restriction, a condition on predicate dependency in programs, has been imposed on co-logic programs (co-LPs). In this paper, we first consider dual programs in co-logic programming: Given a program P, its dual program \(P^{*}\) is a program such that it defines the “complement” of P, i.e., for any ground atom \(p(\overline{t})\), it computes its negation \(\lnot p(\overline{t})\). When we consider co-LPs with negation, we show that the stratification restriction becomes too restrictive in general, and that the Horn \(\mu \)-calculus by Charatonik et al. can be used as an extension of co-logic programming for handling “non-stratified” co-LPs. We then consider some applications of non-stratified co-LPs to Answer Set Programming (ASP) and the well-founded semantics (WFS). In particular, we give new iterated fixpoint characterizations of answer sets as well as the WFS via dual programs. We also discuss some applications of non-stratified co-LPs to program transformation such as partial deduction, and a proof procedure for the WFS.


Logic Programming Predicate Symbol Ground Atom Dual Program Proof Procedure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



The author would like to thank anonymous reviewers for their constructive and useful comments on the previous version of the paper. The idea of using co-LP techniques for a proof procedure for the WFS in Sect. 4 came from the discussions with Gopal Gupta at LOPSTR’13 in Madrid.


  1. 1.
    Alferes, J.J., Pereira, L.M., Swift, T.: Abduction in well-founded semantics and generalized stable models via tabled dual programs. Theor. Pract. Log. Program. 4, 383–428 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Ancona, D., Dovier, A.: co-LP: Back to the Roots. Theory and Practice of Logic Programming 13(4–5) (2013)Google Scholar
  3. 3.
    Apt, K.R.: Introduction to logic programming. In: Handbook of Theoretical Computer Science, pp. 493–576. Elsevier (1990)Google Scholar
  4. 4.
    Aravindan, C., Dung, P.M.: Partial deduction of logic programs wrt well-founded semantics. New Gener. Comput. 13(1), 45–74 (1994)CrossRefGoogle Scholar
  5. 5.
    Charatonik, W., McAllester, D., Niwinski, D., Podelski, A., Walukiewicz, I.: The Horn Mu–calculus. In: LICS 1998, pp. 58–69. IEEE Computer Society (1998)Google Scholar
  6. 6.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  7. 7.
    Denecker, M., Bruynooghe, M., Vennekens, J.: Approximation fixpoint theory and the semantics of logic and answers set programs. In: Erdem, E., Lee, J., Lierler, Y., Pearce, D. (eds.) Correct Reasoning. LNCS, vol. 7265, pp. 178–194. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  8. 8.
    Farwer, B.: \(\omega \)-Automata. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 3–21. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  9. 9.
    Fitting, M.: Fixpoint semantics for logic programming a survey. Theoret. Comput. Sci. 278(1–2), 25–51 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Proceedings of the Fifth International Conference and Symposium on Logic Programming, pp. 1070–1080. MIT Press (1988)Google Scholar
  11. 11.
    Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive logic programming and its applications. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 27–44. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  12. 12.
    Gupta, G., Saeedloei, N., DeVries, B., Min, R., Marple, K., Kluzniak, F.: Infinite computation, co-induction and computational logic. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 40–54. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  13. 13.
    Jaffar, J., Stuckey, P.: Semantics of infinite tree logic programming. Theoret. Comput. Sci. 46, 141–158 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Kluzniak, F.: Meta-interpreter supporting tabling and coinduction (2009).
  15. 15.
    Lloyd, J.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987). Extended edition CrossRefzbMATHGoogle Scholar
  16. 16.
    Marple, K., Bansal, A., Min, R., Gupta, G.: Goal-directed execution of answer set programs. In: PPDP 2012. pp. 35–44 (2012)Google Scholar
  17. 17.
    Marple, K., Bansal, A., Min, R., Gupta, G.: Dynamic consistency checking in goal-directed answer set programming. Theory Pract. Log. Program. 14(4–5), 415–427 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Min, R.: Predicate Answer Set Programming with Coinduction. Ph.D. thesis, Universityof Texas at Dallas (2010)Google Scholar
  19. 19.
    Niemelä, I., Simons, A.: Smodels — an implementation of the stable model and well-founded semantics for normal logic programs. In: Fuhrbach, U., Dix, J., Nerode, A. (eds.) LPNMR 1997. LNCS, vol. 1265, pp. 420–429. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  20. 20.
    Pereira, L.M., Saptawijaya, A.: Abductive logic programming with tabled abduction. In: Proceedings of the Seventh International Conference on Software Engineering Advances ICSEA 2012, pp. 548–556 (2012)Google Scholar
  21. 21.
    Saptawijaya, A., Pereira, L.M.: Tabled abduction in logic programs. Theory Pract. Log. Program. 13, 4–5 (2013)Google Scholar
  22. 22.
    Sato, T., Tamaki, H.: Transformational logic program synthesis. In: FGCS 1984 Tokyo, pp. 195–201 (1984)Google Scholar
  23. 23.
    Seki, H.: Proving properties of co-logic programs by unfold/fold transformations. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 205–220. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  24. 24.
    Seki, H.: Proving properties of co-logic programs with negation by program transformations. In: Albert, E. (ed.) LOPSTR 2012. LNCS, vol. 7844, pp. 213–227. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  25. 25.
    Seki, H.: Extending co-logic programs for branching-time model checking. In: Gupta, G., Peña, R. (eds.) LOPSTR 2013, LNCS 8901. LNCS, vol. 8901, pp. 127–144. Springer, Heidelberg (2014) Google Scholar
  26. 26.
    Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive logic programming. In: Etalle, S., Truszczynski, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 330–345. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  27. 27.
    Simon, L.E.: Extending Logic Programming with Coinduction. Ph.D. thesis. University of Texas at Dallas (2006)Google Scholar
  28. 28.
    Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. Theory Pract. Log. Program. 12(1–2), 67–96 (2012)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Department of Computer ScienceNagoya Institute of TechnologyNagoyaJapan

Personalised recommendations