A lógica formal desempenha um papel fundamental na ciência da computação. É necessário introduzir os fundamentos dessa disciplina para que esses alunos possam alcançar o domínio em todas as suas aplicações em ciência da computação. Infelizmente, observa-se que a eficiência do processo de aprendizagem do programa de Bacharelado em Sistemas de Informação se mostrou menos do que ideal. Neste trabalho, propomos que é possível aumentar a efetividade do processo de aprendizagem através do uso de assistentes de prova como ferramenta de ensino, mas com a introdução de elementos do tipo jogo. Essa abordagem é conhecida como gamificação. Apresentamos uma visão geral da base teórica que apóia o uso da gamificação. Em seguida, descrevemos a proposta de um sistema gamificado para o aprendizado da lógica formal, bem como a implementação de um protótipo desse sistema proposto. Concluímos este artigo apresentando alguns resultados de um experimento realizado adotando nosso protótipo como ferramenta de aprendizado durante um semestre acadêmico. Em seguida, comparamos esses resultados com o semestre anterior e analisamos as possibilidades do uso da gamificação em um ambiente educacional.