Implementação e automação de sistemas de dedução

Abstract

Sistemas lógicos permitem descrever e raciocinar de forma rigorosa acerca dos mais variados domínios, sejam eles teorias matemáticas abstractas como álgebra, análise ou geometria, ou áreas mais aplicadas como especificação de software, verificação de hardware ou processamentode linguagens naturais. Este rigor é conseguido à custa da utilização de linguagens bem definidas, que podem ser interpretadas de forma precisa sobre os domínios que pretendemos estudar. Assim, construíndo frases nestas linguagens lógicas, que designamos por proposições ou fórmulas, expressamos propriedades nos respectivos domínios, que poderão ser satisfeitas sempre, nunca, ou apenas mediante determinadas circunstâncias. Interessa-nos conseguir raciocinar acerca destas propriedades, ser capazes de determinar se são ou não sempre verificadas no nosso domínio de estudo, ou de um modo mais geral, se são verificadas mediante determinadas condições, ou seja, como consequência da verificação de certas propriedades no domínio. Tomando como exemplo a área da aritmética de inteiros, podemos querer tentar determinar se "qualquer número inteiro pode ser escrito como a soma de dois quadrados perfeitos", ou não. Uma representação comum desta frase num sistema lógico é dada por Vk. Ǝ m. Ǝ n. k = m2 + n2. Para que este tipo de estudo seja efectuado de forma rigorosa, é necessário não só a representação e interpretação precisa destas propriedades, mas uma base formal, perfeitamente definida, que sirva de suporte aos raciocínios efectuados durante esse mesmo estudo. Os sistemas lógicos dedutivos formam essa base. Tomando como ponto de partida relações de consequência elementares entre fórmulas (axiomas) e regras básicas que permitem inferir novas conclusões a partir de consequências conhecidas ou assumidas válidas num determinado contexto (regras de inferência), é possível criar e apresentar raciocínios de forma clara e concisa acerca dos objectos de estudo, ou seja, efectuar demonstrações no sistema. O objectivo deste trabalho passa por estudar sistemas lógicos dedutivos, com especial ênfase na sua implementação numa linguagem de programação (Haskell), tendo em vista a automação do processo de demonstração.