ANALISIS COMBINATORIO

Autor: ELIZALDE TORRENT SERGI.
Año: 2003.
Universidad: POLITÉCNICA DE CATALUÑA [www.upc.edu].
Centro de lectura: SALA D'ACTES DE LA FME.
Centro de realización: U FACULTAT DE MATEMATIQUES I ESTADISTICA SUD.

Resumen: El tema d'aquesta tesi és l'enumeració de permutacions amb subseqüències prohibides respecte a certs estadístics, i l'enumeració de permutacions que eviten subseqüències generalitzades. Després d'introduir algunes definicions sobre subseqüències i estadístics en permutacions i camins de Dyck, comencem estudiant la distribució dels estadístics `nombre de punts fixos' i `nombre d'excedències' en permutacions que eviten una subseqüència de longitud 3. Un dels resultats principals és que la distribució conjunta d'aquest parell de paràmetres és la mateixa en permutacions que eviten 321 que en permutacions que eviten 132. Això generalitza un teorema recent de Robertson, Saracino i Zeilberger. Demostrem aquest resultat donant una bijecció que preserva els dos estadístics en qüestió i un altre paràmetre. La idea clau consisteix en introduir una nova classe d'estadístics en camins de Dyck, basada en el que anomenem túnel. A continuació considerem el mateix parell d'estadístics en permutacions que eviten simultàniament dues o més subseqüències de longitud 3. Resolem tots els casos donant les funcions generadores corresponents. Alguns casos són generalitzats a subseqüències de longitud arbitrària. També descrivim la distribució d'aquests paràmetres en involucions que eviten qualsevol subconjunt de subseqüències de longitud 3. La tècnica principal consisteix en fer servir bijeccions entre permutacions amb subseqüències prohibides i certs tipus de camins de Dyck, de manera que els estadístics en permutacions que considerem corresponen a estadístics en camins de Dyck que són més fàcils d'enumerar. Tot seguit presentem una nova família de bijeccions del conjunt de camins de Dyck a sí mateix, que envien estadístics que apareixen en l'estudi de permutacions amb subseqüències prohibides a estadístics clàssics en camins de Dyck, la distribució dels quals s'obté fàcilment. En particular, això ens dóna una prova bijectiva senzilla de l'equidistribució de punts fixos en les permutacions que eviten 321 i en les que eviten 132. A continuació donem noves interpretacions dels nombres de Catalan i dels nombres de Fine. Considerem una classe de permutacions definida en termes d'aparellaments de 2n punts en una circumferència sense creuaments. N'estudiem l'estructura i algunes propietats, i donem la distribució de diversos estadístics en aquests permutacions. En la següent part de la tesi introduïm una noció diferent de subseqüències prohibides, amb el requeriment que els elements que formen la subseqüència han d'aparèixer en posicions consecutives a la permutació. Més en general, estudiem la distribució del nombre d'ocurrències de subparaules (subseqüències consecutives) en permutacions. Resolem el problema en diversos casos segons la forma de la subparaula, obtenint-ne les funcions generadores exponencials bivariades corresponents com a solucions de certes equacions diferencials lineals. El mètode està basat en la representació de permutacions com a arbres binaris creixents i en mètodes simbòlics. La part final tracta de subseqüències generalitzades, que extenen tant la noció de subseqüències clàssiques com la de subparaules. Per algunes subseqüències obtenim nous resultats enumeratius. Finalment estudiem el comportament assimptòtic del nombre de permutacions de mida n que eviten una subseqüència generalitzada fixa quan n tendeix a infinit. També donem fites inferiors i superiors en el nombre de permutacions que eviten certes subseqüències.

Autor: HIDALGO DOBLADO MARIA JOSE.
Año: 2003.
Universidad: SEVILLA [www.us.es].
Centro de lectura: FACULTAD DE MATEMATICAS.
Centro de realización: FACULTAD DE MATEMATICAS.

Resumen: Los objetivos principales de la Tesis son la formalización de teorías matemáticas en sistemas de razonamiento automático, la verificación formal de algoritmos de dichas teorías y la realización de dicha verificación de forma que las pruebas en el sistema se correspondan esencialmente con las habituales. Para ello, hemos elegido un sistema de razonamiento, PVS, y dos teorías como objetos de formalización, la programación lógica preposicional y el análisis formal de conceptos. Por otra parte, el deseo de realizar un razonamiento natural sobre las especificaciones conduce al problema de la elección de los tipos básicos sobre los que construir las especificaciones. En este sentido, los tipos de datos elegidos para representar formalmente las nociones de las teorías han de estar los más próximo posible a dichas nociones. En ambos casos, el tipo más cercano al os objetos que se desea representar en el lenguaje de PVS es el tipo de los conjuntos finitos. Ahora bien, aunque la elección del tipo de los conjuntos de PVS como tipo base para realizar las especificaciones haga posible un razonamiento elegante sobre las mismas, se tiene el problema de que dichas especificaciones no son evaluables. La solución que proponemos para este problema es de carácter metodológico. Para ello hemos establecido en PVS un marco genérico en el que relacionar distintas especificaciones, definiendo formalmente cuándo dos especificaciones diferentes corresponden a un mismo concepto. En dicho marco, hemos estudiado las propiedades de carácter general que se conservan entre especificaciones de un mismo algoritmo. Esto nos ha permitido trabajar en dos planos. Por una parte, realizar el razonamiento en el plano en el que la distancia entre una noción y su especificación formal es mínima, aunque ésta no sea evaluable. Y por otra, sólo para determinadas especificaciones, obtener otras evaluables correspondientes al mismo concepto, y con las mismas propiedades (en particular, la propiedad de corrección de un algoritmo). En relación con las teorías consideradas: * Hemos realizado una formalización de la programación lógica preposicional, probando la equivalencia entre las distintas interpretaciones semánticas de los programas lógicos. Asimismo, hemos probado la completitud fuerte de la resolución SLD, usando una representación abstracta de los elementos que intervienen en el proceso de resolución. Finalmente, hemos construido refinamientos evaluables de los algoritmos de la programación lógica proporcional. * hemos formalizado la teoría del análisis formal de conceptos, de forma abstracta y hemos obtenido refinamientos evaluables de los algoritmos de dicha teoría.

Autor: GIMENEZ LLACH OMER.
Año: 2004.
Universidad: POLITÉCNICA DE CATALUÑA [www.upc.edu].
Centro de lectura: SALA D'ACTES FME.
Centro de realización: U FACULTAT DE MATEMATIQUES I ESTADISTICA SUD.

Autor: MOLINERO ALBAREDA XAVIER.
Año: 2005.
Universidad: POLITÉCNICA DE CATALUÑA [www.upc.edu].
Centro de lectura: SALA D'ACTES DE L'FME.
Centro de realización: U FACULTAT DE MATEMATIQUES I ESTADISTICA SUD.

Autor: BARAJAS TOMAS JAVIER.
Año: 2006.
Universidad: POLITÉCNICA DE CATALUÑA [www.upc.edu].
Centro de lectura: SALA D'ACTES FME.
Centro de realización: U FACULTAT DE MATEMATIQUES I ESTADISTICA SUD.