Интерактивное доказательство теорем ( ITP ) - это ежегодная международная научная конференция, посвященная автоматическому доказательству теорем , помощникам по доказательствам и связанным темам, начиная от теоретических основ и заканчивая аспектами реализации и приложениями в проверке программ , безопасности и формализации математики .
ITP объединяет сообщества, использующие множество систем, основанных на логике более высокого порядка, таких как ACL2 , Coq , Mizar , HOL , Isabelle , Lean , NuPRL , PVS и Twelf . Индивидуальные семинары или встречи, посвященные отдельным системам, обычно проводятся одновременно с конференцией.
Вместе с КАДОЙ и Tableaux , ИТП, как правило , один из трех основных конференций Международной совместной конференции по автоматизированному Рассуждению (IJCAR) всякий раза , когда он собирается ,
История [ править ]
Первое собрание ITP состоялось 11–14 июля 2010 г. в Эдинбурге, Шотландия, в рамках конференции Federated Logic Conference . Это расширение серии конференций по доказательству теорем в логике высокого порядка ( TPHOL ) на широкую область интерактивного доказательства теорем. Встречи TPHOL проходили ежегодно с 1988 по 2009 год.
Первые три были неформальными встречами пользователей системы HOL и были единственными, на которых не было опубликованных документов. С 1990 года TPHOLs опубликовала официальные рецензируемых научных трудов, опубликованных Springer «s Lecture Notes в области компьютерных наук серии. Он также привлекает все более широкое поле интересов.
Внешние ссылки [ править ]
