{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T16:54:22Z","timestamp":1725814462051},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319137698"},{"type":"electronic","value":"9783319137704"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-13770-4_1","type":"book-chapter","created":{"date-parts":[[2014,12,8]],"date-time":"2014-12-08T13:36:05Z","timestamp":1418045765000},"page":"1-6","source":"Crossref","is-referenced-by-count":0,"title":["Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems (Invited Talk)"],"prefix":"10.1007","author":[{"given":"Jos\u00e9\u2013Luis","family":"Ruiz\u2013Reina","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification Theory. In: Handbook of Automated Reasoning. Elsevier Science Publishers (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"1_CR3","unstructured":"Boyer, R., Moore, J S.: Single-Threaded objects in ACL2 (1999), http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/stobj\/main.pdf"},{"issue":"3-4","key":"1_CR4","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1016\/j.jsc.2005.09.007","volume":"41","author":"B. Buchberger","year":"2006","unstructured":"Buchberger, B.: Bruno Buchberger\u2019s PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Journal of Symbolic Computation\u00a041(3-4), 475\u2013511 (2006)","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR5","unstructured":"Dousson, X., Rubio, J., Sergeraert, F., Siret, Y.: The Kenzo Program, Institut Fourier (1999), http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Greve, D., Kaufmann, M., Manolios, P., Moore, J S., Ray, S., Ruiz-Reina, J.-L., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. Journal of Functional Programming\u00a01, 15\u201346 (2008)","DOI":"10.1017\/S0956796807006338"},{"key":"1_CR7","unstructured":"Kaufmann, M., Moore, J S.: ACL2 home page. University of Texas at Austin (2014), http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Moore, J S.: Structured Theory Development for a Mechanized Logic. Journal of Automated Reasoning 26(2), 161\u2013203 (2001)","DOI":"10.1023\/A:1026517200045"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10472-011-9274-6","volume":"64","author":"L. Lamb\u00e1n","year":"2012","unstructured":"Lamb\u00e1n, L., Mart\u00edn-Mateos, F.-J., Rubio, J., Ruiz-Reina, J.-L.: Formalization of a normalization theorem in simplicial topology. Annals of Mathematics and Artificial Intelligence\u00a064, 1\u201337 (2012)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1","key":"1_CR11","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1093\/jigpal\/jzt034","volume":"22","author":"L. Lamb\u00e1n","year":"2014","unstructured":"Lamb\u00e1n, L., Mart\u00edn-Mateos, F.-J., Rubio, J., Ruiz-Reina, J.-L.: Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm. Logic Journal of the IGPL\u00a022(1), 39\u201365 (2014)","journal-title":"Logic Journal of the IGPL"},{"key":"1_CR12","unstructured":"May, J.P.: Simplicial objects in Algebraic Topology. Van Nostrand (1967)"},{"issue":"1","key":"1_CR13","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"},{"issue":"3","key":"1_CR14","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1016003314081","volume":"36","author":"J.L. Ruiz-Reina","year":"2002","unstructured":"Ruiz-Reina, J.L., Alonso, J.A., Hidalgo, M.J., Mart\u00edn-Mateos, F.J.: Formal proofs about rewriting using ACL2. Ann. Math. and Artificial Intelligence\u00a036(3), 239\u2013262 (2002)","journal-title":"Ann. Math. and Artificial Intelligence"},{"issue":"1-2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10817-006-9030-5","volume":"37","author":"J.-L. Ruiz-Reina","year":"2006","unstructured":"Ruiz-Reina, J.-L., Alonso, J.-A., Hidalgo, M.-J., Mart\u00edn-Mateos, F.J.: Formal correctness of a quadratic unification algorithm. Journal of Automated Reasoning\u00a037(1-2), 67\u201392 (2006)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-13770-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,24]],"date-time":"2022-04-24T00:52:35Z","timestamp":1650761555000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-13770-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319137698","9783319137704"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-13770-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}