Registro:
| Documento: | Tesis de Grado |
| Título: | PPA - Un asistente de demostración para lógica de primer orden con extracción de testigos usando la traducción de Friedman |
| Título alternativo: | PPA - A proof-assistant for first-order logic with witness extraction using Friedman’s translation |
| Autor: | Panichelli, Manuel |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2025-06-12 |
| Fecha de defensa: | 2024-12-23 |
| Fecha en portada: | 2024 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Barenbaum, Pablo |
| Jurado: | Becher, Verónica Andrea; Pagano, Miguel |
| Idioma: | Español |
| Palabras clave: | ASISTENTE DE DEMOSTRACION; LOGICA DE PRIMER ORDEN; DEDUCCION NATURAL; LOGICA CLASICA; LOGICA INTUICIONISTA; EXTRACCION DE TESTIGOS; TRADUCCION DE FRIEDMANPROOF ASSISTANT; FIRST-ORDER LOGIC; NATURAL DEDUCTION; CLASSICAL LOGIC; INTUITIONISTIC LOGIC; WITNESS EXTRACTION; FRIEDMAN’S TRANSLATION |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000832_Panichelli |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000832_Panichelli.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000832_Panichelli |
| Ubicación: | Dep.COM 000832 |
| 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. Panichelli, Manuel. (2024). PPA - Un asistente de demostración para lógica de primer orden con extracción de testigos usando la traducción de Friedman. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000832_Panichelli |
Resumen:
Los asistentes de demostración son programas que simplifican la escritura de demostraciones matemáticas, permitiendo la colaboración masiva o la verificación formal de programas. Existen muchos asistentes como Mizar, Coq e Isabelle, basados en distintas teorías. Un criterio deseable que pueden cumplir es el de De Bruijn: a partir de demostraciones en un lenguaje de alto nivel se pueden extraer demostraciones en un lenguaje núcleo fácilmente verificable. Esto elimina la necesidad de tener que confiar en la implementación del asistente, ya que las demostraciones pueden ser verificadas por un programa independiente. En esta tesis se presenta PPA, un asistente de demostración para lógica clásica de primer orden. Cumple con el criterio de De Bruijn, generando demostraciones en el sistema lógico de deducción natural a partir de programas escritos en un lenguaje de alto nivel, cuyo objetivo es ser similar a cómo serían en lenguaje natural. Tiene un mecanismo principal de demostración, el by, que por debajo cuenta con un solver heurístico para lógica de primer orden que facilita la escritura de demostraciones. Está inspirado en el mecanismo análogo en Mizar. Algunos asistentes implementan la extracción de testigos de existencial. Dada una demostración de ∃x.p(x), se extrae un testigo t tal que cumpla p(t). Es sencillo hacerlo sobre lógica intuicionista por su naturaleza constructiva, pero un desafío sobre lógica clásica, que no lo es. Para ello hay dos grandes categorías: directas (mediante técnicas semánticas como realizabilidad clásica [Miq11]) o indirectas (mediante traducciones a otra lógica, como intuicionista). El aporte principal del trabajo es una implementación práctica de la extracción de testigos. PPA la implementa de forma indirecta usando la traducción de Friedman, que permite convertir demostraciones clásicas de fórmulas Π2 de la forma ∀y0 . . . ∀yn.∃x.φ, con φ sin cuantificadores, a demostraciones intuicionistas. Se describe cómo una vez traducidas pueden ser normalizadas usando reglas de reducción bien conocidas, que se corresponden con las reglas de reducción del cálculo lambda vistas desde el isomorfismo Curry-Howard. Finalmente, de una demostración normalizada se podrá extraer un testigo. Identificamos algunos detalles en la implementación práctica de la traducción, que limitan las fórmulas para las cuales se puede usar (más allá de la limitación teórica de Π2) y también limitan las axiomatizaciones de las teorías que se pueden hacer.
Abstract:
Proof assistants are programs that simplify the writing of mathematical proofs, enabling large-scale collaboration or the formal verification of programs. There are many proof assistants such as Mizar, Coq, and Isabelle, based on different theories. A desirable property they may have is described by the De Bruijn criterion: from proofs written in a high level language, one can extract proofs in a core, easily verifiable language. This eliminates the need to trust their implementation, as the extracted proofs can be verified by an independent program. This thesis presents PPA, a proof assistant for classical first-order logic. It fulfills De Bruijn’s criterion by generating proofs in the natural deduction proof system from high-level proofs, designed to resemble natural language as closely as possible. Its main proof mechanism, by, features an underlying heuristic solver for first-order logic, inspired by Mizar’s analogous mechanism. Some proof assistants implement existential witness extraction. Given a proof of ∃x.p(x), they extract a *witness* t such that p(x) holds. While this is straightforward in intuitionistic logic due to its constructive nature, it is challenging in classical logic, which lacks constructiveness. There are two main approaches: direct (using semantic techniques such as classical realizability [Miq11]) or indirect (via translations to another logic, such as intuitionistic). The main contribution of this work is a practical implementation of witness extraction. PPA achieves this indirectly by using Friedman’s translation, which allows converting classical proofs of Π2 formulas of the form ∀y0 . . . ∀yn.∃x.φ, with the formula φ having no quantifiers, into intuitionistic ones. We describes how, once translated, these proofs can be normalized using wellknown reduction rules, which correspond to the reduction rules of lambda calculus viewed through the Curry-Howard isomorphism. Finally, a normalized proof enables the extraction of a witness. We identify some practical implementation details of the translation, which limit the formulas for which it can be used (beyond the theoretical Π2 restriction) and also constrain the axiomatizations of theories that can be made.
Citación:
---------- APA ----------
Panichelli, Manuel. (2024). PPA - Un asistente de demostración para lógica de primer orden con extracción de testigos usando la traducción de Friedman. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000832_Panichelli
---------- CHICAGO ----------
Panichelli, Manuel. "PPA - Un asistente de demostración para lógica de primer orden con extracción de testigos usando la traducción de Friedman". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2024.https://hdl.handle.net/20.500.12110/seminario_nCOM000832_Panichelli
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000832_Panichelli.pdf
Distrubución geográfica
