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

Abstract

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.

In this work we investigate computational reasoning methods for dynamic modal languages. By dynamic languages we mean formalisms that allow the underlying structure to change as a formula is being evaluated. In particular, we will study languages that combine operators from modal logic with operators from separation logic. The obtained family of logics is called modal separation logic (MSL). We will focus on developing a labeled tableaux calculus for a logic that combines the classic modal <> operator, the conjunction of separation * and the constant 'emp'. This fragment is denoted by MSL(<>,*). For this development, we will base ourselves on the so-called 'elementary formulas', a set of formulas that describe basic properties on the structure of the models. These formulas are easier to manipulate. Since the language of the elementary formulas is logically equivalent to the aforementioned fragment MSL(<>,*), the calculus obtained is also complete for this logic.