{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:50:45Z","timestamp":1742914245482,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031617157"},{"type":"electronic","value":"9783031617164"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-61716-4_5","type":"book-chapter","created":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:47:52Z","timestamp":1716954472000},"page":"84-99","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Approximation Fixpoint Theory in\u00a0Coq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3460-4251","authenticated-orcid":false,"given":"Bart","family":"Bogaerts","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7866-7484","authenticated-orcid":false,"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,5,22]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-40564-8_11","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"C Antic","year":"2013","unstructured":"Antic, C., Eiter, T., Fink, M.: Hex semantics via approximation fixpoint theory. In: Cabalar, P., Son, T.C. (eds.) Logic Programming and Nonmonotonic Reasoning. Lecture Notes in Computer Science(), vol. 8148, pp. 102\u2013115. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-40564-8_11"},{"issue":"1","key":"5_CR2","first-page":"29","volume":"3","author":"B Barras","year":"2010","unstructured":"Barras, B.: Sets in Coq, Coq in sets. J. Formaliz. Reason 3(1), 29\u201348 (2010)","journal-title":"J. Formaliz. Reason"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer, Cham (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"4","key":"5_CR4","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21(4), 827\u2013859 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.artint.2017.11.003","volume":"255","author":"B Bogaerts","year":"2018","unstructured":"Bogaerts, B., Cruz-Filipe, L.: Fixpoint semantics for active integrity constraints. Artif. Intell. 255, 43\u201370 (2018). https:\/\/doi.org\/10.1016\/j.artint.2017.11.003","journal-title":"Artif. Intell."},{"issue":"1","key":"5_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3430750","volume":"22","author":"B Bogaerts","year":"2021","unstructured":"Bogaerts, B., Cruz-Filipe, L.: Stratification in approximation fixpoint theory and its application to active integrity constraints. ACM Trans. Comput. Log. 22(1), 1\u201319 (2021). https:\/\/doi.org\/10.1145\/3430750","journal-title":"ACM Trans. Comput. Log."},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Bogaerts, B., Cruz-Filipe, L.: A formalisation of approximation fixpoint theory in Coq (2024). https:\/\/doi.org\/10.5281\/zenodo.10709613","DOI":"10.5281\/zenodo.10709613"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Bogaerts, B., Jakubowski, M.: Fixpoint semantics for recursive SHACL. In: Formisano, A., et al. (eds.) Proceedings 37th International Conference on Logic Programming (Technical Communications), ICLP Technical Communications 2021, Porto (virtual event), 20-27th September 2021. EPTCS, vol.\u00a0345, pp. 41\u201347 (2021). https:\/\/doi.org\/10.4204\/EPTCS.345.14","DOI":"10.4204\/EPTCS.345.14"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.artint.2015.03.006","volume":"224","author":"B Bogaerts","year":"2015","unstructured":"Bogaerts, B., Vennekens, J., Denecker, M.: Grounded fixpoints and their applications in knowledge representation. Artif. Intell. 224, 51\u201371 (2015). https:\/\/doi.org\/10.1016\/j.artint.2015.03.006","journal-title":"Artif. Intell."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Bogaerts, B., Vennekens, J., Denecker, M.: Safe inductions and their applications in knowledge representation. Artif. Intell. 259, 167\u2013185 (2018). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S000437021830122X","DOI":"10.1016\/j.artint.2018.03.008"},{"issue":"3\u20134","key":"5_CR11","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1017\/S1471068418000108","volume":"18","author":"A Charalambidis","year":"2018","unstructured":"Charalambidis, A., Rondogiannis, P., Symeonidou, I.: Approximation fixpoint theory and the well-founded semantics of higher-order logic programs. Theory Pract. Log. Program. 18(3\u20134), 421\u2013437 (2018). https:\/\/doi.org\/10.1017\/S1471068418000108","journal-title":"Theory Pract. Log. Program."},{"key":"5_CR12","series-title":"The Springer International Series in Engineering and Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-1-4615-1567-8_6","volume-title":"Logic-Based Artificial Intelligence","author":"M Denecker","year":"2000","unstructured":"Denecker, M., Marek, V., Truszczy\u0144ski, M.: Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning. In: Minker, J. (ed.) Logic-Based Artificial Intelligence. The Springer International Series in Engineering and Computer Science, vol. 597, pp. 127\u2013144. Springer, Boston (2000). https:\/\/doi.org\/10.1007\/978-1-4615-1567-8_6"},{"issue":"1","key":"5_CR13","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/S0004-3702(02)00293-X","volume":"143","author":"M Denecker","year":"2003","unstructured":"Denecker, M., Marek, V., Truszczy\u0144ski, M.: Uniform semantic treatment of default and autoepistemic logics. Artif. Intell. 143(1), 79\u2013122 (2003). https:\/\/doi.org\/10.1016\/S0004-3702(02)00293-X","journal-title":"Artif. Intell."},{"key":"5_CR14","unstructured":"Denecker, M., Marek, V., Truszczy\u0144ski, M.: Reiter\u2019s default logic is a logic of autoepistemic reasoning and a good one, too. In: Brewka, G., Marek, V., Truszczy\u0144ski, M. (eds.) Nonmonotonic Reasoning \u2013 Essays Celebrating Its 30th Anniversary, pp. 111\u2013144. College Publications (2011). http:\/\/arxiv.org\/abs\/1108.3278"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-72200-7_9","volume-title":"LPNMR","author":"M Denecker","year":"2007","unstructured":"Denecker, M., Vennekens, J.: Well-founded semantics and the algebraic theory of non-monotone inductive definitions. In: Baral, C., Brewka, G., Schlipf, J.S. (eds.) LPNMR. Lecture Notes in Computer Science, vol. 4483, pp. 84\u201396. Springer, Cham (2007). https:\/\/doi.org\/10.1007\/978-3-540-72200-7_9"},{"issue":"1\u20132","key":"5_CR16","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0304-3975(00)00330-3","volume":"278","author":"M Fitting","year":"2002","unstructured":"Fitting, M.: Fixpoint semantics for logic programming \u2013 a survey. Theor. Comput. Sci. 278(1\u20132), 25\u201351 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(00)00330-3","journal-title":"Theor. Comput. Sci."},{"key":"5_CR17","unstructured":"Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K.A. (eds.) ICLP\/SLP, pp. 1070\u20131080. MIT Press, Cambridge (1988). http:\/\/citeseer.ist.psu.edu\/viewdoc\/summary?nodoi=10.1.1.24.6050"},{"key":"5_CR18","unstructured":"Grall, H.: Proving fixed points. Technical Report. HAL-00507775, HAL archives ouvertes (2010)"},{"key":"5_CR19","unstructured":"Grimm, J.: Implementation of three types of ordinals in Coq. Technical Report. RR-8407, INRIA (2013)"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Heyninck, J., Bogaerts, B.: Non-deterministic approximation operators: ultimate operators, semi-equilibrium semantics and aggregates (full version). CoRR abs\/2305.10846 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.10846","DOI":"10.48550\/arXiv.2305.10846"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"de\u00a0Jong, T., Kraus, N., Forsberg, F.N., Xu, C.: Set-theoretic and type-theoretic ordinals coincide. In: LICS, pp. 1\u201313 (2023).https:\/\/doi.org\/10.1109\/LICS56636.2023.10175762","DOI":"10.1109\/LICS56636.2023.10175762"},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0004-3702(88)90021-5","volume":"35","author":"K Konolige","year":"1988","unstructured":"Konolige, K.: On the relation between default and autoepistemic logic. Artif. Intell. 35(3), 343\u2013382 (1988). https:\/\/doi.org\/10.1016\/0004-3702(88)90021-5","journal-title":"Artif. Intell."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Kuratowski, C.: Une m\u00e9thode d\u2019\u00e9limination des nombres transfinis des raisonnements math\u00e9matiques. Fundamenta Mathematicae 3(1), 76\u2013108 (1922). http:\/\/eudml.org\/doc\/213282","DOI":"10.4064\/fm-3-1-76-108"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-319-34111-8_28","volume-title":"Advances in Artificial Intelligence","author":"F Liu","year":"2016","unstructured":"Liu, F., Bi, Y., Chowdhury, M.S., You, J., Feng, Z.: Flexible approximators for approximating fixpoint theory. In: Khoury, R., Drummond, C. (eds.) Advances in Artificial Intelligence. Lecture Notes in Computer Science(), vol. 9673, pp. 224\u2013236. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-34111-8_28"},{"key":"5_CR25","unstructured":"Blanqui, F.: https:\/\/github.com\/fblanqui\/color\/blob\/master\/Util\/Relation\/Tarski.v. Accessed 02 June 2021"},{"key":"5_CR26","unstructured":"Cast\u00e9ran, P.: https:\/\/github.com\/coq-community\/hydra-battles\/tree\/master\/theories\/ordinals. Accessed 02 June 2021"},{"issue":"1","key":"5_CR27","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0004-3702(85)90042-6","volume":"25","author":"RC Moore","year":"1985","unstructured":"Moore, R.C.: Semantical considerations on nonmonotonic logic. Artif. Intell. 25(1), 75\u201394 (1985). https:\/\/doi.org\/10.1016\/0004-3702(85)90042-6","journal-title":"Artif. Intell."},{"issue":"3","key":"5_CR28","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1017\/S1471068406002973","volume":"7","author":"N Pelov","year":"2007","unstructured":"Pelov, N., Denecker, M., Bruynooghe, M.: Well-founded and stable semantics of logic programs with aggregates. TPLP 7(3), 301\u2013353 (2007). https:\/\/doi.org\/10.1017\/S1471068406002973","journal-title":"TPLP"},{"issue":"1\u20132","key":"5_CR29","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/0004-3702(80)90014-4","volume":"13","author":"R Reiter","year":"1980","unstructured":"Reiter, R.: A logic for default reasoning. Artif. Intell. 13(1\u20132), 81\u2013132 (1980). https:\/\/doi.org\/10.1016\/0004-3702(80)90014-4","journal-title":"Artif. Intell."},{"key":"5_CR30","unstructured":"Simpson, C.: Set-theoretical mathematics in Coq. CoRR abs\/math\/0402336 (2004)"},{"key":"5_CR31","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.artint.2013.09.004","volume":"205","author":"H Strass","year":"2013","unstructured":"Strass, H.: Approximating operators and semantics for abstract dialectical frameworks. Artif. Intell. 205, 39\u201370 (2013). https:\/\/doi.org\/10.1016\/j.artint.2013.09.004","journal-title":"Artif. Intell."},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. (1955)","DOI":"10.2140\/pjm.1955.5.285"},{"issue":"3\u20134","key":"5_CR33","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10472-007-9049-2","volume":"48","author":"M Truszczy\u0144ski","year":"2006","unstructured":"Truszczy\u0144ski, M.: Strong and uniform equivalence of nonmonotonic theories - an algebraic approach. Ann. Math. Artif. Intell. 48(3\u20134), 245\u2013265 (2006). https:\/\/doi.org\/10.1007\/s10472-007-9049-2","journal-title":"Ann. Math. Artif. Intell."},{"issue":"4","key":"5_CR34","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/321978.321991","volume":"23","author":"MH van Emden","year":"1976","unstructured":"van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23(4), 733\u2013742 (1976). https:\/\/doi.org\/10.1145\/321978.321991","journal-title":"J. ACM"},{"issue":"3","key":"5_CR35","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1145\/116825.116838","volume":"38","author":"A Van Gelder","year":"1991","unstructured":"Van Gelder, A., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general logic programs. J. ACM 38(3), 620\u2013650 (1991). https:\/\/doi.org\/10.1145\/116825.116838","journal-title":"J. ACM"},{"key":"5_CR36","unstructured":"Van Hertum, P., Cramer, M., Bogaerts, B., Denecker, M.: Distributed autoepistemic logic and its application to access control. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pp. 1286\u20131292. IJCAI\/AAAI Press (2016). http:\/\/www.ijcai.org\/Abstract\/16\/186"},{"issue":"4","key":"5_CR37","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/1182613.1189735","volume":"7","author":"J Vennekens","year":"2006","unstructured":"Vennekens, J., Gilis, D., Denecker, M.: Splitting an operator: algebraic modularity results for logics with fixpoint semantics. ACM Trans. Comput. Log. 7(4), 765\u2013797 (2006). https:\/\/doi.org\/10.1145\/1182613.1189735","journal-title":"ACM Trans. Comput. Log."},{"issue":"1\u20132","key":"5_CR38","first-page":"187","volume":"79","author":"J Vennekens","year":"2007","unstructured":"Vennekens, J., Mari\u00ebn, M., Wittocx, J., Denecker, M.: Predicate introduction for logics with a fixpoint semantics. Parts I and II. Fund. Inform. 79(1\u20132), 187\u2013227 (2007)","journal-title":"Fund. Inform."}],"container-title":["Lecture Notes in Computer Science","Logics and Type Systems in Theory and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-61716-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:48:10Z","timestamp":1716954490000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-61716-4_5"}},"subtitle":["With an Application to Logic Programming"],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031617157","9783031617164"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-61716-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"22 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}