A Theoretical Perspective of Coinductive Logic Programming

• Autorzy: Ancona D. , Dovier A.

Identyfikatory

DOI

10.3233/FI-2015-1252

• Konferencja: Italian Conference on Computational Logic, CILC 2013, (25-27.09.2013; Catania, Italy)
• Języki publikacji: EN

Abstrakty

EN

In this paper we study the semantics of Coinductive Logic Programming and clarify its intrinsic computational limits, which prevent, in particular, the definition of a complete, computable, operational semantics. We propose a new operational semantics that allows a simple correctness result and the definition of a simple meta-interpreter. We compare, and prove the equivalence, with the operational semantics defined and used in other papers on this topic.

Słowa kluczowe

EN

logic programming; denotational semantics; coinduction

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 140, nr 3/4
• Strony: 221--246
• Opis fizyczny: Bibliogr. 31 poz., rys.

Twórcy

autor

Ancona D.

• University of Genova DIBRIS, Via Dodecaneso 35, 16146 Genova, Italy

autor

Dovier A.

• University of Udine DIMI, Via delle Scienze 206, 33100 Udine, Italy

Bibliografia

• [1] Aczel, P.: Non-well-founded sets, CSLI Lecture Notes, 14, Stanford University, Center for the Study of Language and Information, 1988.
• [2] Ancona, D.: Regular corecursion in Prolog, Computer Languages, Systems & Structures, 39(4), 2013, 142–162.
• [3] Ancona, D., Corradi, A.: Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages, ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings, 2014.
• [4] Ancona, D., Corradi, A., Lagorio, G., Damiani, F.: Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?, FoVeOOS 2010 Revised Selected Papers (B. Beckert, C. March´e, Eds.), 6528, Springer, 2010.
• [5] Ancona, D., Lagorio, G.: Coinductive type systems for object-oriented languages, ECOOP 2009 - Object-Oriented Programming (S. Drossopoulou, Ed.), 5653, Springer, 2009.
• [6] Ancona, D., Lagorio, G.: Idealized coinductive type systems for imperative object-oriented programs, RAIRO - Theoretical Informatics and Applications, 45(1), 2011, 3–33.
• [7] Ancona, D., Lagorio, G.: Static single information form for abstract compilation, Theoretical Computer Science (IFIP TCS 2012) (J. C. Baeten, T. Ball, F. S. de Boer, Eds.), 7604, Springer, 2012.
• [8] Apt, K. R.: Introduction to Logic Programming, Technical Report TR-87-35, Department of Computer Sciences, The University of Texas at Austin, 1988.
• [9] Blair, H. A.: The Recursion-Theoretic Complexity of the Semantics of Predicate Logic as a Programming Language, 54, 1982.
• [10] Bonatti, P. A.: Resolution for Skeptical Stable Model Semantics, J. Autom. Reasoning, 27(4), 2001, 391–421.
• [11] Bonatti, P. A., Pontelli, E., Son, T. C.: Credulous Resolution for Answer Set Programming, AAAI (D. Fox, C. P. Gomes, Eds.), AAAI Press, 2008.
• [12] Colmerauer, A.: Equations and Inequations on Finite and Infinite Trees, FGCS, 1984.
• [13] Courcelle, B.: Fundamental Properties of Infinite Trees, Theor. Comput. Sci., 25, 1983, 95–169.
• [14] Dovier, A.: Set Graphs VI: Logic Programming and Bisimulation, Proceedings of the 29th Italian Conference on Computational Logic, Torino, Italy, June 16-18, 2014. (L. Giordano, V. Gliozzi, G. L. Pozzato, Eds.), 1195, CEUR-WS.org, 2014.
• [15] Dovier, A., Formisano, A., Pontelli, E.: Multivalued action languages with constraints in CLP(FD), TPLP, 10(2), 2010, 167–235.
• [16] Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence, Theor. Comput. Sci., 311(1-3), 2004, 221–256.
• [17] Gelfond, M., Lifschitz, V.: Action Languages, Electron. Trans. Artif. Intell., 2, 1998, 193–210.
• [18] Jaffar, J., Stuckey, P. J.: Semantics of Infinite Tree Logic Programming, Theoretical Computer Science, 46, 1986, 141–158.
• [19] Lloyd, J. W.: Foundations of Logic Programming, 2nd Edition, Springer, 1987.
• [20] Mantadelis, T., Rocha, R., Moura, P.: Tabling, Rational Terms, and Coinduction Finally Together!, TPLP, 14(4-5), 2014, 429–443.
• [21] Martelli, A., Montanari, U.: An Efficient Unification Algorithm, ACM Trans. Program. Lang. Syst., 4(2), 1982, 258–282.
• [22] Min, R., Bansal, A., Gupta, G.: Towards Predicate Answer Set Programming via Coinductive Logic Programming, AIAI (L. S. I. et al., Ed.), 296, Springer, 2009.
• [23] Min, R., Gupta, G.: Coinductive Logic Programming and its Application to Boolean SAT, FLAIRS Conference, 2009.
• [24] Moura, P.: A Portable and Efficient Implementation of Coinductive Logic Programming, Practical Aspects of Declarative Languages - 15th International Symposium, PADL 2013, Rome, Italy, January 21-22, 2013. Proceedings (K. F. Sagonas, Ed.), 7752, Springer, 2013, ISBN 978-3-642-45283-3.
• [25] Paige, R., Tarjan, R. E.: Three Partition Refinement Algorithms, SIAM J. Comput., 16(6), 1987, 973–989.
• [26] Rogers, Jr, H.: Theory of Recursive Functions and Effective Computability, The MIT Press, 1987.
• [27] Saeedloei, N., Gupta, G.: Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R), Proc. of LATA 2010, Lecture Notes in Computer Science, Springer, 2010.
• [28] Saeedloei, N., Gupta, G.: A logic-based modeling and verification of CPS, SIGBED Review, 8(2), 2011, 31–34.
• [29] Simon, L.: Extending logic programming with coinduction, Ph.D. Thesis, University of Texas at Dallas, 2006.
• [30] Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-Logic Programming: Extending Logic Programming with Coinduction, ICALP (L. Arge, C. Cachin, T. Jurdzinski, A. Tarlecki, Eds.), 4596, 2007.
• [31] Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive Logic Programming, Proc. of International Conference on Logic Programming (S. Etalle, M. Truszczynski, Eds.), 4079, Springer, 2006.