zbMATH — the first resource for mathematics

On dual programs in co-logic programming. (English) Zbl 1362.68057
Falaschi, Moreno (ed.), Logic-based program synthesis and transformation. 25th international symposium, LOPSTR 2015, Siena, Italy, July 13–15, 2015. Revised selected papers. Cham: Springer (ISBN 978-3-319-27435-5/pbk; 978-3-319-27436-2/ebook). Lecture Notes in Computer Science 9527, 21-35 (2015).
Summary: 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.
For the entire collection see [Zbl 1326.68017].
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68N17 Logic programming
Smodels; SWI-Prolog
Full Text: DOI
[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) · Zbl 1090.68014 · doi:10.1017/S1471068403001960
[2] Ancona, D., Dovier, A.: co-LP: Back to the Roots. Theory and Practice of Logic Programming 13(4–5) (2013)
[3] Apt, K.R.: Introduction to logic programming. In: Handbook of Theoretical Computer Science, pp. 493–576. Elsevier (1990) · Zbl 0900.68136
[4] Aravindan, C., Dung, P.M.: Partial deduction of logic programs wrt well-founded semantics. New Gener. Comput. 13(1), 45–74 (1994) · doi:10.1007/BF03038308
[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) · Zbl 0945.03541
[6] Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
[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) · Zbl 1357.68031 · doi:10.1007/978-3-642-30743-0_13
[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) · Zbl 1021.68045 · doi:10.1007/3-540-36387-4_1
[9] Fitting, M.: Fixpoint semantics for logic programming a survey. Theoret. Comput. Sci. 278(1–2), 25–51 (2002) · Zbl 1002.68023 · doi:10.1016/S0304-3975(00)00330-3
[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)
[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) · Zbl 1213.68177 · doi:10.1007/978-3-540-74610-2_4
[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) · Zbl 1344.68053 · doi:10.1007/978-3-642-22944-2_4
[13] Jaffar, J., Stuckey, P.: Semantics of infinite tree logic programming. Theoret. Comput. Sci. 46, 141–158 (1986) · Zbl 0621.68054 · doi:10.1016/0304-3975(86)90027-7
[14] Kluzniak, F.: Meta-interpreter supporting tabling and coinduction (2009). http://www.utdallas.edu/gupta/meta.html
[15] Lloyd, J.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987). Extended edition · Zbl 0668.68004 · doi:10.1007/978-3-642-83189-8
[16] Marple, K., Bansal, A., Min, R., Gupta, G.: Goal-directed execution of answer set programs. In: PPDP 2012. pp. 35–44 (2012) · doi:10.1145/2370776.2370782
[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) · Zbl 1307.68020 · doi:10.1017/S1471068414000118
[18] Min, R.: Predicate Answer Set Programming with Coinduction. Ph.D. thesis, Universityof Texas at Dallas (2010)
[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) · doi:10.1007/3-540-63255-7_32
[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)
[21] Saptawijaya, A., Pereira, L.M.: Tabled abduction in logic programs. Theory Pract. Log. Program. 13, 4–5 (2013)
[22] Sato, T., Tamaki, H.: Transformational logic program synthesis. In: FGCS 1984 Tokyo, pp. 195–201 (1984)
[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) · Zbl 1377.68066 · doi:10.1007/978-3-642-32211-2_14
[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) · Zbl 1394.68057 · doi:10.1007/978-3-642-38197-3_14
[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) · Zbl 06514623 · doi:10.1007/978-3-319-14125-1_8
[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) · Zbl 1131.68400 · doi:10.1007/11799573_25
[27] Simon, L.E.: Extending Logic Programming with Coinduction. Ph.D. thesis. University of Texas at Dallas (2006)
[28] Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. Theory Pract. Log. Program. 12(1–2), 67–96 (2012) · Zbl 1244.68023 · doi:10.1017/S1471068411000494
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.