Tesis (Ciencias de la Computación e Inteligencia Artificial)
URI permanente para esta colecciónhttps://hdl.handle.net/11441/11305
Examinar
Examinando Tesis (Ciencias de la Computación e Inteligencia Artificial) por Fecha de publicación
Mostrando 1 - 20 de 35
- Resultados por página
- Opciones de ordenación
Tesis Doctoral Métodos algebraicos de razonamiento automático(1988) Alonso Jiménez, José Antonio; Riscos Fernández, Agustín; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialTesis Doctoral Bordismo seccional de fibrados y submersiones(1988-12-16) Arrabal Parrilla, Juan José; Domínguez Murillo, Eladio; Quintero Toscano, Antonio Rafael; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial; Universidad de Sevilla. SEJ189: Estud.estad.e Hist.series Temp.en Andalucia,XIX-XXEl objeto de este trabajo es sistematizar una técnica que intenta atacar el problema de existencia de secciones de funciones continuas o funciones diferenciables, y el problema de triangulación de una variedad topológica. El antecedente directo de esta técnica está en la teoría de homología seccional introducida por Weshu Shih, para el estudio de los sistemas de ecuaciones diferenciales no lineales. Dada una aplicación contínua f : X →B entre espacios topológicos X y B. Shih consideró el conjunto simplicial K(f) construido como sigue: Los q-símplices son las parejas (σ,γ), donde σ:Δq→B es una aplicación inyectiva continua del q-símplice estándar Δq=((Xo,X1,…,Xq)ЄRq+1|X1≥0, ΣXi=1> en B. y γ es uan función continua γ:Δq→X tal que σ=f•γ. Los operadores cara se definen de una manera natural. Cuando X, B son variedades diferenciales, f es un morfismo diferenciable y KЄZ+U(∞), se define el subconjunto simplicial K(f)k de K(f) formado por las (σ,γ) diferenciables de clase Ck, con σ inmersión difeomorfa (fr. “plongement”). Entonces definió el grupo de homología seccional con soportes propios de f. designado por H*(f)s, como el grupo de homología de las cadenas localmente finitas del conjunto simplicial K(f) con coeficientes enteros. De la misma manera definió los grupos seccionales H*(f)s,k. Considerando sólo las cadenas finitas en K(f) y K(F)k se obtienen los respectivos grupos de homología seccional con soportes compactos de f. el homomorfismo natural de la homología seccional de f:X→B en la homología singular de B con cadenas localmente finitas Pn:Hn(f)s→HIIn(B) le permitió definir el grado seccional de la función f, denotado deg(f), cuando B es una variedad orientada de dimensión n por la f´romula deg(f) = card (HIIn(B)/Im Pn>-1. En el caso en que X, B y f sean de clase C∞, se puede utilizar el grupo de homología seccional k-veces derivable Hn(f)s,ken lugar de Hn(f)s, y obtener el grado de k-veces derivable de f: degk(f). Estas nociones le permitieron probar que la anulación de deg(f) es necesaria para que f admita una sección continua y, en el caso diferenciable, que degk(f)=O es necesario para que f tenga una sección de clase Ck. Redefiniendo los grupos de homología con soportes compactos de f. Shih obtiene nuevos grados (ver el capítulo VIII de esta Tesis), que coinciden con los anteriores cuando la variedad V es compacta, y demuestra un teorema de caracterización del nuevo grado seccional continuo de f:Y→X, con la condición de que f sea un espacio fibrado localmente trivial cuya base X sea una variedad topológica conexa orientada de dimensión n y cuya fibra sea un CW-complejo finito conexo. Shih no presenta demostraciones ni propiedades de las homologías, ni indica la categoría explícitamente. Lo hace François Lalonde, quien ha dedicado su Tesis a estudiar sistemáticamente la homología seccional con soportes compactos. Ha demostrado que cumple los axiomas de Eilenberg-Steenrod, excepto el de escisión, en una categoría adecuada y que los grupos correspondientes no son invariantes de homotopía continua. Esto último es un inconveniente para el cálculo, pero es fundamental para poder aplicar esta teoría a los problemas de ecuaciones en derivadas parciales o integrales pues estos problemas no son invariantes por homotopía. La These d’Etat de Lalonde está dedicada a calcular la homología seccional diferenciable de clase CKde las funciones diferenciables f:X2→X1que localmente son de la forma RnxRm→Rn. estas funciones, que se llaman k-submersiones, engloban a los fibrados localmente triviales y a las submersiones en el sentido ordinario. El resultado que obtiene, para lo cual introduce nuevas teorías de homología que llama homología de p-campos transversos y homología de “plongements”, es el siguiente: TEOREMA S. Sea f:X2→X1 una k0-submersión (2≤k0≤∞). Cualquiera que sea 1≤k≤k0, el morfismo inyectivo P2:C(f)k→c(Xz) del grupo de cadenas seccionales finitas de clase Ck de f en el grupo de cadenas singulares finitas del espacio Xz, dado por la proyección (Δq,σ,γ)→(Δq,γ), índice un isomorfismos P2*sobre los grupos de homología en las dimensiones inferiores a n = dim Xz y un epimorfismos en dimensión n (los grupos de homología seccional de f son nulos en las dimensiones >n). Aquí vamos a presentar una teoría de homología más simple que las anteriores, que es una teoría de Eilenberg-Steenrod (es decir, que cumple escisión) y que la definición de grado coincide con las anteriores. El método adoptado consiste en construir una apropiada teoría de bordismo tomando como modelos las seudovariedades. Los ciclos geométricos asociados a una función continua f:Y→X son cuaternas (P, σ, γ, P) donde P es una seudovariedad, σ y γ son funciones continuas tales que σ=f•γ y P es un recubrimiento por subpoliedros compactos de P, de forma que σ es “casi inyectiva” en cada subpoliedro PiЄP. Decimos que una función σ:Pi→X definida en un poliedro Pi es “casi inyectiva” si existe un poliedro Q, un p.l. –epimorfismo π:Pi→Q y una función continua inyectiva υ:Q→X tales que σ = υ•π. El usar funciones “casi inyectivas” es para que sea posible la construcción “cilindro de un ciclo” que permite hacer bordante un ciclo a sí mismo (como se sabe, esto es esencial en toda teoría de bordismo). En nuestro caso el cilindro del ciclo (P, σ, γ; P) es (PxI, σ•pr1, γ•pr1; PxI), donde I es el intervalo cerrado [0.1], pr1 es la proyección canónica sobre el primer factor yPxI = {PixI | PiЄP}; es evidente que σ•pr1 no puede ser inyectiva, ni siquiera “inyectiva a trozos”. Una posible desventaja de este procedimiento de representar los ciclos seccionales frente a otros procedimientos que se imaginen, es que estamos obligados a estudiar si las funciones σ son o no inyectivas en cada PiЄP. La solución que tenemos es que en cada clase de seudobordismo hay al menos un ciclo (P, σ, γ;P) en el cual σ es inyectiva en cada PiЄP. Una característica positiva del bordismo aquí presentado es que hay una equivalencia natural con la homología de un apropiado complejo de cadenas que llamamos homología seccional casi-inyectiva, lo cual nos permite compararlo directamente con la homología singular y demostrar que el grado definido con nuestra homología coincide con el Shih. También se da el seudobordismo seccional diferenciable de clase Ck. Su estudio se basa en un caso particular, el seudobordismo de casi-inmersiones difeomorfas de clase Ck, de forma análoga a lo que ocurre con la homología seccional diferenciables y la homología de “plongements”, pero sin necesitar nada parecido a la homología de p-campos transversos, lo cual, junto al uso de las técnicas de aproximación de inmersiones difeormorfas diferenciales, produce una teoría mucho más sencilla que la dada por Lalonde. Los ciclos seccionales diferenciables de clase Ck (P, σ, γ; P)kasociados a una función f:Y→X de clase Ck son ciclos seccionales con funciones σ y γ continuas que cumplen ciertas condiciones de diferenciabilidad respecto a las variedades cX = X U∂x∂X*[0,1) y cY = Y U∂Y∂Y*[0,1), que se obtienen pegando a X y a Y sendos collares diferenciables. La razón de esto es haber observado que los simplices (Δn, σ, γ)k de la homología seccional diferencial de Shih son, por definición, tales que σ se prolonga a una inmersión difeomorfa s:U→X siendo U un entorno abierto de Δn en el espacio euclideo generado por Δn. por lo tanto, si dim X = n resulta que σΔn∩∂x = 0 γ, en consecuencia ninguna de las cadenas de dimensión igual a la de X que se forme con éstos símplices puede tener como borde una cadena cuyo soporte en X esté enteramente sobre ∂x, con lo cual no tiene sentido tratar con dicha homología seccional el problema de extender una sección definida en ∂x a todo X, ni tampoco tiene sentido tratar con ellas el problema de Dirichlet para una ecuación diferencial. Con dicha teoría de homología, los resultados que presentamos y consideramos más sobresalientes son: (1) Se da un tratamiento unificado de una teoría del grado de Shih utilizando, tanto en el caso compacto como en el no compacto, una teoría de bordimos seccional que es una teoría de homología ordinaria, en el sentido de Eilenberg-Steenrod, que permite un tratamiento más simple que en el realizado por Lalonde. (2) Demostrar que dichos grados nos permite: 2a) Caracterizar la variedades triangulables; 2b) Caracterizar la existencia de secciones de funciones continuas y de funciones diferenciables. Por otro lado, sobresale el haber extendido el “Teorema S” de LALONDE al caso de homología con soportes propios. Hay que observar que los cálculos con éstas homologías son difíciles, los cuales corresponde a la dificultad de los problemas que pretende tratar. Este trabajo, por tanto, no pretende más que sentar las bases de un nuevo método para el futuro estudio de dichos problemas. La memoria se presenta organizada en dos partes, cada una de las cuales consta a su vez de varios capítulos. La primera parte está dedicada a la homología seccional de funciones continuas y al grado continuo. En la segunda parte se trata el caso diferenciable, con especial énfasis en los fibrados localmente triviales y las submersiones. La extensión de algunos capítulos es reducida porque, para facilitar la lectura, se han suprimido las demostraciones que se pudieran obtener con fáciles pero laboriosas adaptaciones de demostraciones anteriores, y porque se ha querido facilitar la localización de los resultados, renunciado por ello a refundirlos con otros. A lo largo de esta memoria, y también en esta introducción, las referencias bibliográficas aparecen entre corchetes, mientras que las referencias internas a las definiciones, notas y resultados de este trabajo se hace colocando entre paréntesis las dos cifras con las cuales están ordenados lexicográficamente, la primera de las cuales india el capítulo en que está situado y la segunda el lugar dentro de él. Así, la cita “(2.4)” se refiere al ítem cuarto del capítulo segundo.Tesis Doctoral Estrategias de análisis gramatical y semántico para un sistema dirigido por voz(1999) López Soto, María Teresa; Amores Carredano, José Gabriel De; Quesada Moreno, José Francisco; Universidad de Sevilla. Departamento de Filología Inglesa (Lengua Inglesa); Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialEl objetivo de esta tesis es demostrar la eficiencia de un módulo del procesamiento de lenguaje natural (PLN) para un sistema telefónico que tiene como entrada expresiones de habla espontánea y que han sido reconocidas por un módulo de reconocimiento de voz (RV). La tesis describirá el sistema, así como las técnicas diseñadas para lograr extr aer el significado de las muestras de lenguaje hablado y espontáneo.Tesis Doctoral Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades(2001) Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialEl objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ello el sistema ACL2. Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos relacionados con la lógica ecuacional, y se llevan a cabo demostraciones automáticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificación formal se realiza en un entorno en el que se pueden combinar la demostración de teoremas con la ejecución de funciones.|Tesis Doctoral Verificación de programas en modelos de computación no convencionales(2002) Sancho Caparrini, Fernando; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialEl objetivo fundamental de esta memoria consiste en desarrollar una primer aproximación a la verificación formal de procedimientos mecánicos en modelos no convencionales, en el marco de la Computación Natural. Para ello, se han elegido dos modelos de computación que poseen características dispares. El primero de ellos, el modelos sticker, es un modelo de computación molecular que usa como sustrato físico el ADN y que se describe a través de un conjunto de operaciones básicas susceptibles de ser implementadas en el laboratorio con las técnicas actuales de biología molecular. Dichas operaciones, a modo de instrucciones de un lenguaje de programación, permiten que los procedimientos diseñados en el modelo adquieran la forma de programas. El segundo de los modelos elegidos es el denominado computación celular con membranas o P sistemas. En este modelo, los procedimientos se describen por medio de mecanismos o dispositivos similares a máquinas, de ejecución independiente.|Tesis Doctoral Operadores de generalización para el aprendizaje clausal(2002) Gutiérrez Naranjo, Miguel Ángel; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial"En esta memoria hemos estudiado los procesos de generalización, el paso de lo particular a lo general, cuando la información está expresada en lenguaje clausal. Para ello hemos definido unos operadores adaptados a los distintos órdenes de generalidad. Ha sido necesar ... io compaginar adecuadamente los distintos niveles en los que se produce la generalización: términos, literales, cláusulas y programas. La solución propuesta se apoya en la utilización de conjuntos de posiciones, conjuntos de literales y conjuntos de cláusulas, es decir, los operadores actúan sin necesidad de considerar órdenes sobre los literales de una cláusula o entre las cláusulas de un programa.Las principales aportaciones realizadas en esta memoria han sido:1.- La definición de una nueva familia de operadores, los Operadores Clausales, con la propiedad de ser operadores universales, esto es, que dadas dos cláusulas cualesquiera C1 y C2 podemos alcanzar C2 desde C1 mediante la sucesiva aplicación de estos operadores.2.- La definición de los Operadores de Aprendizaje para la Subsunción (OAS). Estos operadores son un subconjunto del conjunto de Operadores Clausales y su principal propiedad es que representan una caracterización mediante operadores de la relación de subsunción entre cláusulas, esto es, dadas dos cláusulas cualesquiera C1 y C2, se verifica que C1 subsume a C2 si y sólo si podemos obtener C1 a partir de C2 mediante la aplicación de una cadena de OAS.3.- La definición de una quasi-métrica sobre el conjunto de cláusulas que permite cuantificar la proximidad entre cláusulas basada en la relación de subsunción.4.- Un algoritmo para calcular dicha quasi-métrica.5.- Una fórmula para una rápida estimación de esta quasi-métrica que permite reducir costes computacionales.6.- La definición de operadores de generalización para el orden de derivación por resolución: Los Operadores de Inversión Sesgados (OIS). Una apropiada combinación de estos operadores junto con los Operadores de Aprendizaje para Subsunción nos permiten generalizar una cláusula D para obtener la cláusula C cuando C = D.7.- La definición de los Operadores de Generalización Minimales (OGM). Estos representan las unidades mínimas de generalización clausal de manera que si C y D son cláusulas y están relacionadas por alguna de las tres relaciones estudiadas: Subsunción, derivación o consecuencia, entonces podemos obtener C a partir de D mediante una combinación apropiada de OGM. 8.- La definición de operadores de generalización adaptados a la subsunción entre programas: los OAS compuestos. Estos operadores son extensiones a programas de los Operadores de Aprendizaje para la Subsunción (OAS) y de manera análoga a como ocurría con los OAS, también representan una caracterización de la relación de subsunción entre programas.9.- La definición de una métrica débil (una pseudo-quasi-distnacia) para cuantificar la proximidad entre programas basada en estos operadores.10.- Un método de cálculo de esta distancia débil.11.- La definición de un orden de aprendizaje entre programas definidos mediante sus menores modelos de Herbrand.12.- La relación entre el operador de consecuencia de Kowlski, el aprendizaje clausal, la relación de subsunción y los operadores que hemos definido para programas (OAS compuestos).13.- Diversos resultados relacionados con cadenas infinitas de cláusulas y programas.14. Una cota para el diámetro del conjunto de cláusulas por la relación de subsunción.Nuestro objetivo es profundizar en los procesos de generalización asociados a todo proceso de aprendizaje y en cómo podemos sistematizar ese paso de lo particular a lo general cuando el aprendizaje se realiza sobre lenguaje clausal.El objetivo de esta memoria es el estudio de los procesos de generalización, el paso de lo particular a lo general." -- Resumen del autorTesis Doctoral Teoría computacional (en ACL2) sobre cálculos proposicionales(2002) Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialEn este trabajo se desarrolla una formalización de sistemas de razonamiento proposicionales y se verifican automáticamente sus principales propiedades en el sistema de demostración automática ACL2.Tesis Doctoral Complejidad y universalidad en modelos de computación celular(2003) Romero Jiménez, Álvaro; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial"La Computación Celular es una disciplina que se enmarca dentro del campo de investigación conocido como Computación Natural. Tiene como objetivo fundamental el desarrollo de modelos de computación inspirados en los procesos que tienen lugar en el interioTesis Doctoral Extensiones de fragmentos de la Aritmética(2003) Cordón Franco, Andrés; Fernández Margarit, Alejandro; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialEl presente trabajo se enmarca dentro del campo de estudio de los Modelos de la Aritmética de Peano: PA. En líneas generales, se desarrolla un estudio sistemático de Fragmentos de la Aritmética empleando como metodología el análisis de la complejidad de ... (--) La complejidad sintáctica de sus axiomas.(--) La complejidad descriptiva, desde el punto de vista computacional, del conjunto de sus axiomas.En la primera parte del trabajo, refinamos propiedades conocidas sobre estructuras de elementos definibles, prestando especial atención a aquellos resultados que establecen que en dichas estructuras no son válidos esquemas de inducción o colección. Estos refinamientos son esenciales para obtener propiedades óptimas sobre existencia de extensiones de fragmentos de una cierta complejidad.En la parte central del trabajo, se obtienen resultados (en muchos casos óptimos) sobre la complejidad sintáctica y descriptiva de extensiones de fragmentos. Clásicos de la Aritmética (esto es, los obtenidos al restringir los principios de inducción, colección o minimización a fórmulas $\Sigma-n$ o $\Pi-n$).En la tercera parte del trabajo, se emplean los resultados sobre extensiones anteriores para estudiar Fragmentos Relativizados, es decir, los fragmentos de la Aritmética obtenidos al restringir los principios de inducción, colección, o minimización a fórmulas $\Delta-n(T)$ (esto es, fórmulas $\Sigma-n$ equivalentes a una fórmula $\Pi-n$ y tales que la teoría T demuestra dicha equivalencia). Dichos esquemas habían sido considerados previamente por Fernández Margarit y Lara Martín en relación al estudio del problema de Jeff Paris sobre la equivalencia de los fragmentos de inducción y minimización para fórmulas $\Delta-n$. El objetivo general del estudio de la Aritmética de Peano es obtener una mayor compresión de l|Tesis Doctoral Especificación y verificación de programas moleculares en PVS(2003-09-29) Graciani Díaz, Carmen; Pérez Jiménez, Mario de Jesús; Sancho Caparrini, Fernando; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialLa Computación Molecular y, en concreto, la Computación con ADN, es una disciplina que se enmarca dentro del campo de investigación conocido como Computación Natural. Tiene como objetivo el desarrollo de modelos de computación inspirados en el comportamiento de las moléculas de ADN, y en las posibilidades que abren las técnicas de laboratorio para su manipulación. En la memoria se han estudiado distintas adaptaciones del marco formal en que se describen distintos modelos de computación con ADN al lenguaje de especificaciones de PVS, que es un sistema de verificación cuyo lenguaje está basado en la lógica clásica de segundo orden con un sistema de tipos acorde con la teoría de conjuntos de Zermelo-Fraenkel con el axioma de elección. El demostrador del sistema está basado en cálculos de secuentes combinando la interacción con el usuario y el automatismo. Como aportaciones originales señalar la descripción en PVS del modelo restringido de Adleman y el modelo sticker, y la representación y verificación en PVS de programas moleculares que resuelven problemas clásicos NP-completos. En una primera aproximación al modelo sticker se ha realizado una implementación de la metodología presentada por Fernando Sancho en su tesis doctoral para la verificación de programas en el citado modelo. Así mismo, la consideración de los programas en este modelo como meros programas imperativos ha llevado a la descripción de la lógica de primer orden para dos tipos (indpendiente de la del sistema) y del cálculo de Floyd-Hoare, desarrollando un conjunto de estrategias que permiten simi-automatizar el proceso de verificación de programas imperativos. La presente memoria tiene dos objetivos fundamentales: por un lado estudiar la adaptación de nuevos modelos de computación no convencionales al marco formal de un sistema de verificación automática y, por otro, verificar la corrección y completitud de programas en dichos modelos utilizando para ello el demostrados del sistema. En esta memoria se presentan distintas aproximaciones a dos modelos de computación molecular basada en ADN y a la verificación de programas moleculares en los mismos que resuelven algunos problemas clásicos. El desarrollo de la misma está estructurada en capítulos que pasamos a reseñar sucintamente. En el Capítulo 1 se describen algunos paradigmas y modelos de Computación Natural como son las redes neuronales artificiales, los algoritmos genéticos, la programación evolutiva, la computación molecular, y la computación celular, como marco dentro del cual se describen los modelos de computación basados en AD, una de las áreas en la que se desarrolla presente memoria. En el Capítulo 2 se presenta una descripción básica del sistema PVS, con el fin de facilitar la lectura y compresión de los capítulos posteriores sin requerir un conocimiento mayor del mismo. Cada una de las secciones del capítulo se corresponde con uno de los elementos del lenguaje de especificaciones del sistema. Por último se incluye un breve ejemplo que ilustra el manejo del demostrador. El Capítulo 3 está dedicado a la computación molecular basada en ADN. Se incluye una descripción de la estructura química del ADN y su comportamiento, así como de algunas de las técnicas de laboratorio que se utilizan para su manipulación y que justifican la elección de las operaciones elementales de los modelos de computación molecular considerados. Por su importancia histórica se presenta al experimento de Adleman, considerando propiamente el origen de la Computación basada en ADN. Por último, se describen los modelos restringido de Adleman y sticker, objeto de estudio de la presente memoria. El primero como representante de los modelos sin memoria, ya que las operaciones moleculares consideradas no alteran la estructura de las moléculas de ADN. El segundo, como ejemplo de un modelo molecular con memoria, por el uso que hace de las moléculas de ADN como unidades de memoria que pueden ser modificadas a lo largo de la ejecución de un programa. En el Capítulo 4 se presentan, en primer lugar, dos problemas clásicos en teoría de la complejidad computacional, el problema SAT de la satisfactibilidad de la Lógica Proposicional y el problema de la 3 coloración de un grafo no dirigido. El trabajo de F. Martín y otros inspiró la posibilidad de utilizar un demostrador para la implementación y verificación de programas en modelos moleculares. Basado en dicho trabajo se realizó una primera aproximación en PVS basada en listas. A continuación se desarrolló una segunda implementación que utiliza como tipos de datos básicos los multiconjuntos y las sucesiones finitas de elementos, que permiten manejar de manera más natural las estructuras de datos del modelo. Dado que los dos problemas anteriores tienen en común que en el tubo inicial deben estar representadas todas las posibles funciones con dominio un conjunto finito de elementos y rango en un conjunto de valores, se especifica la construcción de un tubo inicial genérico. Por último, se incluye la verificación de programas moleculares diseñados para resolver los problemas citados. En el Capítulo 5 se estudia la implementación de una metodología diseñada por F. Sancho para la verificación de programas en el modelo sticker. Al considerar los programas como una sucesión de instrucciones básicas, éstos se consideran como la composición de funciones elementales. La única peculiaridad la proporcionan los bucles que son tratados como funciones recursivas dependientes de un valor para el caso base y una función que representa la sucesión de instrucciones que se repite a lo largo del bucle. Como ilustración se presente la verificación de una serie de programas moleculares diseñados para resolver problemas relativos a conjuntos numéricos y que son utilizados como subrutinas de programas que resuelven problemas clásicos NP-completos: el problema Subset-Sum, el problema de la Mochila 0/1 acotado, el problema del empaquetamiento, Set Packing¸ el del recubrimiento exacto, Exact Cover, y el problema del recubrimiento minimal. A continuación se puede decir que empieza una segunda parte en la memoria, en la que se consideran los programas en el modelo sticker como meros programas imperativos y, como tales, susceptibles de ser verificados con los métodos habituales utilizados para este tipo de programas, basados en las especificaciones de corrección parcial de Floyd-Hoare. Se considera que la ejecución de un programa imperativo produce un cambio de estado; es decir, un cambio en el valor de las variables asociadas al programa. Para poder expresar los programas y determinados asertos que permitan formular las condiciones de corrección de los mismos, Gloees represente en PVS la lógica clásica de Primer Orden y una técnica de verificación de programas imperativos basada en el cálculo de Hoare. En el capítulo 6 se presenta la lógica clásica y la lógica tipada de Primer Orden. A continuación se describe una implementación de la primera y el desarrollo, en PVS, de una lógica de primer orden para dos tipos, que nos permitirá escribir los programas de modelos sticker y demostrar la corrección de los mismos. En el Capítulo 7 se describe la implementación de las distintos comandos o instrucciones con los que se construyen los programas imperativos considerados: asignaciones, secuenciación y bucles para. Con cada una de las instrucciones consideradas se incluye el esquema o axioma correspondiente de la lógica de Floyd-Hoare que permite establecer la corrección de las mismas. Las operaciones del modelo se consideran como términos en las variables del programa. Para ilustrar el comportamiento de la misma se incluye la especificación de las subrutinas y del programa, presentadas en el capítulo 5, para resolver el problema del recubrimiento exacto en el modelo sticker, estableciendo su corrección. En el último capítulo de esta memoria se resumen algunas de las ideas acerca del desarrollo del trabajo, se presentan algunos datos que permiten cuantificar el mismo y se destaca algunas conclusiones extraídas de los resultados obtenidos. Se concluye con las perspectivas de trabajo futuro que se vislumbran tras los objetivos conseguidos en esta memoria y que marcan una línea de investigación en modelos de computación no convencionales.Tesis Doctoral Verificación formal en ACL2 del Algoritmo de Buchberger(2003-12-18) Medina Bulo, Inmaculada; Alonso Jiménez, José Antonio; Ruiz-Reina, José-Luis; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialEn este trabajo se han desarrollado los elementos necesarios para especificar, implementar y verificar la correción del algoritmo de Buchberger para el cálculo de bases de Gröbner, utilizando para ello un sistema de razonamiento automatizado (ACL2); esto incluye la formalización completa y precisa de toda la teoría matemática subyacente. Concretamente: -El desarrollo de una teoría computacional sobre los anillos de polinomios de múltiples variables. -La obtención de un orden natural a los polinomios de múltiples variables y demostración de su buena fundamentación. -La representación de los conceptos asociados a los ideales polinómicos de manera que sea posible razonar sobre ellos de manera automatizada. -El desarrollo de una teoría computacional sobre las reducciones polinómicas estableciendo su relación con las reduccines abstractas. -La representación de los conceptos asociados a las bases de Gröbner de manera que sea posible razonar sobre ellos de manera automatizada. -La implementación del algoritmo de Buchberger, especificar sus propiedades y demostrar su corrección. -La obtención de un procedimiento de decisión verificado para el problema de la pertenencia al ideal. Como se observa, nuestro énfasis se sitúa en la automatización del razonamiento. Dentro de los sistemas de razonamiento adecuados para este tipo de tareas hemos elegido a ACL2. Este sistema merece especial atención, ya que formaliza un subconjunto de COMMON LISP, un lenguaje de programación real. De hecho, LISP y sus dialectos se han usado tradicionalmente en la escritura de sistemas de Álgebra Computaciones. Por otro lado, ACL2 es especialmente bueno razonando por inducción. En este sentido, estamos ante un demostrados heurístico que incorpora no sólo potentes procedimientos de decisión, sino también estrategias sobre cómo abordar diferentes tipos de pruebas, cuándo expandir la definición de una función o generalizar un término, etc. La mayor parte de las ideas presentes en ACL2 provienen de un sistema anterior, NQTHM, también llamado el demostrador de teoremas de Boyer y Moore. ACL2 comienza a ser desarrollado en 1989 por Boyer, Moore y Kaufmann como una mejora sustancias de NQTHM, estando las últimas versiones desarrolladas fundamentalmente por los dos últimos autores. Hemos demostrado todos los teoremas (del orden de un millar) que aparecen durante la consecución de los objetivos mencionados en este sistema. Desde el punto de vista lógico, ACL2 es una lógica de primer orden con igualdad sin cuantificadores ni tipos y con funciones recursivas totales. La lógica incluye dos principios de extensión importantes, definición y encapsulado, y un principio de inducción que permite razonar sobre las funciones definidas por recursión. Como se observa, la lógica en sí es muy débil; en particular, la ausencia de cuantificadores supone una restricción importante de la lógica de primer orden. El hecho de que las funciones hayan de ser totales y la ausencia de tipos también tienen su impacto en la expresividad. Éste es el precio que hay que pagar por una mayor automatización: generalmente, nos concentramos en escribir las proposiciones y lemas intermedios que permiten al sistema demostrar un teorema complejo, proporcionándole de vez en cuando indicaciones cuando se desvía de nuestro plan preconcebido. Discutamos brevemente la importancia del algoritmo de Buchberger como justificación de su elección para nuestro trabajo. El gran desarrollo sufrido en la última década por el Álgebra Computacional ha dado como resultado la proliferación de numerosos sistemas de propósito general como MATHEMATICA. Éstos son la culminación de los resultados teóricos obtenidos en el último medio siglo, uno de cuyos descubrimientos centrales fue debido a B. Buchberger cuando en 1965 proporcionó un algoritmo para construir bases de Gröbner, que se emplean fundamentalmente para resolver el problema de la pertenencia en ideales polinómicos. h. Hironaka ya había demostrado poco antes la existencia de este tipo de bases, a las que llamó bases estándar, pero su demostración no era constructiva y no arrojaba ninguna luz sobre el problema de cómo calcularlas. El algoritmo de Buchberger, aunque al principio no tuvo demasiada difusión, causó finalmente un gran impacto en áreas muy diversas. Originalmente, se empleó para resolver problemas en Geometría Algebraica, pero ha sido aplicado con éxito en campos tan diversos como la Teoría de la Codificación, Estadística, Investigación Operativa y Teoría de Invariantes. También se ha empleado para automatizar el razonamiento en lógicas modales. Hoy día está implementado en la mayoría de los sistemas como MUPAD, MAPLE y MATHEMATICA, por citar sólo algunos. También existen unos pocos sistemas especialmente diseñados para proporcionar implementaciones particularmente eficientes del algoritmo de Buchberger como COCOA, SINGULAR, y MACAULAY. Es por esto que consideramos que disponer de implementaciones verificadas del algoritmo de Buchberger es importante. No obstante, esta tarea no resulta sencilla y lo primero que puede sorprendernos es la riqueza de estructuras algebraicas subyacentes a la propia definición del algoritmo de Buchberger y el esfuerzo que hay que dedicar a su formalización. Hay que emplear un cuerpo conmutativo de coeficientes para definir los monomios con los que construir polinomios de múltiples variables, los monomios deben poseer un orden admisible con el que inducir otro sobre los polinomios. Luego, hay que construir funciones de reducción apropiadas entre los polinomios. Para asegurar la corrección del algoritmo y proporcionar un procedimiento de decisión verificado para el problema de la pertenencia al ideal aumenta la variedad de estructuras implicadas y el esfuerzo necesario. En primer lugar, hay que definir el concepto de ideal polinómico finitamente generado y su congruencia inducida. Por otro lado, las funciones de reducción conviene estudiarlas en el marco, más general, de las relaciones de reducción abstractas. Sólo entonces, podemos obtener los resultados necesarios sobre las bases de Gröbner. Es en este esfuerzo adicional donde radica la diferencia entre programar el algoritmo y demostrar que es correcto.Tesis Doctoral Programación celular resolución eficiente de problemas numéricos NP-completos(2004) Riscos Núñez, Agustín; Pérez Jiménez, Mario de Jesús; Gutiérrez Naranjo, Miguel Ángel; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialEsta memoria está estructurada en capítulos cuyos contenidos pasamos a describir sucintamente. En el Capítulo 1 se hace una breve introducción histórica de la Teoría de la Computabilidad, analizándose las limitaciones y potencia de los modelos que formalizan el concepto de procedimiento mecánico, así como de la Teoría de la Complejidad Computacional, justificándose la necesidad de estudiar nuevos modelos de computación a fin de mejorar la resolución cuantitativa de problemas matemáticos especialmente difíciles, desde el punto de vista de esta teoría. También se describen brevemente nuevos modelos de computación inspirados en la forma en que la Naturaleza calcula. El Capítulo 2 está dedicado a la presentación del marco general en que se va a desarrollar esta memoria, la Computación celular con membranas. Concretamente se describen de manera informal los sistemas P de transición, que es el modelo considerado por Gh. Păun en el artículo fundacional de la disciplina. A continuación, se introducen los sistemas celulares reconocedores, que son dispositivos computacionales en el marco de la computación celular con membranas, especialmente adecuadas para reconocer lenguajes y, en consecuencia, para resolver problemas de decisión. Finalmente, se define una clase de complejidad polinomial que proporciona un concepto de resolubilidad eficiente de problemas a través de sistemas celulares reconocedores; es decir, un concepto de tratabilidad en este nuevo marco no convencional. Esta clase se sitúa por el momento a nivel teórico ya que, como hemos dicho, aún no existen implementaciones en soporte electrónico ni bioquímico. A menos que P = NP, para atacar de manera eficiente la resolubilidad de problemas NP-completos es necesario disponer de mecanismos que permitan fabricar una cantidad de espacio de tamaño exponencial en tiempo polinomial. Los sistemas celulares con membranas activas son una variante de modo de computación con membranas que satisface este requisito. En el Capítulo 3 se presenta una formalización de estos sistemas celulares que, en su versión de reconocedores, serán usados a lo largo de la memoria para resolver problemas NP-completos, de manera eficiente, en el marco de la clase de complejidad antes mencionada. En concreto, todas las computaciones de los sistemas diseñados paran y, además, lo hacen tras un número de pasos celulares de orden lineal. Los Capítulos 4, 5 y 6 están dedicados al estudio de soluciones eficientes de tres problemas numéricos NP-completos: Subset Sum, Knapsack y Partición, a través de sistemas celulares reconocedores con membranas activas. En todas las soluciones se sigue una misma estructura: - En primer lugar, se presentan los diseños de las correspondientes familias de sistemas celulares. - A continuación, se realiza una breve descripción intuitiva del funcionamiento de los mismos. - Finalmente, se demuestra la verificación formal de las soluciones, de acuerdo con la definición de clases de complejidad dada en el Capítulo 2. Además, al final del Capítulo 6 se incluyen una serie de comentarios en la línea de minimizar los recursos que emplean los sistemas utilizados. Se indica que es posible reducir en uno el número de cargas eléctricas distintas que se admiten. Más concretamente, en los sistemas P con membranas activas se considera que las membranas pueden tener carga positiva, negativa o neutra, pero se muestra que basta considerar solo dos cargas para poder obtener soluciones celulares eficientes. En las soluciones presentadas en los Capítulos 4, 5 y 6 de los problemas antes citados, se ha observado grandes similitudes entre los diferentes diseños. Ello, unido a las enormes dificultades que existen a la hora de diseñar dispositivos computacionales en los modelos de computación orientados a máquinas (como es el caso de los sistemas P), hace que adquiera especial relevancia la búsqueda de subrutinas que agrupen conjuntos de reglas de evolución de los sistemas, del tal manera que puedan ser utilizadas a modo de instrucciones de un lenguaje de programación celular. Este es el objetivo fundamental del Capítulo 7: la idea de un lenguaje de programación celular es factible, al menos para cierta clase relevante de problemas NP-completos, y podría ser de utilidad a la hora de diseñar y verificar soluciones para nuevos problemas en el futuro. En el Capítulo 8 se presenta un simulador de sistemas celulares, escrito en Prolog, que permite realizar simulaciones de las soluciones celulares presentadas en los capítulos anteriores. Se trata de una simulación secuencial, ya que en un ordenador convencional no se puede implementar la creación de un espacio de trabajo de tamaño exponencial en tiempo polinomial que llevan a cabo, a nivel teórico, los sistemas P con membranas activas. Conviene aclarar que el simulador no ha sido diseñado específicamente para las familias de sistemas P reconocedores presentadas en esta memoria, sino que ha sido para poder simular cualquier sistema P con membranas activas. A la hora de analizar soluciones de dispositivos computacionales en el marco de la complejidad computacional, se estudian, básicamente, los recursos en tiempo y/o en espacio utilizados. Pero estas medidas de complejidad pueden resultar claramente insuficientes cuando se trabaja con sistemas celulares con membranas activas que permiten la división de membranas en un paso de transición. En el Capítulo 9 se estudia la necesidad de profundizar en el estudio de nuevos parámetros que permitan analizar la complejidad de los sistemas P como dispositivos computacionales que resuelven problemas de decisión. Esos parámetros pueden orientar al usuario en la tarea de diseñar mejores sistemas que resuelven un mismo problema. La memoria concluye detallando algunas conclusiones que se pueden extraer de los resultados obtenidos, y se presentan una serie de objetivos y trabajos futuros que marcan nuevas líneas de investigación en modelos de computación no convencionales, algunas de las cuales han comenzado a desarrollarse en colaboración con algunos miembros del grupo de investigación en Computación Natural de la Universidad de Sevilla.Tesis Doctoral Evolution, communication, observation from biology to membrane computing and back(2005) Cavaliere, Matteo; Pérez Jiménez, Mario de Jesús; Paün, Gheorghe; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialLa Computación Natural es una disciplina cuyo objetivo fundamental es la simulación e implementación de procesos dinámicos que se dan en la Naturaleza y que son susceptibles de ser interpretados como procedimientos de cálculo. ... height: 150%; font-family: 'Times New Roman','serif'; font-size: 12pt">La simulación que aborda la Computación Natural puede tener diversas interpretaciones a la hora de describir los nuevos modelos: que se utilice para el diseño de nuevos esquemas algorítmicos usando técnicas inspiradas en la naturaleza, o bien que sugiera la creación física de nuevos modelos experimentales en los que el medio electrónico de los ordenadores convencionales se sustituya por otro sustrato que pueda implementar ciertos procesos que aparecen en el modelo de operar de la Naturaleza.Como ejemplo de la primera interpretación, podemos considera los Algoritmos Genéticos (o de manera más general, la computación evolutiva), que se basan en el proceso genético de los seres vivos a través del cual evoluciona y cuyo elemento fundamental es el principio de selección natural, y las redes neuronales artificiales que están inspiradas en la organización y funcionamiento del cerebro (siendo el origen de los autómatas finitos).Como ejemplo de la segunda interpretación, a finales de la década de los cincuenta el premio nobel R. P. Feynman postul la necesidad de considera operaciones sub-microscópicas como única alternativa revolucionaria en la carrera por la miniaturización de las componentes físicas de los ordenadores convencionales, y propone la computación a nivel molecular como posible modelo en el que implementar dichas operaciones. En 1987, T. Head propone explícitamente el primer modelo teórico basándose en las propiedades de las moléculas de ADN. En Noviembre de 1994, L. Adleman realiza el primer experimento en un laboratorio que permite resolver una instancia concreta de un problema NP-completo a través de la manipulación de moléculas de ADN.Un estudio más detallado del funcionamiento de los organismos vivos nos sugiere un nuevo nivel de computación: el nivel celular.El comportamiento de una célula puede ser considerado como el de una máquina no trivial, desde el punto de vista biológico, en la que por medio de una distribución jerárquica de membranas interiores se produce el flujo y alteración de las componentes químicas que la propia célula procesa. Esta memoria versa sobre el estudio de diversos aspectos teóricos de los sistemas celulares con membranas (que suelen denominarse sistemas P) y el análisis de sus posibles aplicaciones a la simulación y modelización de procesos biológicos. El objetivo fundamental de la Tesis es mostrar que los sistemas celulares pueden ser usados como un nuevo marco no convencional de modelización matemática de procesos biológicos, desde una óptica computacional, y que es posible manipular, modificar y adaptar dicho modelo matemático a través de ideas y sugerencia que parte de la Biología.La interacción entre Matemática y Biología proporciona una serie de posibilidades muy atractivas desde el punto de vista de la investigación científica: La elaboración de nuevos dispositivos matemático-computacionales que pueden ser usados para modelizar procesos biológicos y, a la vez, la formulación de problemas matemáticos relacionados con nuevos paradigmas de computación.Tesis Doctoral Razonamiento mereotopológico automatizado para la depuración de ontologías(2005) Chávez González, Antonia María; Borrego Díaz, Joaquín; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialLa presente memoria se estructura en tres grandes bloques: I Tratamiento automatizado de la teoría RCC y métodos asistidos por SRA para obtener extensiones de dicha teoría. Generalizaciones del retículo de relaciones asistido por SRA. Este bloque abarca los capítulos 2, 3 y 4. II Aplicación de RCC como cálculo meta-ontológico para su posterior uso en el análisis de anomalías en ontologías. Este tema se aborda en los capítulos 5 y 6.Tesis Doctoral Promoting and inhibiting contexts in membrane computing(2005-11-29) Sburlan, Dragos; Paun, Gheorghe; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialTesis Doctoral P systems, a computacional modelling framework for systems biology(2007) Romero Campero, Francisco José; Pérez Jiménez, Mario de Jesús; Gheorghe, Marian; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial"Los programas informáticos que modelizan células facilitarán el trabajo de los biólogos. Se basa en hacer modelos de células, por lo que llevo tres años en los que estoy realizando modelos de sistemas biológicos en bacterias. Una parte de programación la realizan ingenieros de software, pero yo monto el algoritmo o el modelo que simula el comp ... ortamiento de las bacterias y hago el proceso de validación de comparación con los datos del biólogo. El lenguaje que utilizan estos modelos de células está muy cerca del que emplean los biólogos y realizar experimentos con modelos de sistemas celulares desde un ordenador es relativamente fácil, en comparación con el esfuerzo de tiempo y dinero que supone elaborar las pruebas necesarias en un laboratorio hasta alcanzar resultados. Los biólogos no están acostumbrados a modelizar y es muy difícil obtener conocimientos del montón de datos que nos proporcionan. Así pues, nosotros intentamos simplificarlos y abstraerlos hasta conseguir un nuevo conocimiento. El modelo que diseñemos se tiene que comportar tal y como los biólogos indican, así ellos podrán trabajar desde un primer momento con nuestros programas para ver cómo funcionan los experimentos desde el ordenador. Una vez que ya lo hayan comprobado podrán saber si es rentable llevarlo al laboratorio."Tesis Doctoral Técnicas de depuración e integración de ontologías en el ámbito empresarial(2007) Paredes Moreno, Antonio; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Universidad de Sevilla. Departamento de Economía Financiera y Dirección de Operaciones; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialTesis Doctoral Membrane computing, neural inspirations, gene assembly in ciliates(2007-03-28) Ishdorj, Tseren-Onolt; Paun, Gheorghe; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialLa Tesis enmarca dentro de la disciplina de la computación celular con membranas, un modelo de computación orientado a máquinas, inspirado en la estructura y funcionamiento de las células de los organismos vivos, Que fue creada por G. Paun a finales de 1998 y que, en Octubre de 2003, el prestigioso institute for scientific information (I.S.I., USA) designó a dicha disciplina como fast emergin research front in computes science. La memoria aporta nuevas vías para atacar una serie de problemas clásicos relativos a la potencia y la eficiencia computacional de modelos de computación bio-inspirados y no convencionales, así como resultados relevantes en dichos modelos, conformando una memoria de gran valor científico que cumple, con creces, los requisitos para ser considerados como una tesis doctoral con acreditación de doctorado europeo.Tesis Doctoral P systems, a computational modelling framework for systems biology(2008-02-06) Romero Campero, Francisco José; Gheorghe, Marian; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialLOS PROGRAMAS INFORMÁTICOS QUE MODELIZAN CÉLULAS FACILITARÁN EL TRABAJO DE LOS BIÓLOGOS Se basa en hacer modelos de células, por lo que llevo tres años en los que estoy realizando modelos de sistemas biológicos en bacterias. Una parte de programación la realizan ingenieros de software, pero yo monto el algoritmo o el modelo que simula el comportamiento de las bacterias y hago el proceso de validac ión de comparación con los datos del biólogo. El lenguaje que utilizan estos modelos de células está muy cerca del que emplean los biólogos y realizar experimentos con modelos de sistemas celulares desde un ordenador es relativamente fácil, en comparación con el esfuerzo de tiempo y dinero que supone elaborar las pruebas necesarias en un laboratorio hasta alcanzar resultados. Los biólogos no están acostumbrados a modelizar y es muy difícil obtener conocimientos del montón de datos que nos proporcionan. Así pues, nosotros intentamos simplificarlos y abstraerlos hasta conseguir un nuevo conocimiento. El modelo que diseñemos se tiene que comportar tal y como los biólogos indican, así ellos podrán trabajar desde un primer momento con nuestros programas para ver cómo funcionan los experimentos desde el ordenador. Una vez que ya lo hayan comprobado podrán saber si es rentable llevarlo al laboratorio.Tesis Doctoral Desarrollo y aplicaciones de un entorno de programación para computación celular: P-Lingua(2010-06-24) Pérez Hurtado de Mendoza, Ignacio; Pérez Jiménez, Mario de Jesús; Riscos Núñez, Agustín; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia ArtificialLa presente memoria está estructurada en tres partes que constan de un total de siete capítulos cuyos contenidos se describen sucintamente a continuación. Parte I: Preliminares La memoria comienza con un breve recorrido histórico acerca del desarrollo y evolución de diversos conceptos relacionados con la Teoría de la Computación y la Teoría de la Complejidad Computacional. Se analizan las limitaciones que tienen los dispositivos reales construidos en el marco de dichas teorías, a la hora de resolver eficientemente problemas concretos que son relevantes en la vida real, lo cual hace necesario la búsqueda de nuevos paradigmas de computación que permitan superar algunas de esas limitaciones. Se presentan los conceptos básicos de la Computación Natural y, en particular, de la rama de la Computación celular con membranas, Membrane Computing, en la que se enmarcan los trabajos que se presentan en esta memoria. En el Capítulo 2 se analiza la problemática actual relativa a la modelización de procesos complejos de la realidad, justificando la necesidad de utilizar modelos formales a _n de conseguir ciertos avances de tipo cualitativo. Se describen brevemente algunas aproximaciones clásicas, así como otras más recientes de tipo computacional que tratan de capturar la aleatoriedad inherente a los procesos biológicos. Finalmente, se presenta un marco de especificación para el diseño de modelos basados en el paradigma de Membrane Computing. Parte II: Aplicaciones de software en Membrane Computing El Capítulo 3 está dedicado a justificar la necesidad de desarrollar herramientas informáticas para poder analizar la bondad de los modelos computacionales diseñados, a través de una validación experimental basada en simulaciones. Se presenta una breve panorámica de los simuladores de sistemas P desarrollados hasta la fecha y se describen los elementos comunes que tienen todos ellos y que han de ser implementados. En el Capítulo 4 se presenta un entorno de programación para el paradigma de Membrane Computing. Dicho entorno está compuesto de: (a) un lenguaje de programación para la especificación de sistemas P (P-Lingua); (b) una biblioteca que implementa el procesamiento de ficheros y diversos algoritmos de simulación (pLinguaCore); y (c) una serie de herramientas para la línea de comandos. La última parte está dedicada a la presentación de ejemplos de código de distintos sistemas P, incluyendo dos familias que proporcionan soluciones eficientes del problema SAT de la satisfactibilidad de la Lógica Proposicional. Parte III: Aplicación al estudio de ecosistemas reales En el Capítulo 5 se describe un marco específico para la modelización computacional de ecosistemas basado en Membrane Computing. En particular, se presentan las concreciones del marco general para los sistemas P probabilísticos y, además, se describe con detalle un algoritmo de simulación que trata de capturar la semántica probabilística. Además, se presenta el software EcoSim 2.0 que es una familia de herramientas para la simulación de modelos de ecosistemas y que se ha desarrollado utilizando P-Lingua y pLinguaCore. El capítulo finaliza con un ejemplo simple de ilustración acerca de las interacciones tritróficas. El Capítulo 6 está dedicado al diseño de modelos basados en sistemas P de dos ecosistemas reales. El primero de ellos se refiere a un ecosistema de la zona pirenaico-catalana en donde habita una ave carroñera en peligro de extinción, el quebrantahuesos; el segundo está dedicado a la modelización computacional de un ecosistema del pantano de Ribarroja, gestionado por Endesa S.A. en el que una especie exótica invasora (el mejillón cebra) está causando importantes problemas de sostenibilidad del medio ambiente con la destrucción de especies autóctonas, así como graves problemas de tipo económico al provocar importantes destrozos en instalaciones diversas de la compañía en torno a dicho pantano. En ambos casos, se han diseñado sendos modelos basados en sistemas P multientornos funcionales-probabilísticos para los cuales se han desarrollado aplicaciones informáticas ad hoc que permitan la validación experimental de los modelos y su uso para la realización de experimentos virtuales a partir de diferentes escenarios de interés para los expertos. La memoria finaliza con un breve capítulo dedicado a la presentación de conclusiones y líneas de trabajo futuro de investigación.