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.
Junho 26, 2020, 15:0
Publicação
Obra sujeita a Direitos de Autor
Orientação
