インタラクティブ定理証明（カンファレンス）

インタラクティブ定理証明( ITP ) は、自動定理証明、証明アシスタント、および関連するトピックに関する年次国際学術会議で、理論的基礎から実装面、プログラム検証、セキュリティ、数学の形式化におけるアプリケーションまでを扱っています。

ITP は、 ACL2、Coq、Mizar、HOL、Isabelle、Lean、NuPRL、PVS、Twelfなど、高階論理に基づく多くのシステムを使用するコミュニティを結集します。通常、個々のシステムに特化した個別のワークショップや会議がカンファレンスと同時に開催されます。

ITPはCADEやTABLEAUXとともに、国際自動推論合同会議（IJCAR）が開催されるたびに開催される3つの主要会議の1つです。

ITP の初会合は、2010 年 7 月 11 日から 14 日まで、スコットランドのエジンバラで、Federated Logic Conference の一環として開催されました。これは、Theorem Proving in Higher Order Logics ( TPHOL ) カンファレンス シリーズを、インタラクティブな定理証明の幅広い分野に拡張したものです。TPHOL ミーティングは、1988 年から 2009 年まで毎年開催されました。

最初の 3 回はHOLシステムの非公式なユーザー ミーティングであり、論文が出版されなかった唯一のミーティングでした。1990 年以降、TPHOL はSpringerのLecture Notes in Computer Scienceシリーズで、正式な査読済み議事録を出版しています。また、TPHOL はますます幅広い関心を集めています。

• 公式サイト