Resumen de Métodos de tableaux para lógicas con declaraciones de términos dominios preordenados y operaciones monótonas
Pedro Jesús Martín de la Calle 
Las tesis presenta sistemas de tableaux para tres extensiones de la lógica de primer orden. En cada una de ellas se estudian métodos de tableaux correctos y completos en dos versiones: básica y de variables libre. La primera es una Lógica con Preórdenes y Géneros Dinámicos (LPGD); admite fórmulas que expresen relación de preorden entre términos y relación subtipo entre géneros. Las funciones y predicados son, en todos sus argumentos, monótonas o antimonótonas, y los tableaux actúan de forma que, en cada expansión de una rama por razón de anti-monotonía de alguna operación, se asegure que la fórmula introducida respeta la jerarquía de géneros contenida en la rama. La segunda es una Lógica con Declaraciones de Términos LDT que extiende LPGD permitiendo la declaración explícita de un término como perteneciente a un género dado, aunque no permite relación de preorden entre los datos. Para LDT se estudian y definen las sustituciones sobre tableaux con variables libres que conservan la corrección de la expansión de ramas, y se presenta un cálculo correcto, completo y termiante para resolver los problemas de unificación rígida ordenada que se dan en el cierre de tableaux. En la tercera es una Lógica con Preórdenes Monótonos LPM. Se trata de una lógica homogénea que admite relación de preorden entre datos, pero no jerarquías dinámicas entre género. LPM se estudia en dos fases; en la primera no se considera la monotonía en las operaciones y se obtiene un cálculo correcto, completo y terminante para la resolución de los problemas de unificación rígida preordenada que se presentan en el cierre de tableaux; este cálculo es mejorado con la introducción de órdenes de reducción. En la segunda fase se supone que las operaciones son monótonas en todos sus argumentos y se define un cálculo correcto y completo, pero no terminante, para la resolución de los respectivos problemas de unificación rígida preordenada monótona
