{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T11:12:16Z","timestamp":1742987536181,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_16","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"200-215","source":"Crossref","is-referenced-by-count":4,"title":["Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials"],"prefix":"10.1007","author":[{"given":"L.","family":"Lamb\u00e1n","sequence":"first","affiliation":[]},{"given":"F. J.","family":"Mart\u00edn-Mateos","sequence":"additional","affiliation":[]},{"given":"J.","family":"Rubio","sequence":"additional","affiliation":[]},{"given":"J. L.","family":"Ruiz-Reina","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","volume-title":"Triangulations. Structures for Algorithms and Applications","author":"J.A. Loera De","year":"2010","unstructured":"De Loera, J.A., Rambau, J., Santos, F.: Triangulations. Structures for Algorithms and Applications. Springer, Heidelberg (2010)"},{"key":"16_CR2","unstructured":"Dousson, X., Sergeraert, F., Siret, Y.: The Kenzo Program. Institut Fourier, Grenoble (1999), \n                    \n                      http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-20551-4_3","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J. Heras","year":"2011","unstructured":"Heras, J., Pascual, V., Rubio, J.: Proving with ACL2 the correctness of simplicial sets in the kenzo system. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol.\u00a06564, pp. 37\u201351. Springer, Heidelberg (2011)"},{"key":"16_CR4","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)"},{"key":"16_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-62029-4","volume-title":"Homology","author":"S. Mac Lane","year":"1963","unstructured":"Mac Lane, S.: Homology. Springer, Heidelberg (1963)"},{"key":"16_CR6","unstructured":"Mart\u00edn\u2013Mateos, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz\u2013Reina, J.L.: A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. In: Proceedings of the Third International ACL2 Workshop and its Applications, pp. 188\u2013201 (2002)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-642-02614-0_13","volume-title":"Intelligent Computer Mathematics","author":"F.J. Mart\u00edn-Mateos","year":"2009","unstructured":"Mart\u00edn-Mateos, F.J., Rubio, J., Ruiz-Reina, J.L.: ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol.\u00a05625, pp. 106\u2013121. Springer, Heidelberg (2009)"},{"key":"16_CR8","volume-title":"Simplicial objects in Algebraic Topology","author":"J.P. May","year":"1967","unstructured":"May, J.P.: Simplicial objects in Algebraic Topology. Van Nostrand, New York (1967)"},{"issue":"1","key":"16_CR9","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.jsc.2009.07.002","volume":"45","author":"I. Medina\u2013Bulo","year":"2010","unstructured":"Medina\u2013Bulo, I., Palomo\u2013Lozano, F., Ruiz\u2013Reina, J.L.: A verified Common Lisp implementation of Buchberger\u2019s algorithm in ACL2. Journal of Symbolic Computation\u00a045(1), 96\u2013123 (2010)","journal-title":"Journal of Symbolic Computation"},{"key":"16_CR10","first-page":"35","volume":"192","author":"J. Rubio","year":"1990","unstructured":"Rubio, J., Sergeraert, F.: Supports Acycliques and Algorithmique. Ast\u00e9risque\u00a0192, 35\u201355 (1990)","journal-title":"Ast\u00e9risque"},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1016\/S0007-4497(02)01119-3","volume":"126","author":"J. Rubio","year":"2002","unstructured":"Rubio, J., Sergeraert, F.: Constructive Algebraic Topology. Bulletin Sciences Math\u00e9matiques\u00a0126, 389\u2013412 (2002)","journal-title":"Bulletin Sciences Math\u00e9matiques"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T02:47:32Z","timestamp":1554000452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}