Interaktywne dowodzenie twierdzeń (konferencja)

Interactive Theorem Proving ( ITP ) to coroczna międzynarodowa konferencja naukowa poświęcona zautomatyzowanemu dowodzeniu twierdzeń , asystentom dowodu i tematom pokrewnym, od podstaw teoretycznych po aspekty implementacyjne i zastosowania w weryfikacji programów , bezpieczeństwie i formalizacji matematyki .

ITP skupia społeczności korzystające z wielu systemów opartych na logice wyższego rzędu, takich jak ACL2 , Coq , Mizar , HOL , Isabelle , Lean , NuPRL , PVS i Twelf . Równolegle z konferencją odbywają się zazwyczaj indywidualne warsztaty lub spotkania poświęcone poszczególnym systemom.

Wraz z CADE i TABLEAUX , ITP jest zwykle jedną z trzech głównych konferencji Międzynarodowej Wspólnej Konferencji na temat Zautomatyzowanego Rozumowania (IJCAR), ilekroć się zwołuje,

Historia

Inauguracyjne spotkanie ITP odbyło się w dniach 11-14 lipca 2010 r. w Edynburgu w Szkocji w ramach Federated Logic Conference. Jest to rozszerzenie Theorem Proving in Higher Order Logics ( TPHOLs ) na szeroką dziedzinę interaktywnego udowadniania twierdzeń. Spotkania TPHOLs odbywały się corocznie od 1988 do 2009 roku.

Pierwsze trzy były nieformalnymi spotkaniami użytkowników systemu HOL i jako jedyne nie doczekały się publikacji. Od 1990 TPHOLs publikuje formalne recenzowane materiały, publikowane Springer 's Lecture Notes in Computer Science . Cieszyła się też coraz szerszym zainteresowaniem.

Linki zewnętrzne

• Oficjalna strona internetowa