{"id":72421,"date":"2018-03-09T23:17:14","date_gmt":"2018-03-09T23:17:14","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/bases-de-ga%c2%b6bner-desarrollo-formal-en-coq\/"},"modified":"2018-03-09T23:17:14","modified_gmt":"2018-03-09T23:17:14","slug":"bases-de-ga%c2%b6bner-desarrollo-formal-en-coq","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/bases-de-ga%c2%b6bner-desarrollo-formal-en-coq\/","title":{"rendered":"Bases de g\u00c1\u00b6bner: desarrollo formal en coq"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Gilberto P\u00e9rez Vega <\/strong><\/h2>\n<p>En primer lugar, se aborda, de forma ajustada a lo que se va a necesitar, las nociones m\u00e1s pr\u00e1cticas del sistema coq que son necesarias para comprender la formalizaci\u00f3n de la teor\u00eda matem\u00e1tica de los polinomios, su reducci\u00f3n y bases de gr\u00ed\u00b6bner.  el trabajo espec\u00edfico comienza con la formalizaci\u00f3n de los t\u00e9rminos de \u00abn\u00bb variables, as\u00ed como las operaciones m\u00e1s usuales de polinomios en el sistema coq. Se implementa el orden lexicogr\u00e1fico profundizado en la prueba de que dicho orden es bien fundado.  para formalizar el anillo de polinomios en varias variables, se describen las pruebas de la estructura de cuerpo abstracto.  se implementan los polinomios y los polinomios can\u00f3nicos, formalizando una igualdad expl\u00edcita de polinomios original, describiendo tambi\u00e9n sus operaciones. Se implementa el orden de polinomios demostrando que es noetheriano.Asimismo, se implementa el concepto de ideal.  se generaliza, en el sistema de coq, el algoritmo de la divisi\u00f3n de polinomios en varias variables. Una vez implementada dicha divisi\u00f3n, llamada reducci\u00f3n; se estudia la relaci\u00f3n entre congruencia y reducci\u00f3n, obteni\u00e9ndose la forma normal m\u00f3dulo un conjunto de polinomios.  finalmente, se introduce el concepto de base de gr\u00ed\u00b6bner, estudiando y probando su equiValencia con otras caracterizaciones alternativas. Para resolver estas equiValencias se da una versi\u00f3n del lema de newman, implementando un esquema de recursi\u00f3n sobre polinomios can\u00f3nicos, as\u00ed como propiedades de la confluencia de la reducci\u00f3n.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Bases de g\u00c1\u00b6bner: desarrollo formal en coq<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Bases de g\u00c1\u00b6bner: desarrollo formal en coq <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Gilberto P\u00e9rez Vega <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 A coru\u00f1a<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 21\/01\/2005<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li> Barja P\u00e9rez Jos\u00e9 M\u00aa<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal:  Freire nistal Jos\u00e9 Luis <\/li>\n<li>Manuel Ojeda aciego (vocal)<\/li>\n<li>inmaculada Perez de guzman molina (vocal)<\/li>\n<li>felipe Gago couso (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Gilberto P\u00e9rez Vega En primer lugar, se aborda, de forma ajustada a lo que se va a [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[18576,2809,147772,3747,3748,16437,126,10522,33898,30772],"tags":[157504,38181,10525,157503,24725,74745],"class_list":["post-72421","post","type-post","status-publish","format-standard","hentry","category-a-coruna","category-algebra","category-intuicion","category-logica","category-logica-deductiva","category-logica-inductiva","category-matematicas","category-polinomios","category-teoria-de-la-demostracion","category-teoria-de-lenguajes-formales","tag-barja-perez-jose-ma","tag-felipe-gago-couso","tag-freire-nistal-jose-luis","tag-gilberto-perez-vega","tag-inmaculada-perez-de-guzman-molina","tag-manuel-ojeda-aciego"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/72421","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=72421"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/72421\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=72421"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=72421"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=72421"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}