Formas normais de fórmulas em lógica de primeira ordem e aplicações em dedução automática

Abstract

Pesquisas recentes em prova automática de teoremas para lógica clausal de primeira ordem lidam com fórmulas representadas em apenas uma de suas formas normais, conjuntiva ou disjuntiva, para realizar inferências lógicas. No entanto, a autora toma outro caminho e examina o uso simultâneo de ambas formas normais de uma fórmula para realizar estas inferências. A motivação original foi o desenvolvimento de uma estratégia que melhorasse a eficiência do Método de Inferência por Transformação Dual (Método Dual). Este método, para lógica de primeira ordem, processa uma inferência lógica sem a explícita aplicação de nenhuma regra de inferência; ao invés, ele transforma sucessivamente a fórmula em suas formas normais conjuntiva e disjuntiva e remove as contradições tornadas explícitas por estas transformações. A fim de desenvolver uma estratégia que explorasse a representação de uma fórmula nas duas formas normais, relações estruturais apresentadas por esta representação foram formalizadas e usadas como base para expressar e filtrar inferências realizadas durante o processo de dedução. Conseqüentemente, este trabalho apresenta resultados em duas áreas: as formas normais de uma fórmula lógica, suas relações, simplificação e transformação de uma para a outra; e a estratégia propriamente dita. Embora o uso simultâneo de ambas formas normais pela estratégia tenha se mostrado redundante, este estudo deu origem a um novo método de inferência com interessantes características: (i) ele combina atributos de ambos cálculos: de saturação e de tableau e conexão, (ii) ele permite o processamento paralelo de inferências, e (iii) ele facilita o reuso de inferências previamente efetuadas. Estas são características não encontradas em nenhum outro método conhecido pela autora.