¿Qué es?

Es una secuencia de enunciados, los cuales o bien son premisas, o bien se han obtenido de la aplicación de un conjunto finito de reglas de inferencia a enunciados anteriores (que le preceden en la secuencia).