Registro:
| Documento: | Tesis de Grado |
| Título: | Recuperando 'fórmulas culpables' de un lenguaje deóntico mediante el mapeo inverso de unsat cores |
| Autor: | Mazzini, Damián |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2025-06-12 |
| Fecha de defensa: | 2021 |
| Fecha en portada: | 2021 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Schapachnik, Fernando Pablo |
| Jurado: | Czemerinski, Hernán; Mera, Sergio Fernando |
| Idioma: | Español |
| Palabras clave: | FORMALEX; NUSMV; PICOSAT; UNSAT CORE |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000564_Mazzini |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000564_Mazzini.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000564_Mazzini |
| Ubicación: | Dep.COM 000564 |
| 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. Mazzini, Damián. (2021). Recuperando 'fórmulas culpables' de un lenguaje deóntico mediante el mapeo inverso de unsat cores. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000564_Mazzini |
Resumen:
FormaLex es un conjunto de herramientas que tiene como objetivo modelar y analizar sistemas legales realizando de manera automatizada verificaciones de fórmulas lógicas que representan textos normativos. Como resultado de la ejecución, FormaLex determina si un documento normativo es consistente o si por el contrario se hallaron inconsistencias. En este proceso de verificación intervienen distintas herramientas, entre ellas se encuentra NuSMV que es un model checker utilizado como motor de razonamiento. Este trabajo se centra principalmente en la interacción entre FormaLex y NuSMV, tanto en la optimización de los archivos que sirven como input de NuSMV como en la interpretación del output del mismo. Con respecto a la primera tarea el problema consiste en que los archivos de autómatas que se generan y que sirven de input de NuSMV pueden llegar a ser de gran volumen. Esto no solo impacta en la performance de la ejecución sino que también se identificó una limitación en NuSMV que no permite inputs que superen un tamaño específico. La propuesta para abordar esta problemática se centra en realizar una reducción del tamaño de estos archivos de manera que permita a una mayor cantidad de casos ser admitidos por NuSMV. En el caso de la segunda tarea, el problema está relacionado con que actualmente el model checker al momento de responder que existe una contradicción no da indicios de cuáles son las fórmulas involucradas en la misma. En un trabajo previo llamado Recuperación de “fórmulas culpables” mediante análisis de unsat core de Francisco Giménez se realizaron modificaciones a las herramientas que intervienen en el proceso de verificación de modelos, el model checker NuSMV y su interacción con el SAT solver Picosat. Dichas modificaciones permitieron formar un vínculo directo entre las variables del unsat core y las variables del model checker. Esta información brindada resulta valiosa para entender en dónde residen las inconsistencias, por lo que la propuesta de este trabajo en este aspecto consiste en tomar la información resultante de la extracción de unsat core y procesarla para identificar las variables de alto nivel involucradas en las fórmulas que hacen que un modelo legal no sea satisfacible.
Citación:
---------- APA ----------
Mazzini, Damián. (2021). Recuperando 'fórmulas culpables' de un lenguaje deóntico mediante el mapeo inverso de unsat cores. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000564_Mazzini
---------- CHICAGO ----------
Mazzini, Damián. "Recuperando 'fórmulas culpables' de un lenguaje deóntico mediante el mapeo inverso de unsat cores". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2021.https://hdl.handle.net/20.500.12110/seminario_nCOM000564_Mazzini
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000564_Mazzini.pdf
Distrubución geográfica
