{"id":3818,"date":"1994-01-01T00:00:00","date_gmt":"1994-01-01T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/1994\/01\/01\/automated-deduction-with-constrained-clauses\/"},"modified":"1994-01-01T00:00:00","modified_gmt":"1994-01-01T00:00:00","slug":"automated-deduction-with-constrained-clauses","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/automated-deduction-with-constrained-clauses\/","title":{"rendered":"Automated deduction with constrained clauses"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Albert Rubio Gimeno <\/strong><\/h2>\n<p>Esta tesis doctoral se centra en el estudio de mecanismos para realizar deduccion automatica en logica de primer orden con igualdad. La demostracion automatica de teoremas se esta aplicando actualmente en muchas areas de la informatica como son la ingenieria de software, las bases de datos o la inteligencia artificial.  los resultados de la tesis se pueden dividir en: los considerados basicos, como son en la definicion de ordenes sobre terminos (o expresiones) en la resolucion de restricciones simbolicas, cuya utilidad va mas alla de su aplicacion en este trabajo; y les resultados en deduccion automatica, que incluye resultados de completitud refutacional para procesos de deduccion mediante clausulas con restricciones de igualdad (tambien llamadas estrategias basicas) y de orden, considerando ademas el predicado de igualdad como predefinido y dando la posibilidad de trabajar modulo alguna teoria equacional.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Automated deduction with constrained clauses<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Automated deduction with constrained clauses <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Albert Rubio Gimeno <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Polit\u00e9cnica de catalunya<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 01\/01\/1994<\/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>Robert Nieu Wenhuis<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Fernando Orejas Vald\u00e9s <\/li>\n<li>Leo Bachimair (vocal)<\/li>\n<li>Mar\u00eda Alpuente Frasnedo (vocal)<\/li>\n<li>Pierre Jonannaud Jean (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Albert Rubio Gimeno Esta tesis doctoral se centra en el estudio de mecanismos para realizar deduccion automatica [&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,126,15596,15624],"tags":[15920,5512,15922,6479,15923,15921],"class_list":["post-3818","post","type-post","status-publish","format-standard","hentry","category-ciencia-de-los-ordenadores","category-inteligencia-artificial","category-matematicas","category-politecnica-de-catalunya","category-software","tag-albert-rubio-gimeno","tag-fernando-orejas-valdes","tag-leo-bachimair","tag-maria-alpuente-frasnedo","tag-pierre-jonannaud-jean","tag-robert-nieu-wenhuis"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/3818","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=3818"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/3818\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=3818"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=3818"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=3818"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}