| Título: | Lidando com a legibilidade de provas em Isabelle |
| Autor(es): | Rodrigues, Rafael Monteiro |
| Orientador(es): | Nalon, Cláudia |
| Assunto: | Software - desenvolvimento
Raciocínio automatizado |
| Data de apresentação: | 25-Jul-2023 |
| Data de publicação: | 6-Out-2023 |
| Referência: | RODRIGUES, Rafael Monteiro. Lidando com a legibilidade de provas em Isabelle. 2023. 67 f., il. Trabalho de conclusão de curso (Bacharelado em Ciência da Computação) — Universidade de Brasília, Brasília, 2023. |
| Resumo: | O raciocínio automatizado é a área de inteligência artificial que busca criar ferramentas
capazes de simular o raciocínio humano. Estas ferramentas são bastante úteis no domínio
da prova automática de teoremas. No entanto, um fator a ser considerado é a possí-
vel dificuldade que provas automaticamente encontradas podem apresentar quanto à sua
legibilidade.
A legibilidade de provas é um tema de grande importância, pois está diretamente
ligada com a divulgação de resultados científicos. Neste trabalho, o problema central
abordado é o aprimoramento da legibilidade de provas produzidas por meio da interação
com assistentes de provas, com um foco em provas produzidas com o auxílio de ferramentas
de automação do raciocínio, utilizando técnicas de melhoria da legibilidade propostas por
Zammit [1] e Lamport [2].
Como base teórica, este trabalho utiliza a lógica de predicados de ordem superior e
a dedução natural. Este alicerce teórico é usado por meio da ferramenta Isabelle, um
assistente de provas que utiliza a lógica de ordem superior, e que neste projeto serviu
como ferramenta principal.
Para ilustrar os conceitos abordados, este projeto apresenta um estudo de caso onde
se faz a especificação e verificação formal de um sistema de comando e controle. Esta
verificação é feita por meio da prova de alguns teoremas que demonstram propriedades
da especificação. O central do trabalho consiste na reescrita dessas provas, inicialmente
feitas com um alto grau de automação, para provas mais legíveis para humanos, utilizando
técnicas de aprimoramento da legibilidade extraídas da literatura a respeito do tema. |
| Abstract: | Automated reasoning is the area of artificial intelligence that seeks to create tools
capable of simulating human reasoning. These tools are very useful in the domain of
automated theorem proving. However, one factor to be considered is the possible difficulty
that automatically produced proofs may present regarding their readability.
The readability of proofs is a topic of great importance, as it is directly linked to
the dissemination of scientific results. In this work, the central problem addressed is the
improvement of the readability of proofs produced through the interaction with proof
assistants, with a focus on proofs produced with the aid of automated reasoning tools
using techniques for the improvement of proof legibility proposed by Zammit [1] and
Lamport [2]..
This work uses higher-order predicate logic and natural deduction as it’s theoretic
foundation. These concepts are used in practice with Isabelle, a proof assistant that uses
higher-order logic.
To illustrate the concepts covered, this project presents a case study regarding the
formal specification and verification of a command and control system. This verification
is done through the proof of several theorems that demonstrate properties of the spec-
ification. The central part of the work consists in rewriting these proofs, initially done
with a high degree of of automation, to more human-readable proofs using techniques for
improving the legibility of proofs taken from the literature available on this topic. |
| Informações adicionais: | Trabalho de conclusão de curso (graduação) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2023. |
| Licença: | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor que autoriza a Biblioteca Digital da Produção Intelectual Discente da Universidade de Brasília (BDM) a disponibilizar o trabalho de conclusão de curso por meio do sítio bdm.unb.br, com as seguintes condições: disponível sob Licença Creative Commons 4.0 International, que permite copiar, distribuir e transmitir o trabalho, desde que seja citado o autor e licenciante. Não permite o uso para fins comerciais nem a adaptação desta. |
| Aparece na Coleção: | Ciência da Computação
|
Todos os itens na BDM estão protegidos por copyright. Todos os direitos reservados.
