Tesis doctoral de Juan Luis Esteban Angeles
El capítulo 1 presenta la mayoría de los conceptos que se usarán más adelante. Comenzamos explicando el origen de la complejidad de la demostración. Luego definimos los sistemas de demostración y medidas de complejidad consideradas en esta obra. También reseñamos resultados de complejidad de la demostración y listamos nuestros propios resultados. el capítulo 2 trata de resultados acerca de tamaño para resolución, r(k), y planos secantes, que incluyen cotas de espacio inferiores y superiores que cuando están relacionadas proporcionan separaciones entre diferentes sistemas de demostración o entre las versiones en árbol y general de un mismo sistema de demostración. el capítulo 4 es corto y en él recapitulamos nuestros resultados y sugerimos problemas relacionados con nuestro trabajo que consideramos interesantes. También aparece una tabla de cotas inferiores y superiores de tamaño y espacio incluyendo nuestros resultados. Esta tabla facilita ver cuáles han sido nuestras contribuciones a la complejidad de la demostración. los resultados aparecieron en [begj]. En esta sección mejoramos la separación entre las versiones en árbol y generales de resolución y planos secantes. Para hacerlo, extendemos una cota inferior de tamaños para circuitos booleanos monótonos de ran y mckenzie a circuitos reales monótonos. Este tipo de separaciones resulta interesante puesto que muchos demostradores automáticos de teoremas se basan en la versión en árbol de sistemas de demostración, así la separación muestra que no siempre es una buena idea restringirse a la versión en árbol. Lo que hacemos es demostrar cotas inferiores exponenciales para planos secantes en árbol para ciertas fórmulas usando la propiedad de la interpolación monótona factible, que son a su vez cotas inferiores para la resolución en árbol. Para obtener la separación mostramos cotas superiores polinómicas en resolución para las mismas fórmulas, que son a su v
Datos académicos de la tesis doctoral «Complexity mesures for resolution«
- Título de la tesis: Complexity mesures for resolution
- Autor: Juan Luis Esteban Angeles
- Universidad: Politécnica de catalunya
- Fecha de lectura de la tesis: 15/12/2003
Dirección y tribunal
- Director de la tesis
- Bonet Carbonell M. Luisa
- Tribunal
- Presidente del tribunal: José Luis Balcazar navarro
- eli Ben-sasson (vocal)
- uwe Schí¶ning (vocal)
- victor Dalmau (vocal)