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

This article may rely excessively on sources too closely associated with the subject, potentially preventing the article from being verifiable and neutral. Please help improve it by replacing them with more appropriate citations to reliable, independent sources. (January 2025) (Learn how and when to remove this message)

Интерактивное доказательство теорем ( ITP ) — ежегодная международная научная конференция, посвящённая теме автоматизированного доказательства теорем , помощников в доказательстве и смежным темам, от теоретических основ до аспектов реализации и приложений в верификации программ , безопасности и формализации математики .

ITP объединяет сообщества, использующие множество систем, основанных на логике высшего порядка, таких как ACL2 , Coq , Mizar , HOL , Isabelle , Lean , NuPRL , PVS и Twelf . Отдельные семинары или встречи, посвященные отдельным системам, обычно проводятся одновременно с конференцией.

Вместе с CADE и TABLEAUX , ITP обычно является одной из трех основных конференций Международной объединенной конференции по автоматизированному обоснованию (IJCAR), когда бы она ни созывалась,

Первое заседание ITP состоялось 11–14 июля 2010 года в Эдинбурге, Шотландия, в рамках конференции Federated Logic Conference. Это расширение серии конференций Theorem Proving in Higher Order Logics ( TPHOLs ) на широкую область интерактивного доказательства теорем. Встречи TPHOLs проводились ежегодно с 1988 по 2009 год.

Первые три были неформальными встречами пользователей системы HOL и были единственными, на которых не было опубликованных статей. С 1990 года TPHOLs публикует формальные рецензируемые труды, издаваемые в серии Lecture Notes in Computer Science компании Springer . Он также охватывал все более широкую область интересов.

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