{"id":{"repo_id":"cadiz","oai_identifier":"oai:rodin.uca.es:10498/14705"},"canonical_url":"https://search.dev.ndltd.org/etd/cadiz/oai:rodin.uca.es:10498/14705","repository":{"repo_id":"cadiz","name":"Universidad de Cadiz","base_url":"https://rodin.uca.es/oai/request"},"display":{"title":"Verificación formal en ACL2 del algoritmo de Buchberger","abstract":"ACL2 is a computational logic, an automated reasoning system and an applicative programming language, a subset of COMMON LISP, based in pure lambda-calculus. It was developed in the University of Texas at Austin (USA) and is based in an untyped quantifier-free first-order logic of total recursive functions with equality. This thesis presents a computational theory about Buchberger's algorithm for Grobner bases computation in ACL2 in which: (1) Multivariate polynomial rings are formalized. This formalization is abstract: it encapsulates a coefficient ring which is used for the construction of polynomials and the verification of their properties. (2) These rings are equipped with an ordering relation induced by the terms (a lexicographical ordering on terms is defined). Its well-foundedness is proved and a polynomial embedding in epsilon0-ordinals is obtained. (3) An executable and verified ACL2 implementation of polynomials with rational coefficients, which is used for the construction of Buchberger's algorithm, is developed. (4) Polynomial ideals are formalized to state the ideal membership problem. The congruence induced by an ideal is defined and its fundamental properties are proved. (5) Reduction relations over polynomials are formalized in the framework of abstract reductions. It is proved that the equivalence relation equals to the congruence induced by the ideal and that the reduction is Noetherian with respect to the underlying polynomial ordering. Algorithms for the computation of normal forms are also presented and it is proved that ideals are closed under them. (6) S-polynomials are formalized and it is proved that the reduction relation induced by a set of polynomials is locally confluent (under certain conditions) and that it is possible to decide its equivalence closure by checking the equality of normal forms. (7) A fully-executable ACL2 implementation of Buchberger's algorithm compliant with the COMMON L ISP standard is built. Its termination and partial correctness are proved and a verified decision procedure for the ideal membership problem is supplied.","abstract_html":"ACL2 is a computational logic, an automated reasoning system and an applicative programming language, a subset of COMMON LISP, based in pure lambda-calculus. It was developed in the University of Texas at Austin (USA) and is based in an untyped quantifier-free first-order logic of total recursive functions with equality. This thesis presents a computational theory about Buchberger's algorithm for Grobner bases computation in ACL2 in which: (1) Multivariate polynomial rings are formalized. This formalization is abstract: it encapsulates a coefficient ring which is used for the construction of polynomials and the verification of their properties. (2) These rings are equipped with an ordering relation induced by the terms (a lexicographical ordering on terms is defined). Its well-foundedness is proved and a polynomial embedding in epsilon0-ordinals is obtained. (3) An executable and verified ACL2 implementation of polynomials with rational coefficients, which is used for the construction of Buchberger's algorithm, is developed. (4) Polynomial ideals are formalized to state the ideal membership problem. The congruence induced by an ideal is defined and its fundamental properties are proved. (5) Reduction relations over polynomials are formalized in the framework of abstract reductions. It is proved that the equivalence relation equals to the congruence induced by the ideal and that the reduction is Noetherian with respect to the underlying polynomial ordering. Algorithms for the computation of normal forms are also presented and it is proved that ideals are closed under them. (6) S-polynomials are formalized and it is proved that the reduction relation induced by a set of polynomials is locally confluent (under certain conditions) and that it is possible to decide its equivalence closure by checking the equality of normal forms. (7) A fully-executable ACL2 implementation of Buchberger's algorithm compliant with the COMMON L ISP standard is built. Its termination and partial correctness are proved and a verified decision procedure for the ideal membership problem is supplied.","abstract_has_math":false,"creators":["Medina Bulo, María Inmaculada"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Alonso Jiménez, José Antonio","Ruiz Reina, José Luis"],"committee_chairs":[],"committee_members":[],"year":2003,"date_issued":"2003-01-01T00:00:00Z","date_published":"2003-01-01T00:00:00Z","updated_at":"2026-07-24T01:29:34Z","subjects":["computer science","mathematics","ciencia de la computación","matemáticas","artificial intelligence","inteligencia artificial"],"languages":["spa"],"rights":["Attribution-NonCommercial-NoDerivs 3.0 Unported","info:eu-repo/semantics/openAccess"],"rights_urls":["http://creativecommons.org/licenses/by-nc-nd/3.0/"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10498/14705","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Alonso Jiménez, José Antonio","Ruiz Reina, José Luis"]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Lenguajes y Sistemas Informáticos"]},{"key":"dc:creator","label":"Author","values":["Medina Bulo, María Inmaculada"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2012-04-09T11:39:42Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2012-04-09T11:39:42Z"]},{"key":"dc:date.issued","label":"Date","values":["2003-01-01T00:00:00Z"]},{"key":"dc:type","label":"Dc Type","values":["doctoral thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["computer science","mathematics","ciencia de la computación","matemáticas","artificial intelligence","inteligencia artificial"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["spa"]},{"key":"dc:rights","label":"Dc Rights","values":["Attribution-NonCommercial-NoDerivs 3.0 Unported","info:eu-repo/semantics/openAccess"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://creativecommons.org/licenses/by-nc-nd/3.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10498/14705"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["ACL2 is a computational logic, an automated reasoning system and an applicative programming language, a subset of COMMON LISP, based in pure lambda-calculus. It was developed in the University of Texas at Austin (USA) and is based in an untyped quantifier-free first-order logic of total recursive functions with equality. This thesis presents a computational theory about Buchberger's algorithm for Grobner bases computation in ACL2 in which: (1) Multivariate polynomial rings are formalized. This formalization is abstract: it encapsulates a coefficient ring which is used for the construction of polynomials and the verification of their properties. (2) These rings are equipped with an ordering relation induced by the terms (a lexicographical ordering on terms is defined). Its well-foundedness is proved and a polynomial embedding in epsilon0-ordinals is obtained. (3) An executable and verified ACL2 implementation of polynomials with rational coefficients, which is used for the construction of Buchberger's algorithm, is developed. (4) Polynomial ideals are formalized to state the ideal membership problem. The congruence induced by an ideal is defined and its fundamental properties are proved. (5) Reduction relations over polynomials are formalized in the framework of abstract reductions. It is proved that the equivalence relation equals to the congruence induced by the ideal and that the reduction is Noetherian with respect to the underlying polynomial ordering. Algorithms for the computation of normal forms are also presented and it is proved that ideals are closed under them. (6) S-polynomials are formalized and it is proved that the reduction relation induced by a set of polynomials is locally confluent (under certain conditions) and that it is possible to decide its equivalence closure by checking the equality of normal forms. (7) A fully-executable ACL2 implementation of Buchberger's algorithm compliant with the COMMON L ISP standard is built. Its termination and partial correctness are proved and a verified decision procedure for the ideal membership problem is supplied."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:source","label":"Dc Source","values":["Dissertation Abstracts International, Volume: 65-05, Section: B, page: 2479"]},{"key":"dc:title","label":"Title","values":["Verificación formal en ACL2 del algoritmo de Buchberger"]}]}],"canonical_facts":{"dc:contributor.advisor":["Alonso Jiménez, José Antonio","Ruiz Reina, José Luis"],"dc:contributor.other":["Lenguajes y Sistemas Informáticos"],"dc:creator":["Medina Bulo, María Inmaculada"],"dc:date.accessioned":["2012-04-09T11:39:42Z"],"dc:date.available":["2012-04-09T11:39:42Z"],"dc:date.issued":["2003-01-01T00:00:00Z"],"dc:description.abstract":["ACL2 is a computational logic, an automated reasoning system and an applicative programming language, a subset of COMMON LISP, based in pure lambda-calculus. It was developed in the University of Texas at Austin (USA) and is based in an untyped quantifier-free first-order logic of total recursive functions with equality. This thesis presents a computational theory about Buchberger's algorithm for Grobner bases computation in ACL2 in which: (1) Multivariate polynomial rings are formalized. This formalization is abstract: it encapsulates a coefficient ring which is used for the construction of polynomials and the verification of their properties. (2) These rings are equipped with an ordering relation induced by the terms (a lexicographical ordering on terms is defined). Its well-foundedness is proved and a polynomial embedding in epsilon0-ordinals is obtained. (3) An executable and verified ACL2 implementation of polynomials with rational coefficients, which is used for the construction of Buchberger's algorithm, is developed. (4) Polynomial ideals are formalized to state the ideal membership problem. The congruence induced by an ideal is defined and its fundamental properties are proved. (5) Reduction relations over polynomials are formalized in the framework of abstract reductions. It is proved that the equivalence relation equals to the congruence induced by the ideal and that the reduction is Noetherian with respect to the underlying polynomial ordering. Algorithms for the computation of normal forms are also presented and it is proved that ideals are closed under them. (6) S-polynomials are formalized and it is proved that the reduction relation induced by a set of polynomials is locally confluent (under certain conditions) and that it is possible to decide its equivalence closure by checking the equality of normal forms. (7) A fully-executable ACL2 implementation of Buchberger's algorithm compliant with the COMMON L ISP standard is built. Its termination and partial correctness are proved and a verified decision procedure for the ideal membership problem is supplied."],"dc:format":["application/pdf"],"dc:identifier.uri":["http://hdl.handle.net/10498/14705"],"dc:language.iso":["spa"],"dc:rights":["Attribution-NonCommercial-NoDerivs 3.0 Unported","info:eu-repo/semantics/openAccess"],"dc:rights.uri":["http://creativecommons.org/licenses/by-nc-nd/3.0/"],"dc:source":["Dissertation Abstracts International, Volume: 65-05, Section: B, page: 2479"],"dc:subject":["computer science","mathematics","ciencia de la computación","matemáticas","artificial intelligence","inteligencia artificial"],"dc:title":["Verificación formal en ACL2 del algoritmo de Buchberger"],"dc:type":["doctoral thesis"]},"updated_at":"2026-07-24T01:29:34Z"}