Dissertação

Abduction Algorithm for First-Order Logic Reasoning Frameworks EVALUATED

Abdução é um processo através do qual podemos formular hipóteses que justificam um conjunto de factos observados, usando como base uma teoria. Este processo aborda assuntos reais relacionados com vários campos, como a medicina e a criminalidade, mantendo a sua utilidade em temas mais teóricos, como é o caso da combinação de lógicas. Apesar disto, existem algumas desvantagens, nomeadamente relativas à complexidade temporal e ao poder expressivo das fórmulas utilizadas. Nesta tese, abordamos este último problema. Estudamos as noções de sistema de consequência e de sistema de prova, apresentando também alguns exemplos destes sistemas. Formalizamos alguns conceitos teóricos relacionados com o princípio da Resolução, incluindo a correção e completude de refutação. Estendemos depois este princípio a fórmulas de Primeira Ordem. Formalizamos e implementamos um algoritmo de abdução para fórmulas de Primeira Ordem em Mathematica, baseado num algoritmo já existente e num conceito estendido do princípio de Resolução. Exploramos várias aplicações deste algoritmo. Como este algoritmo aceita fórmulas de Primeira Ordem, permite uma melhor representação de problemas concretos e, consequentemente, uma maior probabilidade de as respostas obtidas serem corretas. Mais, permite uma automatização da combinação de sistemas de prova, através da sua aplicação à determinação de uma função de abdução de um sistema de prova.
Sistemas de Consequência, Sistemas de Prova, Combinação de Lógicas, Algoritmo de Abdução, Estrutura de Raciocínio TCHF, Resolução

Junho 26, 2020, 15:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Jaime Arsénio de Brito Ramos

Departamento de Matemática (DM)

Professor Auxiliar