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

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

ITP объединяет сообщества, использующие множество систем, основанных на логике более высокого порядка, например ACL2, Coq, Мицар, HOL, Изабель, Худой, NuPRL, ПВС, и Двенадцать. Индивидуальные семинары или встречи, посвященные отдельным системам, обычно проводятся одновременно с конференцией.

Вместе с CADE и ТАБЛИЦА, ITP обычно является одной из трех основных конференций Международная совместная конференция по автоматизированному мышлению (IJCAR) всякий раз, когда он созывается,

История

Первое заседание ITP состоялось 11–14 июля 2010 г. в Эдинбурге, Шотландия, в рамках Федеративная логическая конференция. Это продолжение Доказательство теорем в логиках высокого порядка (TPHOLs) серия конференций по широкому кругу вопросов интерактивного доказательства теорем. Заседания TPHOL проходили ежегодно с 1988 по 2009 год.

Первые три были неформальными встречами пользователей для HOL системы и были единственными без опубликованных статей. С 1990 года TPHOL издает официальные рецензируемые труды, публикуемые Springer с Конспект лекций по информатике серии. Он также привлекает все более широкое поле интересов.

внешняя ссылка