{"id":40125,"date":"1999-01-01T00:00:00","date_gmt":"1999-01-01T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/sistemas-de-tipos-puros-con-universos\/"},"modified":"1999-01-01T00:00:00","modified_gmt":"1999-01-01T00:00:00","slug":"sistemas-de-tipos-puros-con-universos","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/sistemas-de-tipos-puros-con-universos\/","title":{"rendered":"Sistemas de tipos puros con universos."},"content":{"rendered":"<h2>Tesis doctoral de <strong> Blas Carlos Ruiz Jimenez <\/strong><\/h2>\n<p>Los sistemas de tipo puros con universos propuestos en esta tesis permiten modelar de forma apropiada las teor\u00edas de tipos y los sistemas l\u00f3gicos m\u00e1s interesantes, y constituyen el n\u00facleo de la mayor\u00eda de los marcos l\u00f3gicos utilizados en la demostraci\u00f3n autom\u00e1tica de teoremas.  este trabajo propone tales teor\u00edas como generalizaci\u00f3n de otras teor\u00edas desarrolladas por un amplio n\u00famero de investigadores. proporciona un estudio general, del cual se pueden obtener propiedades cl\u00e1sicas de muchos sistemas. Desarrolla un original mecanismo algebraico, que es aplicado en la demostraci\u00f3n de algunas propiedades no triviales, como la propiedad de \u00abcondensaci\u00f3n\u00bb o la propiedad \u00abdecidibilidad del problema de la comprobaci\u00f3n de tipos\u00bb.  tales propiedades son caracterizadas a trav\u00e9s de un simple concepto de conservaci\u00f3n de la tipificaci\u00f3n bajo reducciones entre universos generalizados.  sugiere que las herramientas algebraicas desarrolladas son susceptibles de ser utilizadas para resolver otros problemas de la teor\u00eda de tipos hoy d\u00eda a\u00fan abiertos.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Sistemas de tipos puros con universos.<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Sistemas de tipos puros con universos. <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Blas Carlos Ruiz Jimenez <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 M\u00e1laga<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 01\/01\/1999<\/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>Jos\u00e9 Mar\u00eda Troya Linero<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Juan  jose Moreno navarro <\/li>\n<li>Antonio Gavilanes franco (vocal)<\/li>\n<li>inmaculada Perez de guzman molina (vocal)<\/li>\n<li>buenaventura Clares rodr\u00edguez (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Blas Carlos Ruiz Jimenez Los sistemas de tipo puros con universos propuestos en esta tesis permiten modelar [&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":[1890,2528,6474,3747,3748,7834,126,33898],"tags":[101834,78387,35611,24725,4814,16231],"class_list":["post-40125","post","type-post","status-publish","format-standard","hentry","category-ciencia-de-los-ordenadores","category-inteligencia-artificial","category-lenguajes-de-programacion","category-logica","category-logica-deductiva","category-malaga","category-matematicas","category-teoria-de-la-demostracion","tag-antonio-gavilanes-franco","tag-blas-carlos-ruiz-jimenez","tag-buenaventura-clares-rodriguez","tag-inmaculada-perez-de-guzman-molina","tag-jose-maria-troya-linero","tag-juan-jose-moreno-navarro"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/40125","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=40125"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/40125\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=40125"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=40125"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=40125"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}