Verificación de lógicas modales dinámicas en Coq

Mostrar todas las versiones(2)

Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019.

Guardado en:

Detalles Bibliográficos
Autor principal:	Trucco, Francisco Carlos
Otros Autores:	Fervari, Raúl Alberto
Formato:	bachelorThesis publishedVersion
Lenguaje:	Español
Publicado:	2020
Materias:	Verificación Formal Lógicas Modales Lógicas Dinámicas Asistente de Prueba Logic Logic and verification Modal and temporal logics (High Relevance) Theory of computation Formal Verification Coq
Acceso en línea:	http://hdl.handle.net/11086/14648
Aporte de:	Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba

id	I10-R141-11086-14648
record_format	dspace
spelling	I10-R141-11086-146482023-08-31T13:19:23Z Verificación de lógicas modales dinámicas en Coq Trucco, Francisco Carlos Fervari, Raúl Alberto Ziliani, Beta Verificación Formal Lógicas Modales Lógicas Dinámicas Asistente de Prueba Logic Logic and verification Modal and temporal logics (High Relevance) Theory of computation Formal Verification Coq Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019. Fil: Trucco, Francisco Carlos. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Los lenguajes modales son lenguajes adecuados para describir propiedades de grafos dirigidos con nodos etiquetados. Estas estructuras aparecen en una gran variedad de problemas de diversas áreas del conocimiento. Como consecuencia de esto, existe una gran variedad de lógicas modales. En la práctica cada vez que se define una nueva lógica modal, muchos teoremas deben ser demostrados y revisados nuevamente para esta nueva lógica. Este proceso, además de resultar tedioso, es propenso a errores. Afortunadamente, la tarea de realizar demostraciones complejas ha comenzado cada vez más a ser asistida por herramientas computacionales. En este trabajo, formalizamos y verificamos en el asistente de demostraciones Coq un teorema de invarianza bajo bisimulación de ciertas lógicas modales con operadores dinámicos capaces de modificar la relación de accesibilidad. Modal languages are adequate languages to describe properties of labelled directed graphs. These structures appear in a wide variety of problems from different areas of knowledge. As a consequence, there exist a great number of modal logics. In practice, every time a new modal logic is defined, many theorems must be proved and peer-reviewed again for this new logic. This process, besides being tedious, is error-prone. Fortunately, the task of writing complex proofs has increasingly begun to be assisted by computational tools. In this work, we formalize and verify an invariance under bisimulation result in the proof assistant Coq for a particular family of dynamic modal logics that change the accessibility relation of a model. Fil: Trucco, Francisco Carlos. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2020-02-17T12:00:58Z 2020-02-17T12:00:58Z 2019-03 bachelorThesis info:eu-repo/semantics/publishedVersion http://hdl.handle.net/11086/14648 spa Atribución 4.0 Internacional http://creativecommons.org/licenses/by/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	Verificación Formal Lógicas Modales Lógicas Dinámicas Asistente de Prueba Logic Logic and verification Modal and temporal logics (High Relevance) Theory of computation Formal Verification Coq
spellingShingle	Verificación Formal Lógicas Modales Lógicas Dinámicas Asistente de Prueba Logic Logic and verification Modal and temporal logics (High Relevance) Theory of computation Formal Verification Coq Trucco, Francisco Carlos Verificación de lógicas modales dinámicas en Coq
topic_facet	Verificación Formal Lógicas Modales Lógicas Dinámicas Asistente de Prueba Logic Logic and verification Modal and temporal logics (High Relevance) Theory of computation Formal Verification Coq
description	Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019.
author2	Fervari, Raúl Alberto
author_facet	Fervari, Raúl Alberto Trucco, Francisco Carlos
format	bachelorThesis publishedVersion
author	Trucco, Francisco Carlos
author_sort	Trucco, Francisco Carlos
title	Verificación de lógicas modales dinámicas en Coq
title_short	Verificación de lógicas modales dinámicas en Coq
title_full	Verificación de lógicas modales dinámicas en Coq
title_fullStr	Verificación de lógicas modales dinámicas en Coq
title_full_unstemmed	Verificación de lógicas modales dinámicas en Coq
title_sort	verificación de lógicas modales dinámicas en coq
publishDate	2020
url	http://hdl.handle.net/11086/14648
work_keys_str_mv	AT truccofranciscocarlos verificaciondelogicasmodalesdinamicasencoq
_version_	1782015068148334592

Verificación de lógicas modales dinámicas en Coq

Ejemplares similares