“Automatización para el entorno Isabelle/ZF”

Enlace de Meet: https://meet.google.com/okm-yyfg-vsb

Resumen: 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.