La demostración interactiva de teoremas ( ITP ) es una conferencia académica internacional anual sobre el tema de la demostración automatizada de teoremas , asistentes de demostración y temas relacionados, que van desde fundamentos teóricos hasta aspectos de implementación y aplicaciones en verificación de programas , seguridad y formalización de las matemáticas .
ITP reúne a las comunidades utilizando muchos sistemas basados en lógica de orden superior como ACL2 , Coq , Mizar , HOL , Isabelle , Lean , NuPRL , PVS y Twelf . Los talleres individuales o reuniones dedicadas a sistemas individuales por lo general se llevan a cabo al mismo tiempo que la conferencia.
Junto con CADE y TABLEAUX , ITP suele ser una de las tres conferencias principales de la International Joint Conference on Automated Reasoning (IJCAR) siempre que se convoca,
La reunión inaugural de ITP se llevó a cabo del 11 al 14 de julio de 2010 en Edimburgo, Escocia, como parte de la Conferencia de lógica federada. Es la extensión de la serie de conferencias Demostración de teoremas en lógica de orden superior ( TPHOL ) al amplio campo de la demostración interactiva de teoremas. Las reuniones de TPHOL se llevaron a cabo todos los años desde 1988 hasta 2009.
Las tres primeras fueron reuniones informales de usuarios del sistema HOL y fueron las únicas sin artículos publicados. Desde 1990, TPHOLs ha publicado procedimientos formales revisados por pares, publicados por la serie Lecture Notes in Computer Science de Springer . También ha entretenido un campo de interés cada vez más amplio.