Registro:
| Documento: | Tesis de Grado |
| Título: | PRK, una lógica constructiva clásica |
| Título alternativo: | PRK, a constructive classical logic |
| Autor: | Freund, Teodoro |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2023-09-12 |
| Fecha de defensa: | 2021-11-05 |
| Fecha en portada: | 2021 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Barenbaum, Pablo |
| Idioma: | Español |
| Palabras clave: | LOGICA; CURRY-HOWARD; LOGICA CLASICA; PROPOSICIONES COMO TIPOS; LOGICA CONSTRUCTIVA; SEMANTICA DE KRIPKELOGIC; CURRY-HOWARD; CLASSICAL LOGIC; PROPOSITION AS TYPES; CONSTRUCTIVE LOGIC; KRIPKE SEMANTICS |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000486_Freund |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000486_Freund.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000486_Freund |
| Ubicación: | Dep.COM 000486 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Freund, Teodoro. (2021). PRK, una lógica constructiva clásica. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000486_Freund |
Resumen:
Esta tesis presenta el sistema prk, un sistema lógico en el cual las nociones de prueba y refutación son duales. Este sistema extiende a la lógica clásica y es constructivo en el sentido de que se lo puede dotar de una interpretación computacional con buenas propiedades. Las fórmulas de prk se clasifican a lo largo de dos ejes, dependiendo de su positividad (afirmación o negación) y su fuerza (fuerte o clásica). Las proposiciones fuertes se demuestran, canónicamente, con reglas de introducción, mientras que las proposiciones clásicas se demuestran por reducción al absurdo. El sistema prk resulta ser correcto y completo con respecto a una clase de modelos de Kripke, definida en este mismo trabajo. Siguiendo la correspondencia de Curry–Howard, se formaliza un cálculo asociado a prk, denominado λprk, cuyo sistema de tipos se corresponde con la lógica prk. Se establecen varias propiedades sobre λprk, incluyendo preservación de tipos, confluencia y una caracterización de las formas normales de las pruebas y refutaciones. La terminación fuerte del cálculo λprkse demuestra a través de una traducción a System F extendido con ecuaciones recursivas entre tipos, y apoyándose en un resultado de Mendler. Por último, se considera una extensión a segundo orden del sistema prk, junto con el cálculo correspondiente λ2prk. Se extienden a este marco los resultados anteriormente mencionados, exceptuando la terminación fuerte de λ2prk, que queda abierta como trabajo futuro.
Abstract:
This thesis introduces prk, a constructive classical logic with dual proofs and refutations that refines classical logic and provides a well behaved computational interpretation for it. Formulas in prk can be classified along two axes, depending on their positivity (affirmation or denial) and their strength (strong or classical). Strong propositions are, canonically, proved with introduction rules, whereas the proof of a classical proposition always proceeds by contradiction. The system prk is shown to be sound and complete with respect to a particular kind of Kripke semantics, also defined in this work. A calculus for prk, dubbed λprk, is formalized. Its type system is in close correspondence with the logical rules of prk, in the sense of the propositions-as-types paradigm. A number of properties, including subject reduction, confluence, and a characterization of canonical proofs and refutations, are established. Strong normalization of this calculus is proved via a translation to System F with Mendlerstyle recursive type constraints. Finally, an extension of prk to second order logic is presented, including a corresponding calculus λ2prk. The aforementioned results are extended to this setting, except for strong normalization of λ2prk, which is left as future work.
Citación:
---------- APA ----------
Freund, Teodoro. (2021). PRK, una lógica constructiva clásica. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000486_Freund
---------- CHICAGO ----------
Freund, Teodoro. "PRK, una lógica constructiva clásica". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2021.https://hdl.handle.net/20.500.12110/seminario_nCOM000486_Freund
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000486_Freund.pdf
Distrubución geográfica
