Automatización para el entorno Isabelle / ZF

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, 2021.

Guardado en:
Detalles Bibliográficos
Autor principal: Steinberg, Matías Uriel
Otros Autores: Pagano, Miguel María
Formato: publishedVersion bachelorThesis
Lenguaje:Español
Publicado: 2021
Materias:
Formalización
Relativización
Hipótesis del continuo
Isabelle / ZF
Theory of computation
Logic
Forcing
Acceso en línea:http://hdl.handle.net/11086/17550
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-17550
record_format dspace
spelling I10-R141-11086-175502023-08-31T13:19:02Z Automatización para el entorno Isabelle / ZF Steinberg, Matías Uriel Pagano, Miguel María Formalización Relativización Hipótesis del continuo Isabelle / ZF Theory of computation Logic Forcing Tesis (Lic. en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2021. publishedVersion Fil: Steinberg, Matías Uriel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Al formalizar en Isabelle/ZF las definiciones asociadas a Forcing para demostrar la independencia de la Hipótesis del Continuo, se presenta una cantidad significativa de tareas sistemáticas y repetitivas, entre las que se destacan la relativización de términos y predicados, por un lado, y la síntesis de fórmulas internalizadas, por el otro. Por lo tanto, se desea evitar el trabajo manual todo lo posible. Este trabajo consiste en brindar herramientas automáticas que se encarguen de dichas tareas y minimicen la cantidad de intervenciones manuales requeridas. Más aún, se justificará con cierto grado de formalidad la corrección de los métodos implementados, y también se detallará la intuición detrás de las partes más complejas. Finalmente, se mostrará cuál es la disciplina a seguir a la hora de utilizar los comandos implementados. When the definitions regarding Forcing are being formalised in Isabelle/ZF, in order to prove the independence of the Continuum Hypothesis, a lot of systematic and repetitive tasks are required. Among them, relativization of terms and predicates, on the one hand, and synthesis of internalized formulas, on the other hand, are the most important ones. Thus, it is desired to reduce manual intervention as much as possible. In this thesis, some automatic tools will be provided to take care of those tasks, and will reduce the amount of manual interventions required. Furthermore, the soundness of the implemented methods will be formally justified, and the intuition behind the most complex parts will also be detailed. Finally, the whole discipline to use the commands will be shown. publishedVersion Fil: Steinberg, Matías Uriel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2021-03-26T19:12:12Z 2021-03-26T19:12:12Z 2021-03 bachelorThesis http://hdl.handle.net/11086/17550 spa Atribución-NoComercial-CompartirIgual 4.0 Internacional http://creativecommons.org/licenses/by-nc-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 Formalización
Relativización
Hipótesis del continuo
Isabelle / ZF
Theory of computation
Logic
Forcing
spellingShingle Formalización
Relativización
Hipótesis del continuo
Isabelle / ZF
Theory of computation
Logic
Forcing
Steinberg, Matías Uriel
Automatización para el entorno Isabelle / ZF
topic_facet Formalización
Relativización
Hipótesis del continuo
Isabelle / ZF
Theory of computation
Logic
Forcing
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, 2021.
author2 Pagano, Miguel María
author_facet Pagano, Miguel María
Steinberg, Matías Uriel
format publishedVersion
bachelorThesis
author Steinberg, Matías Uriel
author_sort Steinberg, Matías Uriel
title Automatización para el entorno Isabelle / ZF
title_short Automatización para el entorno Isabelle / ZF
title_full Automatización para el entorno Isabelle / ZF
title_fullStr Automatización para el entorno Isabelle / ZF
title_full_unstemmed Automatización para el entorno Isabelle / ZF
title_sort automatización para el entorno isabelle / zf
publishDate 2021
url http://hdl.handle.net/11086/17550
work_keys_str_mv AT steinbergmatiasuriel automatizacionparaelentornoisabellezf
_version_ 1782013968024338432

Ejemplares similares