Sobre os fundamentos da Programação Lógica Paraconsciente

Inicialmente este trabalho estava focado em encontrar regras de resolução para lógicas paraconsistentes, mais especificamente para versões quantificadas de primeira ordem das Lógicas da Inconsistência Formal (LFI’s), tendo em vista aplicações no campo da programação lógica como ferramenta para a pesquisa em inteligência artificial e representação do conhecimento inconsistente (e.g. bancos de dados inconsistentes). Tal proposta se mostrou fora de nosso alcance, principalmente por demandar uma versão do teorema de Herbrand para tais cálculos. Terminamos, por fim, com um trabalho nos fundamentos da programação lógica paraconsistente: com uma nova técnica de demonstração dos Teoremas de Completude para as LFI’s quantificadas, uma formulação por sequentes das LFI’s QmbC e QmCi além do teorema da eliminação do corte, juntamente com uma versão do teorema de Herbrand restrita ao fragmento Pi_2, para QmbC.