Resumo

O objetivo deste trabalho é apresentar um ambiente para resolução de fórmulas lógicas através do método de dedução do cálculo proposicional. A ferramenta apresentada no presente trabalho é a primeira versão do ambiente. Esta versão permite a interação do usuário com ambiente e a dedução de fórmulas que podem ser resolvidas usando as regras básicas não hipotéticas de inferência.