Интерактивное доказательство теорем (конференция)

Интерактивное доказательство теорем ( 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 . Это также привлекло все более широкую сферу интересов.

Внешние ссылки

• Официальный сайт