Como sabemos, há diversos metodos de prova para diferentes lógicas, como sistemas axiomáticos, sistemas de tableaux e sistemas de dedução natural. Cada um desses sistemas, no entanto, apresentam certas vantagens e desvantagens: alguns requerem extrema criatividade para se ter uma prova, outros dependem fortemente de aspectos semânticos de lógicas específicas, e outros ainda são demasiadamente complicado para lógicas não-clássicas. O cálculo de sequentes, desenvolvido por Gentzen para estudar a relação de derivabilidade, apresenta uma alternativa à esses métodos que não partilha das mesmas desvantagens. Nessa palestra, apresentarei o sistema para o cálculo de sequentes para a lógica clássica e como ele pode servir como um método de provas para a lógica modal, através da definição de nested sequents.