Интерактивное доказательство теорем ( ITP ) — это ежегодная международная научная конференция , посвященная теме автоматизированного доказательства теорем , помощников по доказательству и смежным темам, начиная от теоретических основ и заканчивая аспектами реализации и приложениями для проверки программ , безопасности и формализации математики .
ITP объединяет сообщества, используя множество систем, основанных на логике более высокого порядка, таких как ACL2 , Coq , Mizar , HOL , Isabelle , Lean , NuPRL , PVS и Twelf . Одновременно с конференцией обычно проводятся отдельные семинары или встречи, посвященные отдельным системам.
Вместе с CADE и TABLEAUX ITP обычно является одной из трех основных конференций Международной объединенной конференции по автоматизированному мышлению (IJCAR), когда бы она ни созывается.
Учредительное собрание ITP состоялось 11–14 июля 2010 г. в Эдинбурге, Шотландия, в рамках конференции Federated Logic Conference. Это расширение серии конференций «Доказательство теорем в логике высшего порядка » ( TPHOL ) на широкую область интерактивного доказательства теорем. Встречи TPHOL проходили ежегодно с 1988 по 2009 год.
Первые три были неформальными собраниями пользователей системы HOL и были единственными собраниями без опубликованных документов. С 1990 года TPHOL публикует официальные рецензируемые труды, опубликованные в серии лекций Springer 's Lecture Notes in Computer Science . Это также развлекало все более широкую сферу интересов.