La lógica demostrativa es una lógica modal, en la que el operador caja (o "necesidad") es interpretado significando 'debe ser demostrado que'.
Existen varias lógicas demostrativas, algunas de las cuales están tratadas en la literatura en la sección de referencias.
El mismo se puede obtener agregando la versión modal del teorema de Löb a la lógica K (o K4).
Desde entonces el principal investigador del tema ha sido George Boolos.
Los siguientes especialistas han realizado contribuciones significativas al tema: Sergei Artemov, Lev Beklemishev, Giorgi Japaridze, Dick de Jongh, Franco Montagna, Giovanni Sambin, Vladimir Shavrukov, Albert Visser entre otros.