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

Mostrar todas las versiones(2)

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.

Guardado en:
Detalles Bibliográficos
Autor principal: Saravia, Andrés Román
Otros Autores: Fervari, Raúl Alberto
Formato: publishedVersion bachelorThesis
Lenguaje:Español
Publicado: 2020
Materias:
Grafos
Modelos
Algoritmo
Tableaux
Theory of computation
Proof theory
Logic
Separation logic
Modal logic
Acceso en línea:http://hdl.handle.net/11086/15302
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-15302
record_format dspace
spelling I10-R141-11086-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/
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Español
topic Grafos
Modelos
Algoritmo
Tableaux
Theory of computation
Proof theory
Logic
Separation logic
Modal logic
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
topic_facet Grafos
Modelos
Algoritmo
Tableaux
Theory of computation
Proof theory
Logic
Separation logic
Modal logic
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.
author2 Fervari, Raúl Alberto
author_facet Fervari, Raúl Alberto
Saravia, Andrés Román
format publishedVersion
bachelorThesis
author Saravia, Andrés Román
author_sort Saravia, Andrés Román
title 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_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_sort cálculo de tableaux para fórmulas elementales en lógicas de separación
publishDate 2020
url http://hdl.handle.net/11086/15302
work_keys_str_mv AT saraviaandresroman calculodetableauxparaformulaselementalesenlogicasdeseparacion
_version_ 1806949078158802944

Ejemplares similares