{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:21:12Z","timestamp":1759638072165,"version":"3.40.5"},"reference-count":28,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T00:00:00Z","timestamp":1600732800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2020,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called <jats:italic>flexible coinduction<\/jats:italic>, to express a variety of intermediate interpretations, necessary in some cases to get the correct meaning. We provide a detailed formal account of an extension of logic programming supporting flexible coinduction. Syntactically, programs are enriched by <jats:italic>coclauses<\/jats:italic>, clauses with a special meaning used to tune the interpretation of predicates. As usual, the declarative semantics can be expressed as a fixed point which, however, is not necessarily the least, nor the greatest one, but is determined by the coclauses. Correspondingly, the operational semantics is a combination of standard SLD resolution and coSLD resolution. We prove that the operational semantics is sound and complete with respect to declarative semantics restricted to finite comodels.<\/jats:p>","DOI":"10.1017\/s147106842000023x","type":"journal-article","created":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T02:43:15Z","timestamp":1600742595000},"page":"818-833","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":6,"title":["Flexible coinductive logic programming"],"prefix":"10.1017","volume":"20","author":[{"given":"FRANCESCO","family":"DAGNINO","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6297-2011","authenticated-orcid":false,"given":"DAVIDE","family":"ANCONA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ELENA","family":"ZUCCA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2020,9,22]]},"reference":[{"key":"S147106842000023X_ref21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundations of Logic Programming,","author":"Lloyd","year":"1987"},{"key":"S147106842000023X_ref15","volume-title":"Computer Science","volume":"6859","author":"Gupta","year":"2011"},{"key":"S147106842000023X_ref6","unstructured":"6. Ancona, D. , Dagnino, F. , and Zucca, E. 2017b. Generalizing inference systems by coaxioms. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, H. Yang, Ed. Notes, Lecture in Computer Science, vol. 10201. Springer, Berlin, 29\u201355."},{"key":"S147106842000023X_ref12","unstructured":"12. Dagnino, F. 2017. Generalizing inference systems by coaxioms. M.S. thesis, DIBRIS, University of Genova. Best italian master thesis in Theoretical Computer Science 2018."},{"key":"S147106842000023X_ref1","unstructured":"1. Aczel, P. 1977. An introduction to inductive definitions. In Handbook of Mathematical Logic, J. Barwise, Ed. Studies in Logic and the Foundations of Mathematics, vol. 90. Elsevier, 739\u2013782."},{"key":"S147106842000023X_ref14","unstructured":"14. Dagnino, F. 2020. Foundations of regular coinduction. Tech. rep., DIBRIS, University of Genova. May. Available at https:\/\/arxiv.org\/abs\/2006.02887. Submitted for journal publication."},{"key":"S147106842000023X_ref18","doi-asserted-by":"crossref","first-page":"906","DOI":"10.1017\/S147106841700028X","article-title":"Productive corecursion in logic programming","volume":"5","author":"Komendantskaya","year":"2017","journal-title":"Theory Pract. Log. Program. 17,"},{"key":"S147106842000023X_ref24","unstructured":"24. Moura, P. 2013. A portable and efficient implementation of coinductive logic programming. In Practical Aspects of Declarative Languages - 15th International Symposium, PADL 2013, Rome, Italy, January 21-22, 2013. Proceedings. 77\u201392."},{"key":"S147106842000023X_ref10","unstructured":"10. Basold, H. , Komendantskaya, E. , and Li, Y. 2019. Coinduction in uniform: Foundations for corecursive proof search with horn clauses. In ESOP 2019, L. Caires, Ed. Notes, Lecture in Computer Science, vol. 11423. Springer, 783\u2013813."},{"key":"S147106842000023X_ref3","first-page":"142","article-title":"Regular corecursion in prolog","volume":"4","author":"Ancona","year":"2013","journal-title":"Comput. Lang. Syst. Struct. 39,"},{"key":"S147106842000023X_ref13","first-page":"1","article-title":"Coaxioms: flexible coinductive definitions by inference systems","author":"Dagnino","year":"2019","journal-title":"Logical Methods in Computer Science 15"},{"key":"S147106842000023X_ref26","volume-title":"Computer Science","volume":"4596","author":"Simon","year":"2007"},{"key":"S147106842000023X_ref20","unstructured":"20. Li, Y. 2017. Structural resolution with coinductive loop detection. In Post-proceedings of CoALP-Ty\u201916, Komendantskaya, E. and Power, J. , Eds."},{"key":"S147106842000023X_ref19","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","article-title":"Coinductive big-step operational semantics","volume":"2","author":"Leroy","year":"2009","journal-title":"Information and Computation 207"},{"volume-title":"Prentice Hall International series in computer science","year":"1997","author":"Apt","key":"S147106842000023X_ref9"},{"key":"S147106842000023X_ref5","unstructured":"5. Ancona, D. , Dagnino, F. , and Zucca, E. 2017a. Extending coinductive logic programming with co-facts. In First Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty\u201916, Komendantskaya, E. and Power, J. , Eds. Electronic Proceedings in Theoretical Computer Science, vol. 258. Open Publishing Association, 1\u201318."},{"key":"S147106842000023X_ref28","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"2","author":"Tarski","year":"1955","journal-title":"Pacific Journal of Mathematics 5"},{"key":"S147106842000023X_ref11","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(83)90059-2","article-title":"Fundamental properties of infinite trees","author":"Courcelle","year":"1983","journal-title":"Theoretical Computer Science 25"},{"key":"S147106842000023X_ref4","doi-asserted-by":"crossref","first-page":"102492","DOI":"10.1016\/j.scico.2020.102492","article-title":"A big step from finite to infinite computations","author":"Ancona","year":"2020","journal-title":"Science of Computer Programming 197"},{"key":"S147106842000023X_ref8","doi-asserted-by":"crossref","first-page":"221","DOI":"10.3233\/FI-2015-1252","article-title":"A theoretical perspective of coinductive logic programming","volume":"3","author":"Ancona","year":"2015","journal-title":"Fundamenta Informaticae 140"},{"key":"S147106842000023X_ref25","unstructured":"25. Simon, L. 2006. Extending logic programming with coinduction. Ph.D. thesis, University of Texas at Dallas."},{"key":"S147106842000023X_ref23","unstructured":"23. Mantadelis, T. , Rocha, R. , and Moura, P. 2014. Tabling, rational terms, and coinduction finally together! TPLP 14, 4-5, 429\u2013443."},{"key":"S147106842000023X_ref27","unstructured":"27. Simon, L. , Mallya, A. , Bansal, A. , and Gupta, G. 2006. Coinductive logic programming. In Logic Programming, 22nd International Conference, ICLP 2006, Etalle, S. and Truszczynski, M. , Eds. Lecture Notes in Computer Science, vol. 4079. Springer, 330\u2013345."},{"key":"S147106842000023X_ref2","doi-asserted-by":"crossref","first-page":"1085","DOI":"10.1017\/S0960129506005706","article-title":"Iterative algebras at work","volume":"6","author":"Ad\u00e1mek","year":"2006","journal-title":"Mathematical Structures in Computer Scienc 16"},{"key":"S147106842000023X_ref17","doi-asserted-by":"crossref","unstructured":"17. Komendantskaya, E. et al. 2017. A productivity checker for logic programming. Post-proc. LOPSTR\u201916.","DOI":"10.1007\/978-3-319-63139-4_10"},{"key":"S147106842000023X_ref22","unstructured":"22. L\u00f6ding, C. and Tollk\u00f6tter, A. 2016. Transformation between regular expressions and omega-automata. In 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, Faliszewski, P. , Muscholl, A. , and Niedermeier, R. , Eds. LIPIcs, vol. 58. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 88:1\u201388:13."},{"key":"S147106842000023X_ref7","unstructured":"7. Ancona, D. , Dagnino, F. , and Zucca, E. 2018. Modeling infinite behaviour by corules. In 32nd European Conference on Object-Oriented Programming, ECOOP 2018, T. D. Millstein, Ed. LIPIcs, vol. 109. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl, 21:1\u201321:31."},{"key":"S147106842000023X_ref16","doi-asserted-by":"crossref","first-page":"745","DOI":"10.1093\/logcom\/exu026","article-title":"Coalgebraic logic programming: from semantics to implementation","volume":"2","author":"Komendantskaya","year":"2016","journal-title":"J. Logic and Computation 26"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S147106842000023X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,19]],"date-time":"2020-10-19T11:00:38Z","timestamp":1603105238000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S147106842000023X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,22]]},"references-count":28,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["S147106842000023X"],"URL":"https:\/\/doi.org\/10.1017\/s147106842000023x","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2020,9,22]]},"assertion":[{"value":"\u00a9 The Author(s), 2020. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}