Cálculo de tableaux para fórmulas elementales en lógicas de separación
Tesis (Lic. en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2020.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | info:eu-repo/semantics/publishedVersion |
| Language: | spa |
| Published: |
2020
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/15302 |
| _version_ | 1801213983173115904 |
|---|---|
| author | Saravia, Andrés Román |
| author2 | Fervari, Raúl Alberto |
| author_facet | Fervari, Raúl Alberto Saravia, Andrés Román |
| author_sort | Saravia, Andrés Román |
| collection | Repositorio Digital Universitario |
| description | Tesis (Lic. en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2020. |
| format | info:eu-repo/semantics/publishedVersion |
| id | rdu-unc.15302 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2020 |
| record_format | dspace |
| spelling | rdu-unc.153022023-12-13T19:28:37Z Cálculo de tableaux para fórmulas elementales en lógicas de separación Saravia, Andrés Román Fervari, Raúl Alberto Grafos Modelos Algoritmo Tableaux Theory of computation Proof theory Logic Separation logic Modal logic Tesis (Lic. en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2020. info:eu-repo/semantics/publishedVersion Fil: Saravia, Andrés Román. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 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. info:eu-repo/semantics/publishedVersion Fil: Saravia, Andrés Román. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2020-06-02T15:00:36Z 2020-06-02T15:00:36Z 2020 bachelorThesis http://hdl.handle.net/11086/15302 spa Atribución-CompartirIgual 4.0 Internacional http://creativecommons.org/licenses/by-sa/4.0/ |
| spellingShingle | Grafos Modelos Algoritmo Tableaux Theory of computation Proof theory Logic Separation logic Modal logic Saravia, Andrés Román Cálculo de tableaux para fórmulas elementales en lógicas de separación |
| title | Cálculo de tableaux para fórmulas elementales en lógicas de separación |
| title_full | Cálculo de tableaux para fórmulas elementales en lógicas de separación |
| title_fullStr | Cálculo de tableaux para fórmulas elementales en lógicas de separación |
| title_full_unstemmed | Cálculo de tableaux para fórmulas elementales en lógicas de separación |
| title_short | Cálculo de tableaux para fórmulas elementales en lógicas de separación |
| title_sort | calculo de tableaux para formulas elementales en logicas de separacion |
| topic | Grafos Modelos Algoritmo Tableaux Theory of computation Proof theory Logic Separation logic Modal logic |
| url | http://hdl.handle.net/11086/15302 |
| work_keys_str_mv | AT saraviaandresroman calculodetableauxparaformulaselementalesenlogicasdeseparacion |