Medina Bulo, InmaculadaPalomo Lozano, FranciscoAlonso Jiménez, José AntonioRuiz Reina, José Luis2019-05-172019-05-172004Medina Bulo, I., Palomo Lozano, F., Alonso Jiménez, J.A. y Ruiz Reina, J.L. (2004). Verified Computer Algebra in ACL2 (Gröbner Bases Computation). En AISC 2004: 7th International Conference on Artificial Intelligence and Symbolic Computation (171-184), Linz, Austria: Springer.978-3-540-23212-40302-9743https://hdl.handle.net/11441/86466In this paper, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in the Acl2 system and shows how verified Computer Algebra can be achieved in an executable logic.application/pdfengAttribution-NonCommercial-NoDerivatives 4.0 Internacionalhttp://creativecommons.org/licenses/by-nc-nd/4.0/info:eu-repo/semantics/conferenceObjectinfo:eu-repo/semantics/openAccesshttps://doi.org/10.1007/978-3-540-30210-0_15