doctoralThesis
Transformations for proof-graphs with cycle treatment augmented via geometric perspective techniques
Registro en:
Vaz Alves, Gleifer; José Guerra Barreto de Queiroz, Ruy. Transformations for proof-graphs with cycle treatment augmented via geometric perspective techniques. 2009. Tese (Doutorado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2009.
Autor
Vaz Alves, Gleifer
Institución
Resumen
O presente trabalho é baseada em dois aspectos fundamentais: (i) o estudo de procedimentos
de normalização para sistemas de provas, especialmente para a lógica clássica com dedução
natural; e (ii) a investigação de técnicas da perspectiva geométrica aplicadas em propriedades
da teoria da prova. Com isso, a motivação específica deste trabalho reside principalmente na
análise daqueles trabalhos que estão voltados à definição de técnicas da normalização através
de mecanismos da perspectiva geométrica. Destaca-se que técnicas da perspectiva geométrica
trazem o uso de arcabouços gráficos e/ou topológicos com a finalidade de representar sistemas
formais de provas e suas propriedades. Dessa forma, a primeira parte do documento apresenta
o uso de técnicas e arcabouços topológicos para estabelecer algumas propriedades, como, por
exemplo, o critério de corretude e a normalização de sistemas de prova. Ao passo que a segunda
parte do documento é inicialmente direcionada à descrição de algumas abordagens de
normalização (principalmente) para a lógica clássica com dedução natural. E o complemento
da segunda parte é dedicado à definição do principal objetivo do trabalho, i.e., desenvolver um
procedimento de normalização para o conjunto completo de operadores dos N-Grafos, através
do auxílio de algumas técnicas de perspectiva geométrica. (Destaca-se que as técnicas de perspectiva
geométrica, aplicadas à normalização dos N-Grafos, não fazem uso de arcabouços
topológicos). N-Grafos é um sistema de prova com múltipla conclusão definido para lógica
clássica proposicional com dedução natural. Ademais, os N-Grafos possuem tanto regras lógicas
como estruturais, estruturas cíclicas são permitidas e além disso as derivações são representadas
como grafos direcionados. De fato, a princpal característica do procedimento de
normalização aqui apresentado é fornecer um tratamento completo para as estruturas cíclicas.
Ou seja, são definidas classes de ciclos válidos, critério de corretude, propriedades e ainda
um algoritmo específico para normalizar os ciclos nos N-Grafos. Destaca-se que esses elementos
são construídos através do auxílio de arcabouços gráficos. Além disso, o mecanismo
de normalização é capaz de lidar com os diferentes papéis executados pelos operadores ?/>.
Adicionalmente, apresenta-se uma prova direta da normalização fraca para os N-Grafos, bem
como, a determinação das propriedades da subfórmula e da separação Coordenação de Aperfeiçoamento de Pessoal de Nível Superior