Automatización para el entorno Isabelle / ZF

Abstract

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.