BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Departamento de Computación - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Departamento de Computación
X-ORIGINAL-URL:https://www.dc.uba.ar
X-WR-CALDESC:Eventos para Departamento de Computación
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Sao_Paulo
BEGIN:STANDARD
TZOFFSETFROM:-0300
TZOFFSETTO:-0300
TZNAME:-03
DTSTART:20200101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20210615T140000
DTEND;TZID=America/Sao_Paulo:20210615T150000
DTSTAMP:20260507T221000
CREATED:20210604T164539Z
LAST-MODIFIED:20210615T170124Z
UID:6727-1623765600-1623769200@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Damián Mazzini
DESCRIPTION:Título: Recuperando ‘fórmulas culpables’ de un lenguaje deóntico mediante el mapeo inverso de unsat cores\nDirector: Fernando Schapachnik\nJurados: Sergio Mera y Hernán Czemerinski \nResumen: \nFormaLex 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. \nEste trabajo se centra principalmente en la interacción entre FormaLex y NuSMV\, principalmente en la interpretación del output del mismo. 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 un trabajo previo 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.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-damian-mazzini/
LOCATION:http://www.youtube.com/watch?v=BYbw2ycj_QM
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR