Cálculo de tableaux para fórmulas elementales en lógicas de separación

En este trabajo final investigamos métodos computacionales de razonamiento para lenguajes modales dinámicos. Por lenguajes dinámicos nos referimos a formalismos que permitan cambiar la estructura subyacente a medida que se evalúa una fórmula. En particular, estudiaremos lenguajes que combinan operadores de la lógica modal, con operadores dinámicos de las lógicas de separación llamados lógicas modales de separación (MSL). Nos centraremos en el desarrollo de un cálculo de tableaux etiquetado para una lógica que combina el operador modal <> clásico, la conjunción de separación * y la constante 'emp'. Para dicho desarrollo, nos basaremos en las llamadas 'fórmulas elementales', un conjunto de fórmulas que describen propiedades básicas sobre la estructura de los modelos, y que son más fáciles de manipular. Gracias a que el lenguaje de las fórmulas elementales es lógicamente equivalente a la MSL mencionada antes, el cálculo obtenido es también completo para esta lógica.