SISTEMAS FORMALES

Autor: SORIA DE DIEGO FERNANDO.
Año: 2003.
Universidad: PUBLICA DE NAVARRA.
Centro de lectura: E.T.S.I.A..
Centro de realización: UNIVERSIDAD PUBLICA DE NAVARRA.

Resumen: EN LA MEMORIA SE ESTUDIAN LAS DISTINTAS DEFINICIONES DE MEDIDAS DE INCLUSIÓN DIFUSAS, SE DAN NUEVAS DEFINICIONES DE ESTAS MEDIDAS Y SE PROPONE UNA CONSTRUCCIÓN A PARTIR DE OPERADORES DE AGREGACIÓN E IMPLICACIÓN. EN LOS TRES PRIMEROS CAPÍTULOS SE ESTUDIAN PROPIEDADES ESPECIALES DE LOS OPERADORES DE IMPLICACIÓN. EN EL CAPÍTULO CUATRO SE ANALIZAN PROPIEDADES DE LOS OPERADORES DE AGREGACIÓN. CON ESTAS AGREGACIONES E IMPLICACIONES, EN LOS TRES ÚLTIMOS CAPÍTULOS SE DEFINEN NUEVAS MEDIDAS DE INCLUSIÓN (MEDIDA DE INCLUSIÓN, INCLUSIÓN DÉBIL E INCLUSIÓN FUERTE) A PARTIR DE ESTAS MEDIDAS SE CONSTRUYEN OTROS ÍNDICES RELACIONADOS, COMO SON: ENTROPÍAS, DISTANCIAS, MEDIDAS DE SIMILARIDAD, DE PROXIMIDAD Y SOLAPAMIENTOS

Autor: ROBERT SON DAVID.
Año: 1999.
Universidad: AUTONOMA DE BARCELONA.
Centro de lectura: CIENCIAS.
Centro de realización: ESCUELA DE DOCTORADO Y FORMACIÓN CONTINUA.

Resumen: Esta tesis trata de nuevas formas de usar métodos de síntesis estructural para especificaciones Cláusulas de Horn ejecutables como programas lógicos. Estos métodos son aplicables al diseño y refinamiento iniciales de estas especificaciones, estadio considerado crucial para el uso de las especificaciones formales en aplicaciones prácticas. Dos métodos de diseño automático son descritos. El primero es una forma distribuida de diseño que utiliza un conjunto de herramientas independientes para construir las diferentes partes de una especificación. Estas herramientas solamente comparten información de diseño através del lenguaje com partido por todas ellas. La evalución empírica de este sistema revela un conjunto de dificultades nacidas de la insuficiente integración entre las diferentes herramientas mencionadas y también 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áusulas de Horn expresan relaciones entre conjuntos de axionas (donde estos también son Cláusulas 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és las espcificaciones son detalladas progresivamente introduciendo esqueletos de definiciones específicas de la tarea, que describen la manera de relacionar los elementos de los conjuntos de axiomas mencionados y también añadiendo nuevos argumentos a los predicados que permitan llevar nueva información entre las especificaciones. Los métodos descritos en la tesis son implementados por los sistemas LSS y HANSEL. Estos han sido aplicados y comprobados en tareas de especificaciones no triviales, incluyendo la reconstrucicón de una de las herramientas experimentales y el diseño de modelos similares a los construidos con el sistema KADS de ingeniería de conocimientos.

Autor: CASAMAYOR RODENAS JUAN CARLOS.
Año: 1996.
Universidad: POLITECNICA DE VALENCIA.
Centro de lectura: INFORMATICA .
Centro de realización: DEPARTAMENTO: SISTEMAS INFORMATICOS Y COMPUTACION PROGRAMA DE DOCTORADO: SISTEMAS INFORMATICOS Y COMPUTACION.

Resumen: EL TRABAJO INCLUIDO EN LA PRESENTE TESIS SE ENMARCA DENTRO DEL CAMPO DE LA DEMOSTRACION AUTOMATICA DE TEOREMAS Y CONSISTE EN EL ESTUDIO, DEFINICION Y DESARROLLO DE UN PARADIGMA DE RESOLUCION LINEAL, DENOMINADO RESOLUCION SL*: LA RAZON PARA UTILIZAR LA DENOMINACION DE PARADIGMA RESIDE EN EL HECHO DE QUE EN SI MISMA RESOLUCION SL* NO ES UN PROCEDIMIENTO, SINO QUE SE PUEDE ENTENDER COMO UNA FORMA DE RAZONAMIENTO CON CIERTOS PARAMETROS CUYA INSTANCIACION DA LUGAR A DIFERENTES PROCEDIMIENTOS QUE SON ADECUADOS AL TRATAMIENTO DE DISTINTOS TIPOS DE PROBLEMAS. POR OTRO LADO, SE LE HA DADO EL NOMBRE DE RESOLUCION SL* PORQUE, COMO POSTERIORMENTE SE EXPLICARA, ESTA MUY CERCANO A ELIMINACION DE MODELOS Y A RESOLUCION SL (DE AHI LA PRIMERA PARTE DEL NOMBRE). EL ASTERISCO FINAL QUIERE DENOTAR SU PARAMETRIZACION, DE FORMA QUE LOS PROCEDIMIENTOS INSTANCIAS DE RESOLUCION SL* SERAN DENOMINADOS CON UNA LETRA MAS EN VEZ DEL ASTERISCO, COMO POSTERIORMENTE SE VERA. EN RESOLUCION SL* SE INTRODUCE EL CONCEPTO FUNDAMENTAL DE "ELECCION DE ANCESTROS". LA ELECCION DE ANCESTROS ES EL MECANISMO QUE PERMITE CONTROLAR LA APLICACION DE LA RESOLUCION DE ANCESTRO HACIENDO POSIBLE UNA REDUCCION DEL COSTE DE SU PALICACION Y UNA ADECUACION DE RESOLUCION SL* AL TIPO DE PROBLEMAS A TRATAR. EL TRABAJO HACE ESPECIAL HINCAPIE EN LA IMPORTANCIA DE LA ELECCION DE ANCESTROS, YA QUE ES LA PRINCIPAL APORTACION DE RESOLUCION SL*, ANALIZANDO TANTO LAS VENTAJAS QUE APORTA ASOCIADAS AL INCREMENTO DE LA EFICIENCIA COMO EL HECHO DE DOTAR A RESOLUCION SL* LA CAPACIDAD DE ADAPTARSE A LOS PROBLEMAS QUE TRATA. TAMBIEN SE PRESENTA UNA IMPLEMENTACION DE RESOLUCION SL*, EN PARTICULAR DEL PROCEDIMIENTO SLT, Y SE INCLUYEN RESULTADOS SOBRE UN CONJUNTO EXTENSO DE PROBLEMAS DEL CAMPO DE LA DEMOSTRACION AUTOMATICA.

Autor: BUSTINCE SOLA NICANOR HUMBERTO.
Año: 1993.
Universidad: PUBLICA DE NAVARRA.
Centro de lectura: CIENCIAS.
Centro de realización: DEPARTAMENTO: MATEMATICA E INFORMATICA PROGRAMA DE DOCTORADO: MATEMATICA E INFORMATICA.

Resumen: LA MEMORIA ESTUDIA SISTEMATICAMENTE LOS CONJUNTOS INTUICIONISTAS DIFUSOS. ANALIZA LAS ESTRUCTURAS ALGEBRAICAS DE LOS CITADOS CONJUNTOS, DE LOS CONJUNTOS DIFUSOS INTERVALO-VALORADOS, DE LOS INTERVALO-VALORADOS INTUICIONISTAS DIFUSOS Y SUS RELACIONES MUTUAS. SE TRATAN LAS MEDIDAS NUMERICAS DE INFORMACION EN CONJUNTOS INTUICIONISTAS DIFUSOS. SE TRATAN METODOS DE OBTENCION DE SUBCONJUNTOS INTUICIONISTAS DIFUSOS A PARTIR DE SUBCONJUNTOS DIFUSOS. EN PARTICULAR SE PRESTA ATENCION A LAS RELACIONES INTUICIONISTAS EN LAS DIVERSAS CATEGORIAS MENCIONADAS Y A SUS PROPIEDADES DE COMPOSICION.