{"id":80810,"date":"1999-01-10T00:00:00","date_gmt":"1999-01-10T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/pragmatica-de-la-sintesis-de-programas-logicos\/"},"modified":"1999-01-10T00:00:00","modified_gmt":"1999-01-10T00:00:00","slug":"pragmatica-de-la-sintesis-de-programas-logicos","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/pragmatica-de-la-sintesis-de-programas-logicos\/","title":{"rendered":"Pragmatica de la sintesis de programas l\u00f3gicos"},"content":{"rendered":"<h2>Tesis doctoral de <strong> David Robert Son <\/strong><\/h2>\n<p>Esta tesis trata de nuevas formas de usar m\u00e9todos de s\u00edntesis estructural para especificaciones cl\u00e1usulas de horn ejecutables como programas l\u00f3gicos. estos m\u00e9todos son aplicables al dise\u00f1o y refinamiento iniciales de estas especificaciones, estadio considerado crucial para el uso de las especificaciones formales en aplicaciones pr\u00e1cticas.  dos m\u00e9todos de dise\u00f1o autom\u00e1tico son descritos. El primero es una forma distribuida de dise\u00f1o que utiliza un conjunto de herramientas independientes para construir las diferentes partes de una especificaci\u00f3n. Estas herramientas solamente comparten informaci\u00f3n de dise\u00f1o atrav\u00e9s del lenguaje com partido por todas ellas. La evaluci\u00f3n emp\u00edrica de este sistema revela un conjunto de dificultades nacidas de la insuficiente integraci\u00f3n entre las diferentes herramientas mencionadas y tambi\u00e9n la falta de un marco para el refinamiento incremental de especificaciones. El segundo sistema da respuesta a algunos de estos problemas proponiendo un sistema de refinamiento aplicable a problemas que pueden ser vistos como transformaciones sobre conjuntos de axiomas. en este sistema, todas las cl\u00e1usulas de horn expresan relaciones entre conjuntos de axionas (donde estos tambi\u00e9n son cl\u00e1usulas de horn). Esto permite que las especificaciones iniciales sean definifas restringiendo estos conjuntos. Inicialmente, estas especificaciones son refinadas por un sistema de reglas de reescritura aplicadas sobre desigualdades entre esos conjuntos. Inmediatamente despu\u00e9s las espcificaciones son detalladas progresivamente introduciendo esqueletos de definiciones espec\u00edficas de la tarea, que describen la manera de relacionar los elementos de los conjuntos de axiomas mencionados y tambi\u00e9n a\u00f1adiendo nuevos argumentos a los predicados que permitan llevar nueva informaci\u00f3n entre las especificaciones.  los m\u00e9todos descritos en la tesis son implementados por los sistemas lss y hansel. Estos han sido aplicados y comprob<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Pragmatica de la sintesis de programas l\u00f3gicos<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Pragmatica de la sintesis de programas l\u00f3gicos <\/li>\n<li><strong>Autor:<\/strong>\u00a0 David Robert Son <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Aut\u00f3noma de barcelona<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 01\/10\/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>Jaume Agust\u00ed Cullell<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Juan  jose Villanueva pipa\u00f3n <\/li>\n<li>Manuel Hermenegildo salinas (vocal)<\/li>\n<li>ram\u00f3n L\u00f3pez de m\u00e1ntaras bad\u00eda (vocal)<\/li>\n<li>norbert Fuchs (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de David Robert Son Esta tesis trata de nuevas formas de usar m\u00e9todos de s\u00edntesis estructural para especificaciones [&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,3747,3748,126,6566],"tags":[172801,6478,15895,4816,172802,14134],"class_list":["post-80810","post","type-post","status-publish","format-standard","hentry","category-ciencia-de-los-ordenadores","category-inteligencia-artificial","category-logica","category-logica-deductiva","category-matematicas","category-sistemas-formales","tag-david-robert-son","tag-jaume-agusti-cullell","tag-juan-jose-villanueva-pipaon","tag-manuel-hermenegildo-salinas","tag-norbert-fuchs","tag-ramon-lopez-de-mantaras-badia"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/80810","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=80810"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/80810\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=80810"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=80810"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=80810"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}